---

Step * 2 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
{ ((InstLemma `cycle-closed` [⌜n⌝;⌜a1⌝;⌜L⌝]⋅ THEN Auto)⋅ THEN Subst' ⌜(cycle(L) a2) = a2 ∈ ℕn⌝ (-4)⋅ 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.  (a1  \mmember{}  L)
8.  \mneg{}(a2  \mmember{}  L)
\mvdash{}  a1  =  a2


By

---

Latex:
((InstLemma  `cycle-closed`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THEN  Auto)\mcdot{}
  THEN  Subst'  \mkleeneopen{}(cycle(L)  a2)  =  a2\mkleeneclose{}  (-4)\mcdot{}
  THEN  Auto)

---

Home Index