---

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


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
9. m : ℕn + 1
10. 0 < m
11. (f^m x) = x ∈ ℕn
12. (f^k x) = (f^k rem m x) ∈ ℕn
⊢ ∃m:ℕn. ((f^m x) = y ∈ ℕn)
BY
{ xxx((InstLemma `rem_bounds_1` [⌜k⌝;⌜m⌝]⋅ THENA Auto) THEN InstConcl [⌜k rem m⌝]⋅ THEN Auto)xxx }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n
3.  Inj(\mBbbN{}n;\mBbbN{}n;f)
4.  \mforall{}x,y:\mBbbN{}n.    \mexists{}n@0:\mBbbN{}.  ((f\^{}n@0  x)  =  y)
5.  x  :  \mBbbN{}n
6.  y  :  \mBbbN{}n
7.  k  :  \mBbbN{}
8.  (f\^{}k  x)  =  y
9.  m  :  \mBbbN{}n  +  1
10.  0  <  m
11.  (f\^{}m  x)  =  x
12.  (f\^{}k  x)  =  (f\^{}k  rem  m  x)
\mvdash{}  \mexists{}m:\mBbbN{}n.  ((f\^{}m  x)  =  y)


By

---

Latex:
xxx((InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  InstConcl  [\mkleeneopen{}k  rem  m\mkleeneclose{}]\mcdot{}  THEN  Auto)xxx

---

Home Index