---

Step * 1 1 1 2 of Lemma permutation-when-no_repeats


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)
8. f : i:ℕ||sa|| ⟶ ℕ||sb||
9. ∀i:ℕ||sa||. (sa[i] = sb[f i] ∈ T)
10. ||sa|| ≤ ||sb||
⊢ ||sa|| = ||sb|| ∈ ℤ
BY
{ (Assert ∀i:ℕ||sb||. ∃j:ℕ||sa||. (sb[i] = sa[j] ∈ T) BY
         (Auto
          THEN (InstHyp [⌜sb[i]⌝] 4⋅ THEN Auto)
          THEN (D (-1) THENA Auto)
          THEN Unfold `l_member` -1
          THEN ParallelLast
          THEN D (-1)
          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)
8. f : i:ℕ||sa|| ⟶ ℕ||sb||
9. ∀i:ℕ||sa||. (sa[i] = sb[f i] ∈ T)
10. ||sa|| ≤ ||sb||
11. ∀i:ℕ||sb||. ∃j:ℕ||sa||. (sb[i] = sa[j] ∈ T)
⊢ ||sa|| = ||sb|| ∈ ℤ

---

Latex:

---

Latex:

1.  T  :  Type
2.  sa  :  T  List
3.  sb  :  T  List
4.  \mforall{}x:T.  ((x  \mmember{}  sa)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  sb))
5.  no\_repeats(T;sb)
6.  no\_repeats(T;sa)
7.  \mforall{}i:\mBbbN{}||sa||.  \mexists{}j:\mBbbN{}||sb||.  (sa[i]  =  sb[j])
8.  f  :  i:\mBbbN{}||sa||  {}\mrightarrow{}  \mBbbN{}||sb||
9.  \mforall{}i:\mBbbN{}||sa||.  (sa[i]  =  sb[f  i])
10.  ||sa||  \mleq{}  ||sb||
\mvdash{}  ||sa||  =  ||sb||


By

---

Latex:
(Assert  \mforall{}i:\mBbbN{}||sb||.  \mexists{}j:\mBbbN{}||sa||.  (sb[i]  =  sa[j])  BY
              (Auto
                THEN  (InstHyp  [\mkleeneopen{}sb[i]\mkleeneclose{}]  4\mcdot{}  THEN  Auto)
                THEN  (D  (-1)  THENA  Auto)
                THEN  Unfold  `l\_member`  -1
                THEN  ParallelLast
                THEN  D  (-1)
                THEN  Auto))\mcdot{}

---

Home Index