---

Step * 4 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
{ (RWO "apply-cycle-non-member" (-3) THEN Auto)⋅ }

---

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.  \mneg{}(a1  \mmember{}  L)
8.  \mneg{}(a2  \mmember{}  L)
\mvdash{}  a1  =  a2


By

---

Latex:
(RWO  "apply-cycle-non-member"  (-3)  THEN  Auto)\mcdot{}

---

Home Index