making equalityOfSingleton a proved lemma

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/locSetsRules.key

@@ -859,6 +859,7 @@
     // --------------------------------------------------------------------------
 
     // Proven in KeY (DD: 2025-02-20)
+    \lemma
     equalityOfSingleton {
         \schemaVar \term Object o1, o2;
         \schemaVar \term Field f1, f2;

key.core/tacletProofs/locSet/Taclet_equalityOfSingleton.proof

@@ -0,0 +1,138 @@
+\profile "Java Profile";
+
+\settings // Proof-Settings-Config-File
+{ 
+    "Choice" : { 
+        "JavaCard" : "JavaCard:on",
+        "Strings" : "Strings:on",
+        "assertions" : "assertions:on",
+        "bigint" : "bigint:on",
+        "floatRules" : "floatRules:strictfpOnly",
+        "initialisation" : "initialisation:disableStaticInitialisation",
+        "intRules" : "intRules:arithmeticSemanticsIgnoringOF",
+        "integerSimplificationRules" : "integerSimplificationRules:full",
+        "javaLoopTreatment" : "javaLoopTreatment:efficient",
+        "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off",
+        "methodExpansion" : "methodExpansion:modularOnly",
+        "modelFields" : "modelFields:showSatisfiability",
+        "moreSeqRules" : "moreSeqRules:on",
+        "optimisedSelectRules" : "optimisedSelectRules:on",
+        "permissions" : "permissions:off",
+        "programRules" : "programRules:Java",
+        "reach" : "reach:on",
+        "runtimeExceptions" : "runtimeExceptions:ban",
+        "sequences" : "sequences:on",
+        "soundDefaultContracts" : "soundDefaultContracts:on",
+        "wdChecks" : "wdChecks:off",
+        "wdOperator" : "wdOperator:L"
+     },
+    "Labels" : { 
+        "UseOriginLabels" : true
+     },
+    "NewSMT" : { 
+
+     },
+    "SMTSettings" : { 
+        "SelectedTaclets" : [ 
+
+         ],
+        "UseBuiltUniqueness" : false,
+        "explicitTypeHierarchy" : false,
+        "instantiateHierarchyAssumptions" : true,
+        "integersMaximum" : 2147483645,
+        "integersMinimum" : -2147483645,
+        "invariantForall" : false,
+        "maxGenericSorts" : 2,
+        "useConstantsForBigOrSmallIntegers" : true,
+        "useUninterpretedMultiplication" : true
+     },
+    "Strategy" : { 
+        "ActiveStrategy" : "JavaCardDLStrategy",
+        "MaximumNumberOfAutomaticApplications" : 500,
+        "Timeout" : -1,
+        "options" : { 
+            "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
+            "BLOCK_OPTIONS_KEY" : "BLOCK_EXPAND",
+            "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE",
+            "DEP_OPTIONS_KEY" : "DEP_OFF",
+            "INF_FLOW_CHECK_PROPERTY" : "INF_FLOW_CHECK_FALSE",
+            "LOOP_OPTIONS_KEY" : "LOOP_INVARIANT",
+            "METHOD_OPTIONS_KEY" : "METHOD_EXPAND",
+            "MPS_OPTIONS_KEY" : "MPS_MERGE",
+            "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS",
+            "OSS_OPTIONS_KEY" : "OSS_ON",
+            "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS",
+            "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_OFF",
+            "QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF",
+            "SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED",
+            "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT",
+            "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER",
+            "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF",
+            "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF",
+            "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF",
+            "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF",
+            "VBT_PHASE" : "VBT_SYM_EX"
+         }
+     }
+ } 
+
+\proofObligation 
+// Proof-Obligation settings
+{ 
+    "class" : "de.uka.ilkd.key.taclettranslation.lemma.TacletProofObligationInput",
+    "name" : "equalityOfSingleton"
+ }
+
+\proof {
+(keyLog "0" (keyUser "ulbrich" ) (keyVersion "af00212456641ec51f1d89b225061fe018faa149"))
+
+(autoModeTime "163")
+
+(branch "dummy ID"
+(rule "equalityToElementOf" (formula "1") (term "0") (inst "ov=ov") (inst "fv=fv") (userinteraction))
+(rule "eqSymm" (formula "1") (term "0,1"))
+(rule "eqSymm" (formula "1") (term "1,1"))
+(rule "elementOfSingleton" (formula "1") (term "1,0,0,0"))
+(rule "elementOfSingleton" (formula "1") (term "0,0,0,0"))
+(rule "commute_and" (formula "1") (term "1"))
+(rule "equiv_right" (formula "1"))
+(branch "Case '->'"
+   (rule "commute_and" (formula "1") (term "1,0,0"))
+   (rule "commute_and" (formula "1") (term "0,0,0"))
+   (rule "cnf_eqv" (formula "1") (term "0,0"))
+   (rule "nnf_notAnd" (formula "1") (term "1,0,0,0"))
+   (rule "nnf_notAnd" (formula "1") (term "0,1,0,0"))
+   (rule "distr_forallAnd" (formula "1") (term "0"))
+   (rule "distr_forallAnd" (formula "1"))
+   (rule "andLeft" (formula "1"))
+   (rule "commute_or" (formula "1") (term "0,0"))
+   (rule "commute_or" (formula "2") (term "0,0,0"))
+   (rule "commute_or" (formula "1") (term "0,0,0"))
+   (rule "cnf_rightDist" (formula "2") (term "0,0"))
+   (rule "distr_forallAnd" (formula "2") (term "0"))
+   (rule "distr_forallAnd" (formula "2"))
+   (rule "andLeft" (formula "2"))
+   (rule "commute_or_2" (formula "2") (term "0,0"))
+    (builtin "One Step Simplification" (formula "2"))
+   (rule "eqSymm" (formula "2") (term "1,0"))
+   (rule "commute_or" (formula "2") (term "0"))
+    (builtin "One Step Simplification" (formula "2"))
+   (rule "replace_known_left" (formula "4") (term "0") (ifseqformula "2"))
+    (builtin "One Step Simplification" (formula "4"))
+   (rule "applyEqRigid" (formula "1") (term "1,0,1,0,0,0") (ifseqformula "2"))
+   (rule "shift_paren_or" (formula "3") (term "0,0"))
+    (builtin "One Step Simplification" (formula "3"))
+   (rule "eqSymm" (formula "3"))
+   (rule "close" (formula "4") (ifseqformula "3"))
+)
+(branch "Case '<-'"
+   (rule "andLeft" (formula "1"))
+   (rule "allRight" (formula "3") (inst "sk=ov_0"))
+   (rule "allRight" (formula "3") (inst "sk=fv_0"))
+   (rule "applyEqRigid" (formula "3") (term "1,1,1") (ifseqformula "1"))
+   (rule "applyEqRigid" (formula "3") (term "1,0,1") (ifseqformula "2"))
+    (builtin "One Step Simplification" (formula "3"))
+   (rule "closeTrue" (formula "3"))
+)
+)
+}