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