---

Step * 1 1 of Lemma gamma-neighbourhood-prop2

.....assertion..... 
1. beta : ℕ ⟶ ℕ
2. n0 : finite-nat-seq()
3. x : ℕ
4. ¬((beta x) = 0 ∈ ℤ)
⊢ ∃x1:ℕx + 1. ((¬((beta x1) = 0 ∈ ℤ)) ∧ (∀y:ℕx1. ((beta y) = 0 ∈ ℤ)))
BY
{ ((Assert ⌜∃y:ℕx + 1. (¬((beta y) = 0 ∈ ℤ))⌝⋅ THENA (InstConcl [⌜x⌝]⋅ THEN Auto)) THEN Thin (-2)) }

1
1. beta : ℕ ⟶ ℕ
2. n0 : finite-nat-seq()
3. x : ℕ
4. ∃y:ℕx + 1. (¬((beta y) = 0 ∈ ℤ))
⊢ ∃x1:ℕx + 1. ((¬((beta x1) = 0 ∈ ℤ)) ∧ (∀y:ℕx1. ((beta y) = 0 ∈ ℤ)))

---

Latex:

---

Latex:
.....assertion..... 
1.  beta  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
2.  n0  :  finite-nat-seq()
3.  x  :  \mBbbN{}
4.  \mneg{}((beta  x)  =  0)
\mvdash{}  \mexists{}x1:\mBbbN{}x  +  1.  ((\mneg{}((beta  x1)  =  0))  \mwedge{}  (\mforall{}y:\mBbbN{}x1.  ((beta  y)  =  0)))


By

---

Latex:
((Assert  \mkleeneopen{}\mexists{}y:\mBbbN{}x  +  1.  (\mneg{}((beta  y)  =  0))\mkleeneclose{}\mcdot{}  THENA  (InstConcl  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto))  THEN  Thin  (-2))

---

Home Index