---

Step * 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. (∀orbit∈orbits.0 < ||orbit||
          ∧ no_repeats(ℕn;orbit)
          ∧ (∀i:ℕ||orbit||. ((f orbit[i]) = if (i =z ||orbit|| - 1) then orbit[0] else orbit[i + 1] fi  ∈ ℕn))
          ∧ (∀x∈orbit.∀n@0:ℕ. (f^n@0 x ∈ orbit)))
7. ∀a:ℕn. (∃orbit∈orbits. (a ∈ orbit))
8. (∀o1,o2∈orbits.  l_disjoint(ℕn;o1;o2))
⊢ ∃m:ℕn + 1. (0 < m ∧ ((f^m x) = x ∈ ℕn))
BY
{ ((InstHyp [⌜x⌝] (-2)⋅ THEN Auto)
   THEN D (-1)
   THEN With ⌜i⌝ (D 6)⋅
   THEN Auto
   THEN ((Assert ||orbits[i]|| ≤ n BY
                (BLemma `injection_le` THEN Auto THEN FLemma `no_repeats_inject` [-3] THEN Auto))
         THEN InstConcl [⌜||orbits[i]||⌝]⋅
         THEN Auto)⋅) }

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. 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

---

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{}orbit\mmember{}orbits.0  <  ||orbit||
                    \mwedge{}  no\_repeats(\mBbbN{}n;orbit)
                    \mwedge{}  (\mforall{}i:\mBbbN{}||orbit||
                              ((f  orbit[i])  =  if  (i  =\msubz{}  ||orbit||  -  1)  then  orbit[0]  else  orbit[i  +  1]  fi  ))
                    \mwedge{}  (\mforall{}x\mmember{}orbit.\mforall{}n@0:\mBbbN{}.  (f\^{}n@0  x  \mmember{}  orbit)))
7.  \mforall{}a:\mBbbN{}n.  (\mexists{}orbit\mmember{}orbits.  (a  \mmember{}  orbit))
8.  (\mforall{}o1,o2\mmember{}orbits.    l\_disjoint(\mBbbN{}n;o1;o2))
\mvdash{}  \mexists{}m:\mBbbN{}n  +  1.  (0  <  m  \mwedge{}  ((f\^{}m  x)  =  x))


By

---

Latex:
((InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto)
  THEN  D  (-1)
  THEN  With  \mkleeneopen{}i\mkleeneclose{}  (D  6)\mcdot{}
  THEN  Auto
  THEN  ((Assert  ||orbits[i]||  \mleq{}  n  BY
                            (BLemma  `injection\_le`  THEN  Auto  THEN  FLemma  `no\_repeats\_inject`  [-3]  THEN  Auto))
              THEN  InstConcl  [\mkleeneopen{}||orbits[i]||\mkleeneclose{}]\mcdot{}
              THEN  Auto)\mcdot{})

---

Home Index