---

Step * of Lemma cycle-closed

∀n:ℕ. ∀x:ℕn. ∀L:ℕn List.  (x ∈ L) ⇒ (cycle(L) x ∈ L) supposing no_repeats(ℕn;L)
BY
{ (Auto
   THEN RepeatFor 2 (D -1)
   THEN HypSubst' -1 0
   THEN RWO "apply-cycle-member" 0
   THEN Auto
   THEN SplitOnConclITE
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}x:\mBbbN{}n.  \mforall{}L:\mBbbN{}n  List.    (x  \mmember{}  L)  {}\mRightarrow{}  (cycle(L)  x  \mmember{}  L)  supposing  no\_repeats(\mBbbN{}n;L)


By

---

Latex:
(Auto
  THEN  RepeatFor  2  (D  -1)
  THEN  HypSubst'  -1  0
  THEN  RWO  "apply-cycle-member"  0
  THEN  Auto
  THEN  SplitOnConclITE
  THEN  Auto)

---

Home Index