Fix #3563

KeYProject · Feb 20, 2025 · af00212 · af00212
1 parent 51cf67e
commit af00212
Showing 1 changed file with 16 additions and 0 deletions.
diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/locSetsRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/locSetsRules.key
@@ -854,6 +854,22 @@
         \heuristics(classAxiom)
     };
 
+    // --------------------------------------------------------------------------
+    // equality rules
+    // --------------------------------------------------------------------------
+
+    // Proven in KeY (DD: 2025-02-20)
+    equalityOfSingleton {
+        \schemaVar \term Object o1, o2;
+        \schemaVar \term Field f1, f2;
+
+        \find(singleton(o1, f1) = singleton(o2, f2))
+
+        \replacewith(o1 = o2 & f1 = f2)
+
+        \heuristics(simplify)
+    };
+
     // --------------------------------------------------------------------------
     // lemmata for empty and allLocs
     // --------------------------------------------------------------------------