---

Step * of Lemma permutation-when-no_repeats

No Annotations
∀[T:Type]
  ∀sa,sb:T List.  ((∀x:T. ((x ∈ sa) ⇐⇒ (x ∈ sb))) ⇒ no_repeats(T;sb) ⇒ no_repeats(T;sa) ⇒ permutation(T;sb;sa))
BY
{ (Auto
   THEN (Assert ∀i:ℕ||sa||. ∃j:ℕ||sb||. (sa[i] = sb[j] ∈ T) BY
               (Auto
                THEN (InstHyp [⌜sa[i]⌝] (-4)⋅ THEN Auto)
                THEN (D -1 THENA (BHyp (-1) THEN Auto))
                THEN ThinTrivial
                THEN (D -1 THEN RenameVar `j' (-2) THEN D -1 THEN With ⌜j⌝ (D 0)⋅ THEN Auto)⋅))
   ) }

1
1. [T] : Type
2. sa : T List
3. sb : T List
4. ∀x:T. ((x ∈ sa) ⇐⇒ (x ∈ sb))
5. no_repeats(T;sb)
6. no_repeats(T;sa)
7. ∀i:ℕ||sa||. ∃j:ℕ||sb||. (sa[i] = sb[j] ∈ T)
⊢ permutation(T;sb;sa)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type]
    \mforall{}sa,sb:T  List.
        ((\mforall{}x:T.  ((x  \mmember{}  sa)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  sb)))
        {}\mRightarrow{}  no\_repeats(T;sb)
        {}\mRightarrow{}  no\_repeats(T;sa)
        {}\mRightarrow{}  permutation(T;sb;sa))


By

---

Latex:
(Auto
  THEN  (Assert  \mforall{}i:\mBbbN{}||sa||.  \mexists{}j:\mBbbN{}||sb||.  (sa[i]  =  sb[j])  BY
                          (Auto
                            THEN  (InstHyp  [\mkleeneopen{}sa[i]\mkleeneclose{}]  (-4)\mcdot{}  THEN  Auto)
                            THEN  (D  -1  THENA  (BHyp  (-1)  THEN  Auto))
                            THEN  ThinTrivial
                            THEN  (D  -1  THEN  RenameVar  `j'  (-2)  THEN  D  -1  THEN  With  \mkleeneopen{}j\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)\mcdot{}))
  )

---

Home Index