---

Step * 1 1 of Lemma gamma-neighbourhood-prop3


1. beta : ℕ ⟶ ℕ
2. n : ℕ
3. m : ℕ
4. (beta 0) = 0 ∈ ℤ
5. ↑init-seg-nat-seq(0s^(m);0s^(n))
⊢ False ⇒ (n < m ∧ ((inr ⋅ ) = (inl 0) ∈ (ℕ?)))
BY
{ Auto }

---

Latex:

---

Latex:

1.  beta  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
2.  n  :  \mBbbN{}
3.  m  :  \mBbbN{}
4.  (beta  0)  =  0
5.  \muparrow{}init-seg-nat-seq(0s\^{}(m);0s\^{}(n))
\mvdash{}  False  {}\mRightarrow{}  (n  <  m  \mwedge{}  ((inr  \mcdot{}  )  =  (inl  0)))


By

---

Latex:
Auto

---

Home Index