---

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


1. n : ℕ
2. f : ℕn ⟶ ℕn
3. Inj(ℕn;ℕn;f)
4. x : ℕn
⊢ ∃m:ℕn + 1. (0 < m ∧ ((f^m x) = x ∈ ℕn))
BY
{ xxx((InstLemma `orbit-decomp` [⌜ℕn⌝;⌜f⌝]⋅ THENA Auto) THEN ExRepD)xxx }

1
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))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n
3.  Inj(\mBbbN{}n;\mBbbN{}n;f)
4.  x  :  \mBbbN{}n
\mvdash{}  \mexists{}m:\mBbbN{}n  +  1.  (0  <  m  \mwedge{}  ((f\^{}m  x)  =  x))


By

---

Latex:
xxx((InstLemma  `orbit-decomp`  [\mkleeneopen{}\mBbbN{}n\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  ExRepD)xxx

---

Home Index