---

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

.....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)))
BY
{ (D 0 THENA Auto) }

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

---

Latex:

---

Latex:
.....antecedent..... 
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)
\mvdash{}  \mneg{}Inj(\mBbbN{}n  +  1;\mBbbN{}n;\mlambda{}i.(h  (f\^{}i  a)))


By

---

Latex:
(D  0  THENA  Auto)

---

Home Index