---

Step * of Lemma cycle_wf

∀[n:ℕ]. ∀[L:ℕn List].  (cycle(L) ∈ ℕn ⟶ ℕn)
BY
{ (Auto THEN Unfold `cycle` 0 THEN Reduce 0 THEN DVar `L' THEN RepUR ``let`` 0) }

1
1. n : ℕ
⊢ λx.x ∈ ℕn ⟶ ℕn

2
1. n : ℕ
2. u : ℕn
3. v : ℕn List
⊢ λx.if (x =z u)
     then if null(v) then u else hd(v) fi 
     else rec-case(v) of
          [] => x
          h::t =>
           r.if (x =z h) then if null(t) then u else hd(t) fi  else r fi 
     fi  ∈ ℕn ⟶ ℕn

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[L:\mBbbN{}n  List].    (cycle(L)  \mmember{}  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n)


By

---

Latex:
(Auto  THEN  Unfold  `cycle`  0  THEN  Reduce  0  THEN  DVar  `L'  THEN  RepUR  ``let``  0)

---

Home Index