---

Step * of Lemma apply-cycle-non-member

∀[n:ℕ]. ∀[L:ℕn List]. ∀[x:ℕn].  (cycle(L) x) = x ∈ ℕn supposing ¬(x ∈ L)
BY
{ (Auto THEN RepUR ``cycle let`` 0 THEN Auto' THEN SplitOnConclITE THEN Auto) }

1
.....falsecase..... 
1. n : ℕ
2. L : ℕn List
3. x : ℕn
4. ¬(x ∈ L)
5. ¬(L = [] ∈ (ℕn List))
⊢ rec-case(L) of [] => x | a::as => r.if (x =z a) then if null(as) then hd(L) else hd(as) fi  else r fi  = x ∈ ℕn

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[L:\mBbbN{}n  List].  \mforall{}[x:\mBbbN{}n].    (cycle(L)  x)  =  x  supposing  \mneg{}(x  \mmember{}  L)


By

---

Latex:
(Auto  THEN  RepUR  ``cycle  let``  0  THEN  Auto'  THEN  SplitOnConclITE  THEN  Auto)

---

Home Index