diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/seqPerm.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/seqPerm.key
index a9d25fecf86..cdae1369ebb 100644
--- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/seqPerm.key
+++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/seqPerm.key
@@ -558,6 +558,30 @@
                 s1 = seqSwap(s2, iv, jv)))
     };
 
+    \lemma
+    seqSwapPreservesSeqPerm {
+        \schemaVar \term Seq s;
+        \schemaVar \term int x;
+        \schemaVar \term int y;
+
+        \find(==> seqPerm(s, seqSwap(s, x, y)))
+        \add( ==> 0 <= x & x < seqLen(s) & 0 <= y & y < seqLen(s))
+        \heuristics(simplify_enlarging)
+    };
+
+    \lemma
+    seqSwapPreservesSeqPermEQ {
+        \schemaVar \term Seq s;
+        \schemaVar \term Seq EQ;
+        \schemaVar \term int x;
+        \schemaVar \term int y;
+
+        \assumes (seqSwap(s, x, y) = EQ ==>)
+        \find(==> seqPerm(s, EQ))
+        \add( ==> 0 <= x & x < seqLen(s) & 0 <= y & y < seqLen(s))
+        \heuristics(simplify_enlarging)
+    };
+
     /* seqPermOrder {
      \schemaVar \term Seq commEqLeft, commEqRight;
      \find(seqPerm(commEqLeft, commEqRight))
diff --git a/key.core/tacletProofs/seqPerm/Taclet_seqSwapPreservesSeqPerm.proof b/key.core/tacletProofs/seqPerm/Taclet_seqSwapPreservesSeqPerm.proof
new file mode 100644
index 00000000000..92240d6e68e
--- /dev/null
+++ b/key.core/tacletProofs/seqPerm/Taclet_seqSwapPreservesSeqPerm.proof
@@ -0,0 +1,438 @@
+\profile "Java Profile";
+
+\settings // Proof-Settings-Config-File
+{ 
+    "Choice" : { 
+        "JavaCard" : "JavaCard:off",
+        "Strings" : "Strings:on",
+        "assertions" : "assertions:safe",
+        "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:treatAsAxiom",
+        "moreSeqRules" : "moreSeqRules:on",
+        "permissions" : "permissions:off",
+        "programRules" : "programRules:Java",
+        "reach" : "reach:on",
+        "runtimeExceptions" : "runtimeExceptions:ban",
+        "sequences" : "sequences:on",
+        "wdChecks" : "wdChecks:off",
+        "wdOperator" : "wdOperator:L"
+     }
+ } 
+
+\proofObligation // Proof-Obligation settings
+{ 
+    "class" : "de.uka.ilkd.key.taclettranslation.lemma.TacletProofObligationInput",
+    "name" : "seqSwapPreservesSeqPerm"
+ }
+
+\proof {
+(keyLog "0" (keyUser "wolfram" ) (keyVersion "c8b5d84c8b26505e96801636fd7dcce6a7f28f5e"))
+
+(autoModeTime "0")
+
+(branch "dummy ID"
+(rule "impRight" (formula "1") (newnames "f_x,f_s,f_y"))
+(rule "andLeft" (formula "1"))
+(rule "andLeft" (formula "1"))
+(rule "andLeft" (formula "1"))
+(rule "seqPermDef" (formula "5") (inst "s=s") (inst "iv=iv") (userinteraction))
+(rule "andRight" (formula "5") (userinteraction))
+(branch "Case 1"
+   (rule "eqSymm" (formula "5"))
+   (rule "lenOfSwap" (formula "5") (term "0"))
+    (builtin "One Step Simplification" (formula "5"))
+   (rule "closeTrue" (formula "5"))
+)
+(branch "Case 2"
+   (rule "exRight" (formula "5") (inst "t=seqDef{int u;}(Z(0(#)),
+               seqLen(f_s),
+               \\if (u = f_x)
+                   \\then (f_y)
+                   \\else (\\if (u = f_y)
+                              \\then (f_x)
+                              \\else (u)))") (userinteraction))
+   (rule "inEqSimp_ltToLeq" (formula "4"))
+   (rule "inEqSimp_commuteLeq" (formula "1"))
+   (rule "inEqSimp_commuteLeq" (formula "3"))
+   (rule "inEqSimp_ltToLeq" (formula "2"))
+   (rule "polySimp_mulComm0" (formula "2") (term "1,0,0"))
+   (rule "polySimp_mulComm0" (formula "4") (term "1,0,0"))
+   (rule "polySimp_addComm1" (formula "4") (term "0"))
+   (rule "polySimp_addComm1" (formula "2") (term "0"))
+   (rule "inEqSimp_sepNegMonomial0" (formula "2"))
+   (rule "inEqSimp_sepNegMonomial0" (formula "4"))
+   (rule "polySimp_mulLiterals" (formula "2") (term "0"))
+   (rule "polySimp_mulLiterals" (formula "4") (term "0"))
+   (rule "polySimp_elimOne" (formula "2") (term "0"))
+   (rule "polySimp_elimOne" (formula "4") (term "0"))
+   (rule "andRight" (formula "5") (userinteraction))
+   (branch "Case 1"
+      (rule "andRight" (formula "5") (userinteraction))
+      (branch "Case 1"
+         (rule "lenOfSeqDef" (formula "5") (term "0"))
+         (rule "polySimp_elimSub" (formula "5") (term "1,0"))
+         (rule "mul_literals" (formula "5") (term "1,1,0"))
+         (rule "add_zero_right" (formula "5") (term "1,0"))
+          (builtin "One Step Simplification" (formula "5"))
+         (rule "orRight" (formula "5"))
+         (rule "eqSymm" (formula "6"))
+         (rule "inEqSimp_ltRight" (formula "5"))
+         (rule "add_zero_right" (formula "1") (term "0"))
+         (rule "polySimp_mulComm0" (formula "1") (term "0"))
+         (rule "inEqSimp_invertInEq1" (formula "1"))
+         (rule "polySimp_mulLiterals" (formula "1") (term "0"))
+         (rule "mul_literals" (formula "1") (term "1"))
+         (rule "polySimp_elimOne" (formula "1") (term "0"))
+         (rule "inEqSimp_strengthen0" (formula "1") (ifseqformula "6"))
+         (rule "add_zero_right" (formula "1") (term "1"))
+         (rule "inEqSimp_exactShadow3" (formula "5") (ifseqformula "1"))
+         (rule "polySimp_rightDist" (formula "5") (term "0,0"))
+         (rule "mul_literals" (formula "5") (term "0,0,0"))
+         (rule "polySimp_addComm1" (formula "5") (term "0"))
+         (rule "add_literals" (formula "5") (term "0,0"))
+         (rule "inEqSimp_sepNegMonomial1" (formula "5"))
+         (rule "polySimp_mulLiterals" (formula "5") (term "0"))
+         (rule "polySimp_elimOne" (formula "5") (term "0"))
+         (rule "inEqSimp_contradInEq1" (formula "5") (ifseqformula "4"))
+         (rule "qeq_literals" (formula "5") (term "0"))
+          (builtin "One Step Simplification" (formula "5"))
+         (rule "closeFalse" (formula "5"))
+      )
+      (branch "Case 2"
+         (rule "seqNPermDefReplace" (formula "5") (inst "iv=iv") (inst "jv=jv") (userinteraction))
+         (rule "allRight" (formula "5") (inst "sk=iv_0"))
+         (rule "impRight" (formula "5"))
+         (rule "andLeft" (formula "1"))
+         (rule "getOfSeqDef" (formula "7") (term "0,1,0"))
+         (rule "castDel" (formula "7") (term "2,0,1,0"))
+         (rule "castDel" (formula "7") (term "1,0,1,0"))
+         (rule "add_zero_right" (formula "7") (term "0,0,1,0,1,0"))
+         (rule "add_zero_right" (formula "7") (term "0,0,2,1,0,1,0"))
+         (rule "add_zero_right" (formula "7") (term "2,2,1,0,1,0"))
+         (rule "polySimp_elimSub" (formula "7") (term "1,1,0,0,1,0"))
+         (rule "times_zero_2" (formula "7") (term "1,1,1,0,0,1,0"))
+         (rule "add_zero_right" (formula "7") (term "1,1,0,0,1,0"))
+         (rule "lenOfSeqDef" (formula "7") (term "1,1,0,0"))
+         (rule "polySimp_elimSub" (formula "7") (term "1,1,1,0,0"))
+         (rule "times_zero_2" (formula "7") (term "1,1,1,1,0,0"))
+         (rule "add_zero_right" (formula "7") (term "1,1,1,0,0"))
+         (rule "lenOfSeqDef" (formula "2") (term "1"))
+         (rule "polySimp_elimSub" (formula "2") (term "1,1"))
+         (rule "mul_literals" (formula "2") (term "1,1,1"))
+         (rule "add_zero_right" (formula "2") (term "1,1"))
+         (rule "inEqSimp_ltToLeq" (formula "7") (term "1,0,0,1,0"))
+         (rule "polySimp_mulComm0" (formula "7") (term "1,0,0,1,0,0,1,0"))
+         (rule "inEqSimp_ltToLeq" (formula "7") (term "0,1,1,0,0"))
+         (rule "add_zero_right" (formula "7") (term "0,0,1,1,0,0"))
+         (rule "polySimp_mulComm0" (formula "7") (term "1,0,0,1,1,0,0"))
+         (rule "inEqSimp_ltToLeq" (formula "2") (term "0,1"))
+         (rule "add_zero_right" (formula "2") (term "0,0,1"))
+         (rule "polySimp_mulComm0" (formula "2") (term "1,0,0,1"))
+         (rule "inEqSimp_ltToLeq" (formula "7") (term "1,0,0"))
+         (rule "polySimp_mulComm0" (formula "7") (term "1,0,0,1,0,0"))
+         (rule "inEqSimp_ltToLeq" (formula "2"))
+         (rule "polySimp_mulComm0" (formula "2") (term "1,0,0"))
+         (rule "polySimp_addComm1" (formula "2") (term "0"))
+         (rule "inEqSimp_commuteLeq" (formula "7") (term "0,0,0"))
+         (rule "inEqSimp_commuteLeq" (formula "1"))
+         (rule "inEqSimp_commuteLeq" (formula "7") (term "0,0,0,1,0"))
+         (rule "inEqSimp_sepPosMonomial0" (formula "7") (term "1,0,0,1,0"))
+         (rule "polySimp_mulComm0" (formula "7") (term "1,1,0,0,1,0"))
+         (rule "polySimp_rightDist" (formula "7") (term "1,1,0,0,1,0"))
+         (rule "polySimp_mulLiterals" (formula "7") (term "1,1,1,0,0,1,0"))
+         (rule "mul_literals" (formula "7") (term "0,1,1,0,0,1,0"))
+         (rule "polySimp_elimOne" (formula "7") (term "1,1,1,0,0,1,0"))
+         (rule "inEqSimp_sepPosMonomial0" (formula "7") (term "1,0,0"))
+         (rule "polySimp_mulComm0" (formula "7") (term "1,1,0,0"))
+         (rule "polySimp_rightDist" (formula "7") (term "1,1,0,0"))
+         (rule "polySimp_mulLiterals" (formula "7") (term "1,1,1,0,0"))
+         (rule "mul_literals" (formula "7") (term "0,1,1,0,0"))
+         (rule "polySimp_elimOne" (formula "7") (term "1,1,1,0,0"))
+         (rule "inEqSimp_sepNegMonomial0" (formula "2") (term "0,0,1,0"))
+         (rule "polySimp_mulLiterals" (formula "2") (term "0,0,0,1,0"))
+         (rule "polySimp_elimOne" (formula "2") (term "0,0,0,1,0"))
+         (rule "inEqSimp_sepNegMonomial0" (formula "7") (term "0,1,1,1,0,0"))
+         (rule "polySimp_mulLiterals" (formula "7") (term "0,0,1,1,1,0,0"))
+         (rule "polySimp_elimOne" (formula "7") (term "0,0,1,1,1,0,0"))
+         (rule "inEqSimp_sepNegMonomial0" (formula "2"))
+         (rule "polySimp_mulLiterals" (formula "2") (term "0"))
+         (rule "polySimp_elimOne" (formula "2") (term "0"))
+         (rule "nnf_ex2all" (formula "7"))
+         (rule "nnf_notAnd" (formula "1") (term "0"))
+         (rule "nnf_notAnd" (formula "1") (term "0,0"))
+         (rule "inEqSimp_notLeq" (formula "1") (term "1,0,0"))
+         (rule "polySimp_rightDist" (formula "1") (term "1,0,0,1,0,0"))
+         (rule "mul_literals" (formula "1") (term "0,1,0,0,1,0,0"))
+         (rule "polySimp_addAssoc" (formula "1") (term "0,0,1,0,0"))
+         (rule "add_literals" (formula "1") (term "0,0,0,1,0,0"))
+         (rule "add_zero_left" (formula "1") (term "0,0,1,0,0"))
+         (rule "inEqSimp_sepPosMonomial1" (formula "1") (term "1,0,0"))
+         (rule "polySimp_mulLiterals" (formula "1") (term "1,1,0,0"))
+         (rule "polySimp_elimOne" (formula "1") (term "1,1,0,0"))
+         (rule "inEqSimp_notGeq" (formula "1") (term "0,0,0"))
+         (rule "mul_literals" (formula "1") (term "1,0,0,0,0,0"))
+         (rule "add_zero_right" (formula "1") (term "0,0,0,0,0"))
+         (rule "inEqSimp_sepPosMonomial0" (formula "1") (term "0,0,0"))
+         (rule "mul_literals" (formula "1") (term "1,0,0,0"))
+         (rule "commute_or_2" (formula "1") (term "0"))
+         (rule "commute_or" (formula "1") (term "0,0"))
+         (rule "ifthenelse_to_or_left2" (formula "1") (term "0,0,0"))
+         (rule "nnf_notAnd" (formula "1") (term "0,0,0,0,0"))
+         (rule "inEqSimp_notGeq" (formula "1") (term "0,0,0,0,0,0"))
+         (rule "times_zero_1" (formula "1") (term "1,0,0,0,0,0,0,0,0"))
+         (rule "add_zero_right" (formula "1") (term "0,0,0,0,0,0,0,0"))
+         (rule "inEqSimp_sepPosMonomial0" (formula "1") (term "0,0,0,0,0,0"))
+         (rule "mul_literals" (formula "1") (term "1,0,0,0,0,0,0"))
+         (rule "inEqSimp_notLeq" (formula "1") (term "1,0,0,0,0,0"))
+         (rule "polySimp_rightDist" (formula "1") (term "1,0,0,1,0,0,0,0,0"))
+         (rule "mul_literals" (formula "1") (term "0,1,0,0,1,0,0,0,0,0"))
+         (rule "polySimp_addAssoc" (formula "1") (term "0,0,1,0,0,0,0,0"))
+         (rule "add_literals" (formula "1") (term "0,0,0,1,0,0,0,0,0"))
+         (rule "add_zero_left" (formula "1") (term "0,0,1,0,0,0,0,0"))
+         (rule "inEqSimp_sepPosMonomial1" (formula "1") (term "1,0,0,0,0,0"))
+         (rule "polySimp_mulLiterals" (formula "1") (term "1,1,0,0,0,0,0"))
+         (rule "polySimp_elimOne" (formula "1") (term "1,1,0,0,0,0,0"))
+         (rule "commute_or" (formula "1") (term "0,0"))
+         (rule "commute_or_2" (formula "1") (term "0"))
+         (rule "commute_or" (formula "1") (term "1,1,0"))
+         (rule "cnf_rightDist" (formula "1") (term "1,1,0"))
+         (rule "cnf_rightDist" (formula "1") (term "0"))
+         (rule "distr_forallAnd" (formula "1"))
+         (rule "andLeft" (formula "1"))
+         (rule "shift_paren_or" (formula "1") (term "0"))
+         (rule "commute_or_2" (formula "1") (term "0,0"))
+         (rule "shift_paren_or" (formula "1") (term "0,0,0"))
+          (builtin "One Step Simplification" (formula "1"))
+         (rule "ifthenelse_to_or_left2" (formula "1") (term "1,0"))
+         (rule "eqSymm" (formula "1") (term "0,1,0,1,0"))
+         (rule "cnf_rightDist" (formula "1") (term "0"))
+         (rule "distr_forallAnd" (formula "1"))
+         (rule "andLeft" (formula "1"))
+         (rule "commute_or_2" (formula "2") (term "0"))
+         (rule "shift_paren_or" (formula "1") (term "0"))
+         (rule "commute_or_2" (formula "1") (term "0"))
+          (builtin "One Step Simplification" (formula "1"))
+         (rule "inEqSimp_commuteGeq" (formula "1") (term "1,0,0"))
+         (rule "inEqSimp_commuteGeq" (formula "1") (term "1,0"))
+         (rule "inEqSimp_contradInEq1" (formula "1") (term "1,0,0") (ifseqformula "7"))
+         (rule "inEqSimp_homoInEq1" (formula "1") (term "0,1,0,0"))
+         (rule "polySimp_pullOutFactor1b" (formula "1") (term "0,0,1,0,0"))
+         (rule "add_literals" (formula "1") (term "1,1,0,0,1,0,0"))
+         (rule "times_zero_1" (formula "1") (term "1,0,0,1,0,0"))
+         (rule "add_zero_right" (formula "1") (term "0,0,1,0,0"))
+         (rule "leq_literals" (formula "1") (term "0,1,0,0"))
+          (builtin "One Step Simplification" (formula "1"))
+         (rule "inEqSimp_contradInEq1" (formula "1") (term "0,0") (ifseqformula "6"))
+         (rule "qeq_literals" (formula "1") (term "0,0,0"))
+          (builtin "One Step Simplification" (formula "1"))
+         (rule "commute_or" (formula "1"))
+         (rule "shift_paren_or" (formula "2") (term "0,0"))
+         (rule "shift_paren_or" (formula "2") (term "0,0,0"))
+         (rule "commute_or" (formula "2") (term "0,0,0,0"))
+         (rule "ifthenelse_to_or_left2" (formula "2") (term "1,0"))
+         (rule "eqSymm" (formula "2") (term "0,1,0,1,0"))
+         (rule "commute_or" (formula "2") (term "0,1,0"))
+         (rule "cnf_rightDist" (formula "2") (term "0"))
+         (rule "distr_forallAnd" (formula "2"))
+         (rule "andLeft" (formula "2"))
+         (rule "commute_or_2" (formula "3") (term "0"))
+          (builtin "One Step Simplification" (formula "3"))
+         (rule "inEqSimp_commuteGeq" (formula "3") (term "1,1"))
+         (rule "inEqSimp_commuteGeq" (formula "3") (term "1,0,1"))
+         (rule "inEqSimp_contradInEq1" (formula "3") (term "1,1") (ifseqformula "6"))
+         (rule "inEqSimp_homoInEq1" (formula "3") (term "0,1,1"))
+         (rule "polySimp_pullOutFactor1b" (formula "3") (term "0,0,1,1"))
+         (rule "add_literals" (formula "3") (term "1,1,0,0,1,1"))
+         (rule "times_zero_1" (formula "3") (term "1,0,0,1,1"))
+         (rule "add_literals" (formula "3") (term "0,0,1,1"))
+         (rule "leq_literals" (formula "3") (term "0,1,1"))
+          (builtin "One Step Simplification" (formula "3"))
+         (rule "inEqSimp_contradInEq1" (formula "3") (term "0,0,1") (ifseqformula "5"))
+         (rule "qeq_literals" (formula "3") (term "0,0,0,1"))
+          (builtin "One Step Simplification" (formula "3"))
+         (rule "shift_paren_or" (formula "3"))
+         (rule "commute_or" (formula "3") (term "0"))
+         (rule "shift_paren_or" (formula "2") (term "0"))
+          (builtin "One Step Simplification" (formula "2"))
+         (rule "inEqSimp_commuteGeq" (formula "2") (term "1,0"))
+         (rule "inEqSimp_commuteGeq" (formula "2") (term "1,0,0"))
+         (rule "inEqSimp_contradInEq1" (formula "2") (term "0,0,0,0") (ifseqformula "9"))
+         (rule "qeq_literals" (formula "2") (term "0,0,0,0,0"))
+          (builtin "One Step Simplification" (formula "2"))
+         (rule "inEqSimp_contradInEq1" (formula "2") (term "1,0,0") (ifseqformula "10"))
+         (rule "inEqSimp_homoInEq1" (formula "2") (term "0,1,0,0"))
+         (rule "polySimp_pullOutFactor1b" (formula "2") (term "0,0,1,0,0"))
+         (rule "add_literals" (formula "2") (term "1,1,0,0,1,0,0"))
+         (rule "times_zero_1" (formula "2") (term "1,0,0,1,0,0"))
+         (rule "add_zero_right" (formula "2") (term "0,0,1,0,0"))
+         (rule "leq_literals" (formula "2") (term "0,1,0,0"))
+          (builtin "One Step Simplification" (formula "2"))
+         (rule "commute_or_2" (formula "2"))
+         (rule "ifthenelse_split" (formula "6") (term "0"))
+         (branch "f_s.length ≥ 1 TRUE"
+            (rule "replace_known_left" (formula "1") (term "0,0,1") (ifseqformula "6"))
+             (builtin "One Step Simplification" (formula "1"))
+            (rule "replace_known_left" (formula "2") (term "0,0,1") (ifseqformula "6"))
+             (builtin "One Step Simplification" (formula "2"))
+            (rule "inEqSimp_contradInEq1" (formula "1") (term "1") (ifseqformula "9"))
+            (rule "inEqSimp_homoInEq1" (formula "1") (term "0,1"))
+            (rule "polySimp_pullOutFactor1b" (formula "1") (term "0,0,1"))
+            (rule "add_literals" (formula "1") (term "1,1,0,0,1"))
+            (rule "times_zero_1" (formula "1") (term "1,0,0,1"))
+            (rule "add_zero_right" (formula "1") (term "0,0,1"))
+            (rule "leq_literals" (formula "1") (term "0,1"))
+             (builtin "One Step Simplification" (formula "1"))
+            (rule "notLeft" (formula "1"))
+            (rule "replace_known_right" (formula "2") (term "1,0") (ifseqformula "11"))
+             (builtin "One Step Simplification" (formula "2"))
+            (rule "inEqSimp_contradInEq1" (formula "1") (term "1") (ifseqformula "10"))
+            (rule "inEqSimp_homoInEq1" (formula "1") (term "0,1"))
+            (rule "polySimp_pullOutFactor1b" (formula "1") (term "0,0,1"))
+            (rule "add_literals" (formula "1") (term "1,1,0,0,1"))
+            (rule "times_zero_1" (formula "1") (term "1,0,0,1"))
+            (rule "add_zero_right" (formula "1") (term "0,0,1"))
+            (rule "leq_literals" (formula "1") (term "0,1"))
+             (builtin "One Step Simplification" (formula "1"))
+            (rule "inEqSimp_contradInEq1" (formula "2") (term "1") (ifseqformula "6"))
+            (rule "inEqSimp_homoInEq1" (formula "2") (term "0,1"))
+            (rule "polySimp_pullOutFactor1b" (formula "2") (term "0,0,1"))
+            (rule "add_literals" (formula "2") (term "1,1,0,0,1"))
+            (rule "times_zero_1" (formula "2") (term "1,0,0,1"))
+            (rule "add_zero_right" (formula "2") (term "0,0,1"))
+            (rule "leq_literals" (formula "2") (term "0,1"))
+             (builtin "One Step Simplification" (formula "2"))
+            (rule "replace_known_left" (formula "1") (term "0,1") (ifseqformula "2"))
+             (builtin "One Step Simplification" (formula "1"))
+            (rule "applyEq" (formula "11") (term "0") (ifseqformula "2"))
+            (rule "eqSymm" (formula "11"))
+            (rule "close" (formula "11") (ifseqformula "1"))
+         )
+         (branch "f_s.length ≥ 1 FALSE"
+            (rule "inEqSimp_homoInEq1" (formula "6"))
+            (rule "times_zero_2" (formula "6") (term "1,0"))
+            (rule "add_zero_right" (formula "6") (term "0"))
+            (rule "inEqSimp_sepPosMonomial0" (formula "6"))
+            (rule "mul_literals" (formula "6") (term "1"))
+            (rule "inEqSimp_contradInEq1" (formula "6") (ifseqformula "5"))
+            (rule "qeq_literals" (formula "6") (term "0"))
+             (builtin "One Step Simplification" (formula "6"))
+            (rule "closeFalse" (formula "6"))
+         )
+      )
+   )
+   (branch "Case 2"
+      (rule "lenOfSeqDef" (formula "5") (term "1,1,0,0") (userinteraction))
+      (rule "allRight" (formula "5") (inst "sk=iv_0") (userinteraction))
+      (rule "impRight" (formula "5") (userinteraction))
+      (rule "andLeft" (formula "1"))
+      (rule "eqSymm" (formula "7"))
+      (rule "polySimp_elimSub" (formula "2") (term "1,1"))
+      (rule "times_zero_2" (formula "2") (term "1,1,1"))
+      (rule "add_zero_right" (formula "2") (term "1,1"))
+      (rule "getOfSeqDef" (formula "7") (term "1,0"))
+      (rule "castDel" (formula "7") (term "1,1,0"))
+      (rule "add_zero_right" (formula "7") (term "0,0,1,1,0"))
+      (rule "add_zero_right" (formula "7") (term "2,2,1,1,0"))
+      (rule "add_zero_right" (formula "7") (term "0,0,2,1,1,0"))
+      (rule "replace_known_left" (formula "7") (term "0,0,1,0") (ifseqformula "1"))
+       (builtin "One Step Simplification" (formula "7"))
+      (rule "polySimp_elimSub" (formula "7") (term "1,0,1,0"))
+      (rule "mul_literals" (formula "7") (term "1,1,0,1,0"))
+      (rule "add_zero_right" (formula "7") (term "1,0,1,0"))
+      (rule "inEqSimp_ltToLeq" (formula "2") (term "0,1"))
+      (rule "add_zero_right" (formula "2") (term "0,0,1"))
+      (rule "polySimp_mulComm0" (formula "2") (term "1,0,0,1"))
+      (rule "inEqSimp_ltToLeq" (formula "7") (term "0,1,0"))
+      (rule "polySimp_mulComm0" (formula "7") (term "1,0,0,0,1,0"))
+      (rule "polySimp_addComm1" (formula "7") (term "0,0,1,0"))
+      (rule "inEqSimp_ltToLeq" (formula "2"))
+      (rule "polySimp_mulComm0" (formula "2") (term "1,0,0"))
+      (rule "polySimp_addComm1" (formula "2") (term "0"))
+      (rule "inEqSimp_commuteLeq" (formula "1"))
+      (rule "inEqSimp_sepNegMonomial0" (formula "7") (term "0,1,0"))
+      (rule "polySimp_mulLiterals" (formula "7") (term "0,0,1,0"))
+      (rule "polySimp_elimOne" (formula "7") (term "0,0,1,0"))
+      (rule "inEqSimp_sepNegMonomial0" (formula "2"))
+      (rule "polySimp_mulLiterals" (formula "2") (term "0"))
+      (rule "polySimp_elimOne" (formula "2") (term "0"))
+      (rule "inEqSimp_sepNegMonomial0" (formula "2") (term "0,0"))
+      (rule "polySimp_mulLiterals" (formula "2") (term "0,0,0"))
+      (rule "polySimp_elimOne" (formula "2") (term "0,0,0"))
+      (rule "getOfSwap" (formula "7") (term "0"))
+      (rule "ifthenelse_negated" (formula "7") (term "0"))
+      (rule "inEqSimp_ltToLeq" (formula "7") (term "1,0,0"))
+      (rule "polySimp_mulComm0" (formula "7") (term "1,0,0,1,0,0"))
+      (rule "polySimp_addComm1" (formula "7") (term "0,1,0,0"))
+      (rule "inEqSimp_ltToLeq" (formula "7") (term "1,0,0,0"))
+      (rule "polySimp_mulComm0" (formula "7") (term "1,0,0,1,0,0,0"))
+      (rule "polySimp_addComm1" (formula "7") (term "0,1,0,0,0"))
+      (rule "inEqSimp_commuteLeq" (formula "7") (term "0,0,0,0,0"))
+      (rule "replace_known_left" (formula "7") (term "0,0,0,0,0") (ifseqformula "3"))
+       (builtin "One Step Simplification" (formula "7"))
+      (rule "inEqSimp_commuteLeq" (formula "7") (term "0,0,0,0"))
+      (rule "replace_known_left" (formula "7") (term "0,0,0,0") (ifseqformula "5"))
+       (builtin "One Step Simplification" (formula "7"))
+      (rule "inEqSimp_sepNegMonomial0" (formula "7") (term "0,0,0"))
+      (rule "polySimp_mulLiterals" (formula "7") (term "0,0,0,0"))
+      (rule "polySimp_elimOne" (formula "7") (term "0,0,0,0"))
+      (rule "replace_known_left" (formula "7") (term "0,0,0") (ifseqformula "4"))
+       (builtin "One Step Simplification" (formula "7"))
+      (rule "inEqSimp_sepNegMonomial0" (formula "7") (term "0,0"))
+      (rule "polySimp_mulLiterals" (formula "7") (term "0,0,0"))
+      (rule "polySimp_elimOne" (formula "7") (term "0,0,0"))
+      (rule "replace_known_left" (formula "7") (term "0,0") (ifseqformula "6"))
+       (builtin "One Step Simplification" (formula "7"))
+      (rule "ifthenelse_split" (formula "2") (term "0"))
+      (branch "f_s.length ≥ 1 TRUE"
+         (rule "replace_known_left" (formula "8") (term "0,1,2,2,0") (ifseqformula "3"))
+          (builtin "One Step Simplification" (formula "8") (ifInst ""  (formula "3")) (ifInst ""  (formula "3")))
+         (rule "ifthenelse_split" (formula "8") (term "0,0,0"))
+         (branch "iv_0 = f_x TRUE"
+            (rule "replace_known_left" (formula "9") (term "0,0,2,0") (ifseqformula "1"))
+             (builtin "One Step Simplification" (formula "9") (ifInst ""  (formula "1")))
+            (rule "applyEqRigid" (formula "9") (term "1,1") (ifseqformula "1"))
+             (builtin "One Step Simplification" (formula "9"))
+            (rule "orRight" (formula "9"))
+            (rule "notRight" (formula "9"))
+            (rule "applyEqRigid" (formula "10") (term "1,0") (ifseqformula "1"))
+             (builtin "One Step Simplification" (formula "10"))
+            (rule "closeTrue" (formula "10"))
+         )
+         (branch "iv_0 = f_x FALSE"
+             (builtin "One Step Simplification" (formula "9") (ifInst ""  (formula "8")) (ifInst ""  (formula "8")) (ifInst ""  (formula "8")))
+            (rule "ifthenelse_split" (formula "9") (term "0"))
+            (branch "iv_0 = f_y TRUE"
+               (rule "eqSymm" (formula "10"))
+               (rule "applyEq" (formula "10") (term "1,0") (ifseqformula "1"))
+                (builtin "One Step Simplification" (formula "10"))
+               (rule "closeTrue" (formula "10"))
+            )
+            (branch "iv_0 = f_y FALSE"
+               (rule "replace_known_right" (formula "10") (term "0,1,2,0") (ifseqformula "9"))
+                (builtin "One Step Simplification" (formula "10") (ifInst ""  (formula "9")) (ifInst ""  (formula "9")))
+               (rule "closeTrue" (formula "10"))
+            )
+         )
+      )
+      (branch "f_s.length ≥ 1 FALSE"
+         (rule "inEqSimp_homoInEq1" (formula "2"))
+         (rule "times_zero_2" (formula "2") (term "1,0"))
+         (rule "add_zero_right" (formula "2") (term "0"))
+         (rule "inEqSimp_sepPosMonomial0" (formula "2"))
+         (rule "mul_literals" (formula "2") (term "1"))
+         (rule "inEqSimp_contradInEq0" (formula "1") (ifseqformula "2"))
+         (rule "qeq_literals" (formula "1") (term "0"))
+          (builtin "One Step Simplification" (formula "1"))
+         (rule "closeFalse" (formula "1"))
+      )
+   )
+)
+)
+}
diff --git a/key.core/tacletProofs/seqPerm/Taclet_seqSwapPreservesSeqPermEQ.proof b/key.core/tacletProofs/seqPerm/Taclet_seqSwapPreservesSeqPermEQ.proof
new file mode 100644
index 00000000000..6c84c81372b
--- /dev/null
+++ b/key.core/tacletProofs/seqPerm/Taclet_seqSwapPreservesSeqPermEQ.proof
@@ -0,0 +1,53 @@
+\profile "Java Profile";
+
+\settings // Proof-Settings-Config-File
+{ 
+    "Choice" : { 
+        "JavaCard" : "JavaCard:off",
+        "Strings" : "Strings:on",
+        "assertions" : "assertions:safe",
+        "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:treatAsAxiom",
+        "moreSeqRules" : "moreSeqRules:on",
+        "permissions" : "permissions:off",
+        "programRules" : "programRules:Java",
+        "reach" : "reach:on",
+        "runtimeExceptions" : "runtimeExceptions:ban",
+        "sequences" : "sequences:on",
+        "wdChecks" : "wdChecks:off",
+        "wdOperator" : "wdOperator:L"
+     }
+ } 
+
+\proofObligation // Proof-Obligation settings
+{ 
+    "class" : "de.uka.ilkd.key.taclettranslation.lemma.TacletProofObligationInput",
+    "name" : "seqSwapPreservesSeqPermEQ"
+ }
+
+\proof {
+(keyLog "0" (keyUser "wolfram" ) (keyVersion "c8b5d84c8b26505e96801636fd7dcce6a7f28f5e"))
+
+(autoModeTime "271")
+
+(branch "dummy ID"
+(rule "impRight" (formula "1") (newnames "f_x,f_s,f_y,f_EQ"))
+(rule "orRight" (formula "2"))
+(rule "andLeft" (formula "1"))
+(rule "notRight" (formula "4"))
+(rule "andLeft" (formula "2"))
+(rule "andLeft" (formula "2"))
+(rule "applyEqReverse" (formula "6") (term "1") (ifseqformula "1") (userinteraction))
+(rule "seqSwapPreservesSeqPerm" (formula "6") (userinteraction))
+(rule "replace_known_left" (formula "6") (term "1") (ifseqformula "5"))
+ (builtin "One Step Simplification" (formula "6") (ifInst ""  (formula "2")) (ifInst ""  (formula "3")) (ifInst ""  (formula "4")))
+(rule "closeTrue" (formula "6"))
+)
+}