---

Step * of Lemma cycle_wf2

∀[n:ℕ]. ∀[L:Combination(n;ℕn)].  (cycle(L) ∈ cyclic-map(ℕn))
BY
{ (Auto THEN MemTypeCD) }

1
1. n : ℕ
2. L : Combination(n;ℕn)
⊢ cycle(L) ∈ ℕn →⟶ ℕn

2
.....set predicate..... 
1. n : ℕ
2. L : Combination(n;ℕn)
⊢ ∀x,y:ℕn.  ∃n@0:ℕ. ((cycle(L)^n@0 x) = y ∈ ℕn)

3
.....wf..... 
1. n : ℕ
2. L : Combination(n;ℕn)
3. f : ℕn →⟶ ℕn
⊢ ∀x,y:ℕn.  ∃n@0:ℕ. ((f^n@0 x) = y ∈ ℕn) ∈ Type

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[L:Combination(n;\mBbbN{}n)].    (cycle(L)  \mmember{}  cyclic-map(\mBbbN{}n))


By

---

Latex:
(Auto  THEN  MemTypeCD)

---

Home Index