---

Step * of Lemma cyclic-map-transitive

∀n:ℕ. ∀f:cyclic-map(ℕn). ∀x,y:ℕn.  ∃m:ℕn. ((f^m x) = y ∈ ℕn)
BY
{ xxx(Auto
      THEN RepeatFor 2 (D 2)
      THEN Unhide
      THEN Auto
      THEN (InstHyp [⌜x⌝;⌜y⌝] 4⋅ THENA Auto)
      THEN ExRepD
      THEN RenameVar `k' (-2))xxx }

1
1. n : ℕ
2. f : ℕn ⟶ ℕn
3. Inj(ℕn;ℕn;f)
4. ∀x,y:ℕn.  ∃n@0:ℕ. ((f^n@0 x) = y ∈ ℕn)
5. x : ℕn
6. y : ℕn
7. k : ℕ
8. (f^k x) = y ∈ ℕn
⊢ ∃m:ℕn. ((f^m x) = y ∈ ℕn)

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}f:cyclic-map(\mBbbN{}n).  \mforall{}x,y:\mBbbN{}n.    \mexists{}m:\mBbbN{}n.  ((f\^{}m  x)  =  y)


By

---

Latex:
xxx(Auto
        THEN  RepeatFor  2  (D  2)
        THEN  Unhide
        THEN  Auto
        THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]  4\mcdot{}  THENA  Auto)
        THEN  ExRepD
        THEN  RenameVar  `k'  (-2))xxx

---

Home Index