---

Step * 2 2 1 1 1 1 1 1 1 of Lemma cyclic-map-equipollent


1. n : ℕ+
2. ∀L:Combination(n - 1;ℕn - 1). ([n - 1 / L] ∈ Combination(n;ℕn))
3. b : ℕn ⟶ ℕn
4. Inj(ℕn;ℕn;b)
5. ∀x,y:ℕn.  ∃n@0:ℕ. ((b^n@0 x) = y ∈ ℕn)
6. orbit : ℕn List
7. (0 ∈ orbit)
8. orbit(ℕn;b;orbit)
9. ∀y:ℕn. (y ∈ orbit)
10. x : ℕn
11. i : ℕ
12. i < ||orbit||
13. x = orbit[i] ∈ ℕn
⊢ (b orbit[i]) = (cycle(orbit) orbit[i]) ∈ ℕn
BY
{ xxx(RWO "apply-cycle-member" 0 THENA Auto)xxx }

1
1. n : ℕ+
2. ∀L:Combination(n - 1;ℕn - 1). ([n - 1 / L] ∈ Combination(n;ℕn))
3. b : ℕn ⟶ ℕn
4. Inj(ℕn;ℕn;b)
5. ∀x,y:ℕn.  ∃n@0:ℕ. ((b^n@0 x) = y ∈ ℕn)
6. orbit : ℕn List
7. (0 ∈ orbit)
8. orbit(ℕn;b;orbit)
9. ∀y:ℕn. (y ∈ orbit)
10. x : ℕn
11. i : ℕ
12. i < ||orbit||
13. x = orbit[i] ∈ ℕn
⊢ (b orbit[i]) = if (i =z ||orbit|| - 1) then orbit[0] else orbit[i + 1] fi  ∈ ℕn

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  \mforall{}L:Combination(n  -  1;\mBbbN{}n  -  1).  ([n  -  1  /  L]  \mmember{}  Combination(n;\mBbbN{}n))
3.  b  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n
4.  Inj(\mBbbN{}n;\mBbbN{}n;b)
5.  \mforall{}x,y:\mBbbN{}n.    \mexists{}n@0:\mBbbN{}.  ((b\^{}n@0  x)  =  y)
6.  orbit  :  \mBbbN{}n  List
7.  (0  \mmember{}  orbit)
8.  orbit(\mBbbN{}n;b;orbit)
9.  \mforall{}y:\mBbbN{}n.  (y  \mmember{}  orbit)
10.  x  :  \mBbbN{}n
11.  i  :  \mBbbN{}
12.  i  <  ||orbit||
13.  x  =  orbit[i]
\mvdash{}  (b  orbit[i])  =  (cycle(orbit)  orbit[i])


By

---

Latex:
xxx(RWO  "apply-cycle-member"  0  THENA  Auto)xxx

---

Home Index