---

Step * 1 1 1 1 of Lemma orbit-exists


1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)
3. n : ℕ
4. g : ℕn ⟶ T
5. Surj(ℕn;T;g)
6. f : T ⟶ T
7. a : T
⊢ ∃k:ℕ. ∃i:ℕk. ((f^k a) = (f^i a) ∈ T)
BY
{ (Unfold `surject` -3
   THEN (Skolemize (-3) `h' THENA Auto)
   THEN (InstLemma `not-inject` [⌜ℕn⌝;⌜n + 1⌝;⌜λi.(h (f^i a))⌝]⋅ THENA Auto)) }

1
.....antecedent..... 
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)
⊢ ¬Inj(ℕn + 1;ℕn;λi.(h (f^i a)))

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

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  \mforall{}x,y:T.    Dec(x  =  y)
3.  n  :  \mBbbN{}
4.  g  :  \mBbbN{}n  {}\mrightarrow{}  T
5.  Surj(\mBbbN{}n;T;g)
6.  f  :  T  {}\mrightarrow{}  T
7.  a  :  T
\mvdash{}  \mexists{}k:\mBbbN{}.  \mexists{}i:\mBbbN{}k.  ((f\^{}k  a)  =  (f\^{}i  a))


By

---

Latex:
(Unfold  `surject`  -3
  THEN  (Skolemize  (-3)  `h'  THENA  Auto)
  THEN  (InstLemma  `not-inject`  [\mkleeneopen{}\mBbbN{}n\mkleeneclose{};\mkleeneopen{}n  +  1\mkleeneclose{};\mkleeneopen{}\mlambda{}i.(h  (f\^{}i  a))\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index