---

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


1. n : ℕ
2. f : ℕn ⟶ ℕn
3. Inj(ℕn;ℕn;f)
4. orbit : ℕn List
5. i : ℕ
6. i < ||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|| orbit[i]) = orbit[i] ∈ ℕn
BY
{ xxxAssert ⌜∀m:ℕ. ((f^m orbit[i]) = orbit[i + m rem ||orbit||] ∈ ℕn)⌝⋅xxx }

1
.....assertion..... 
1. n : ℕ
2. f : ℕn ⟶ ℕn
3. Inj(ℕn;ℕn;f)
4. orbit : ℕn List
5. i : ℕ
6. i < ||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)
⊢ ∀m:ℕ. ((f^m orbit[i]) = orbit[i + m rem ||orbit||] ∈ ℕn)

2
1. n : ℕ
2. f : ℕn ⟶ ℕn
3. Inj(ℕn;ℕn;f)
4. orbit : ℕn List
5. i : ℕ
6. i < ||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)
8. ∀m:ℕ. ((f^m orbit[i]) = orbit[i + m rem ||orbit||] ∈ ℕn)
⊢ (f^||orbit|| orbit[i]) = orbit[i] ∈ ℕn

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n
3.  Inj(\mBbbN{}n;\mBbbN{}n;f)
4.  orbit  :  \mBbbN{}n  List
5.  i  :  \mBbbN{}
6.  i  <  ||orbit||
7.  \mforall{}i@0:\mBbbN{}||orbit||
          ((f  orbit[i@0])  =  if  (i@0  =\msubz{}  ||orbit||  -  1)  then  orbit[0]  else  orbit[i@0  +  1]  fi  )
\mvdash{}  (f\^{}||orbit||  orbit[i])  =  orbit[i]


By

---

Latex:
xxxAssert  \mkleeneopen{}\mforall{}m:\mBbbN{}.  ((f\^{}m  orbit[i])  =  orbit[i  +  m  rem  ||orbit||])\mkleeneclose{}\mcdot{}xxx

---

Home Index