---

Step * 2 of Lemma cycle_wf2

.....set predicate..... 
1. n : ℕ
2. L : Combination(n;ℕn)
⊢ ∀x,y:ℕn.  ∃n@0:ℕ. ((cycle(L)^n@0 x) = y ∈ ℕn)
BY
{ xxx((D -1 THEN Auto)
      THEN (Assert no_repeats(ℕn;L) ∧ (||L|| = n ∈ ℤ) BY
                  (All (Unfold `no_repeats`) THEN Unhide THEN Auto))
      THEN Thin (-4))xxx }

1
1. n : ℕ
2. L : ℕn List
3. x : ℕn
4. y : ℕn
5. no_repeats(ℕn;L) ∧ (||L|| = n ∈ ℤ)
⊢ ∃n@0:ℕ. ((cycle(L)^n@0 x) = y ∈ ℕn)

---

Latex:

---

Latex:
.....set  predicate..... 
1.  n  :  \mBbbN{}
2.  L  :  Combination(n;\mBbbN{}n)
\mvdash{}  \mforall{}x,y:\mBbbN{}n.    \mexists{}n@0:\mBbbN{}.  ((cycle(L)\^{}n@0  x)  =  y)


By

---

Latex:
xxx((D  -1  THEN  Auto)
        THEN  (Assert  no\_repeats(\mBbbN{}n;L)  \mwedge{}  (||L||  =  n)  BY
                                (All  (Unfold  `no\_repeats`)  THEN  Unhide  THEN  Auto))
        THEN  Thin  (-4))xxx

---

Home Index