---

Step * of Lemma cycle-injection

∀[n:ℕ]. ∀[L:ℕn List].  Inj(ℕn;ℕn;cycle(L)) supposing no_repeats(ℕn;L)
BY
{ (Auto THEN D 0 THEN Auto THEN (Decide (a1 ∈ L) THENA Auto) THEN (Decide (a2 ∈ L) THENA Auto)) }

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. (a1 ∈ L)
8. (a2 ∈ L)
⊢ a1 = a2 ∈ ℕn

2
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

3
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

4
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

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[L:\mBbbN{}n  List].    Inj(\mBbbN{}n;\mBbbN{}n;cycle(L))  supposing  no\_repeats(\mBbbN{}n;L)


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  (Decide  (a1  \mmember{}  L)  THENA  Auto)  THEN  (Decide  (a2  \mmember{}  L)  THENA  Auto))

---

Home Index