---

Step * 1 1 1 1 1 of Lemma cyclic-map-transitive


1. n : ℕ
2. f : ℕn ⟶ ℕn
3. Inj(ℕn;ℕn;f)
4. x : ℕn
5. orbits : ℕn List List
6. ∀a:ℕn. (∃orbit∈orbits. (a ∈ orbit))
7. (∀o1,o2∈orbits.  l_disjoint(ℕn;o1;o2))
8. i : ℕ||orbits||
9. (x ∈ orbits[i])
10. 0 < ||orbits[i]||
11. no_repeats(ℕn;orbits[i])
12. ∀i@0:ℕ||orbits[i]||
      ((f orbits[i][i@0]) = if (i@0 =z ||orbits[i]|| - 1) then orbits[i][0] else orbits[i][i@0 + 1] fi  ∈ ℕn)
13. (∀x∈orbits[i].∀n@0:ℕ. (f^n@0 x ∈ orbits[i]))
14. ||orbits[i]|| ≤ n
15. 0 < ||orbits[i]||
⊢ (f^||orbits[i]|| x) = x ∈ ℕn
BY
{ (RepeatFor 3 (Thin (-1)) THEN RepeatFor 2 (Thin (-2)))⋅ }

1
1. n : ℕ
2. f : ℕn ⟶ ℕn
3. Inj(ℕn;ℕn;f)
4. x : ℕn
5. orbits : ℕn List List
6. ∀a:ℕn. (∃orbit∈orbits. (a ∈ orbit))
7. (∀o1,o2∈orbits.  l_disjoint(ℕn;o1;o2))
8. i : ℕ||orbits||
9. (x ∈ orbits[i])
10. ∀i@0:ℕ||orbits[i]||
      ((f orbits[i][i@0]) = if (i@0 =z ||orbits[i]|| - 1) then orbits[i][0] else orbits[i][i@0 + 1] fi  ∈ ℕn)
⊢ (f^||orbits[i]|| x) = x ∈ ℕn

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n
3.  Inj(\mBbbN{}n;\mBbbN{}n;f)
4.  x  :  \mBbbN{}n
5.  orbits  :  \mBbbN{}n  List  List
6.  \mforall{}a:\mBbbN{}n.  (\mexists{}orbit\mmember{}orbits.  (a  \mmember{}  orbit))
7.  (\mforall{}o1,o2\mmember{}orbits.    l\_disjoint(\mBbbN{}n;o1;o2))
8.  i  :  \mBbbN{}||orbits||
9.  (x  \mmember{}  orbits[i])
10.  0  <  ||orbits[i]||
11.  no\_repeats(\mBbbN{}n;orbits[i])
12.  \mforall{}i@0:\mBbbN{}||orbits[i]||
            ((f  orbits[i][i@0])
            =  if  (i@0  =\msubz{}  ||orbits[i]||  -  1)  then  orbits[i][0]  else  orbits[i][i@0  +  1]  fi  )
13.  (\mforall{}x\mmember{}orbits[i].\mforall{}n@0:\mBbbN{}.  (f\^{}n@0  x  \mmember{}  orbits[i]))
14.  ||orbits[i]||  \mleq{}  n
15.  0  <  ||orbits[i]||
\mvdash{}  (f\^{}||orbits[i]||  x)  =  x


By

---

Latex:
(RepeatFor  3  (Thin  (-1))  THEN  RepeatFor  2  (Thin  (-2)))\mcdot{}

---

Home Index