---

Step * 1 1 1 1 2 of Lemma orbit-exists


1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)
3. n : ℕ
4. g : ℕn ⟶ T
5. ∀b:T. ∃a:ℕn. ((g a) = b ∈ T)
6. f : T ⟶ T
7. a : T
8. h : b:T ⟶ ℕn
9. ∀b:T. ((g (h b)) = b ∈ T)
10. ∃i:ℕn + 1. ∃j:ℕi. (((λi.(h (f^i a))) i) = ((λi.(h (f^i a))) j) ∈ ℕn)
⊢ ∃k:ℕ. ∃i:ℕk. ((f^k a) = (f^i a) ∈ T)
BY
{ (Reduce (-1) THEN RepeatFor 2 (ParallelLast)) }

1
1. T : Type
2. ∀x,y:T.  Dec(x = y ∈ T)
3. n : ℕ
4. g : ℕn ⟶ T
5. ∀b:T. ∃a:ℕn. ((g a) = b ∈ T)
6. f : T ⟶ T
7. a : T
8. h : b:T ⟶ ℕn
9. ∀b:T. ((g (h b)) = b ∈ T)
10. i : ℕn + 1
11. j : ℕi
12. (h (f^i a)) = (h (f^j a)) ∈ ℕn
⊢ (f^i a) = (f^j a) ∈ T

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  \mforall{}x,y:T.    Dec(x  =  y)
3.  n  :  \mBbbN{}
4.  g  :  \mBbbN{}n  {}\mrightarrow{}  T
5.  \mforall{}b:T.  \mexists{}a:\mBbbN{}n.  ((g  a)  =  b)
6.  f  :  T  {}\mrightarrow{}  T
7.  a  :  T
8.  h  :  b:T  {}\mrightarrow{}  \mBbbN{}n
9.  \mforall{}b:T.  ((g  (h  b))  =  b)
10.  \mexists{}i:\mBbbN{}n  +  1.  \mexists{}j:\mBbbN{}i.  (((\mlambda{}i.(h  (f\^{}i  a)))  i)  =  ((\mlambda{}i.(h  (f\^{}i  a)))  j))
\mvdash{}  \mexists{}k:\mBbbN{}.  \mexists{}i:\mBbbN{}k.  ((f\^{}k  a)  =  (f\^{}i  a))


By

---

Latex:
(Reduce  (-1)  THEN  RepeatFor  2  (ParallelLast))

---

Home Index