---

Step * 1 of Lemma cycle-injection


1. n : ℕ
2. L : ℕn List
3. no_repeats(ℕn;L)
4. a1 : ℕn@i
5. a2 : ℕn@i
6. (cycle(L) a1) = (cycle(L) a2) ∈ ℕn
7. (a1 ∈ L)
8. (a2 ∈ L)
⊢ a1 = a2 ∈ ℕn
BY
{ (RepeatFor 2 (D (-2)) THEN RepeatFor 2 (D (-1))) }

1
1. n : ℕ
2. L : ℕn List
3. no_repeats(ℕn;L)
4. a1 : ℕn@i
5. a2 : ℕn@i
6. (cycle(L) a1) = (cycle(L) a2) ∈ ℕn
7. i : ℕ
8. i < ||L||
9. a1 = L[i] ∈ ℕn
10. i1 : ℕ
11. i1 < ||L||
12. a2 = L[i1] ∈ ℕn
⊢ a1 = a2 ∈ ℕn

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  L  :  \mBbbN{}n  List
3.  no\_repeats(\mBbbN{}n;L)
4.  a1  :  \mBbbN{}n@i
5.  a2  :  \mBbbN{}n@i
6.  (cycle(L)  a1)  =  (cycle(L)  a2)
7.  (a1  \mmember{}  L)
8.  (a2  \mmember{}  L)
\mvdash{}  a1  =  a2


By

---

Latex:
(RepeatFor  2  (D  (-2))  THEN  RepeatFor  2  (D  (-1)))

---

Home Index