---

Step * 1 of Lemma init0-baire-eq-from


1. a : ℕ ⟶ ℕ
2. n : ℕ
3. ¬0 < n
4. init0(a)
⊢ (a n) = 0 ∈ ℕ
BY
{ ((Assert ⌜n = 0 ∈ ℕ⌝⋅ THENA Auto) THEN Eliminate ⌜n⌝⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
2.  n  :  \mBbbN{}
3.  \mneg{}0  <  n
4.  init0(a)
\mvdash{}  (a  n)  =  0


By

---

Latex:
((Assert  \mkleeneopen{}n  =  0\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Eliminate  \mkleeneopen{}n\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index