---

Step * 1 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. ∀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
BY
{ (RepeatFor 2 (MoveToConcl (-1))
   THEN GenConclAtAddr [1;2]
   THEN ThinVar `orbits'
   THEN RenameVar `orbit' (-1)
   THEN Auto) }

1
1. n : ℕ
2. f : ℕn ⟶ ℕn
3. Inj(ℕn;ℕn;f)
4. x : ℕn
5. orbit : ℕn List
6. (x ∈ orbit)
7. ∀i@0:ℕ||orbit||. ((f orbit[i@0]) = if (i@0 =z ||orbit|| - 1) then orbit[0] else orbit[i@0 + 1] fi  ∈ ℕn)
⊢ (f^||orbit|| 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.  \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  )
\mvdash{}  (f\^{}||orbits[i]||  x)  =  x


By

---

Latex:
(RepeatFor  2  (MoveToConcl  (-1))
  THEN  GenConclAtAddr  [1;2]
  THEN  ThinVar  `orbits'
  THEN  RenameVar  `orbit'  (-1)
  THEN  Auto)

---

Home Index