---

Step * 1 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. 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
BY
{ xxx(RepeatFor 2 (D -2) THEN HypSubst' -2 0 THEN ThinVar `x')xxx }

1
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

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n
3.  Inj(\mBbbN{}n;\mBbbN{}n;f)
4.  x  :  \mBbbN{}n
5.  orbit  :  \mBbbN{}n  List
6.  (x  \mmember{}  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||  x)  =  x


By

---

Latex:
xxx(RepeatFor  2  (D  -2)  THEN  HypSubst'  -2  0  THEN  ThinVar  `x')xxx

---

Home Index