---

Step * of Lemma permutation-last

∀[A:Type]
  ∀x:A. ∀L1,L2:A List.
    (permutation(A;L1 @ [x];L2) ⇐⇒ ∃as,bs:A List. ((L2 = (as @ [x / bs]) ∈ (A List)) ∧ permutation(A;L1;as @ bs)))
BY
{ (Auto
   THEN ExRepD
   THEN Try (Complete (((RWO "permutation-rotate" (-1) THENA Auto)
                        THEN Reduce (-1)
                        THEN (RWO "permutation-cons" (-1) THENA Auto)
                        THEN Auto)))
   THEN Try (Complete (((RWO "-2" 0 THENA Auto)
                        THEN ThinVar `L2'
                        THEN (RWO "permutation-rotate" 0 THENA Auto)
                        THEN Reduce 0
                        THEN BLemma `permutation-cons2`
                        THEN Auto
                        THEN RWO "permutation-rotate" 0
                        THEN Auto)))) }

---

Latex:

---

Latex:
\mforall{}[A:Type]
    \mforall{}x:A.  \mforall{}L1,L2:A  List.
        (permutation(A;L1  @  [x];L2)
        \mLeftarrow{}{}\mRightarrow{}  \mexists{}as,bs:A  List.  ((L2  =  (as  @  [x  /  bs]))  \mwedge{}  permutation(A;L1;as  @  bs)))


By

---

Latex:
(Auto
  THEN  ExRepD
  THEN  Try  (Complete  (((RWO  "permutation-rotate"  (-1)  THENA  Auto)
                                            THEN  Reduce  (-1)
                                            THEN  (RWO  "permutation-cons"  (-1)  THENA  Auto)
                                            THEN  Auto)))
  THEN  Try  (Complete  (((RWO  "-2"  0  THENA  Auto)
                                            THEN  ThinVar  `L2'
                                            THEN  (RWO  "permutation-rotate"  0  THENA  Auto)
                                            THEN  Reduce  0
                                            THEN  BLemma  `permutation-cons2`
                                            THEN  Auto
                                            THEN  RWO  "permutation-rotate"  0
                                            THEN  Auto))))

---

Home Index