---

Step * 1 of Lemma gamma-neighbourhood-prop1


1. beta : ℕ ⟶ ℕ
2. n0 : finite-nat-seq()
3. a : ℕ ⟶ ℕ
⊢ ∃x:ℕ. (↑isl(gamma-neighbourhood(beta;n0) a^(x)))
BY
{ (InstConcl [⌜(fst(n0)) + 1⌝]⋅ THENA Auto) }

1
1. beta : ℕ ⟶ ℕ
2. n0 : finite-nat-seq()
3. a : ℕ ⟶ ℕ
⊢ ↑isl(gamma-neighbourhood(beta;n0) a^((fst(n0)) + 1))

---

Latex:

---

Latex:

1.  beta  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
2.  n0  :  finite-nat-seq()
3.  a  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
\mvdash{}  \mexists{}x:\mBbbN{}.  (\muparrow{}isl(gamma-neighbourhood(beta;n0)  a\^{}(x)))


By

---

Latex:
(InstConcl  [\mkleeneopen{}(fst(n0))  +  1\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index