---

Step * 1 1 1 2 1 1 of Lemma gamma-neighbourhood-prop2


1. beta : ℕ ⟶ ℕ
2. n0 : finite-nat-seq()
3. x : ℤ
4. [%1] : 0 < x
5. (∃y:ℕ(x - 1) + 1. (¬((beta y) = 0 ∈ ℤ)))
⇒ (∃x1:ℕ(x - 1) + 1. ((¬((beta x1) = 0 ∈ ℤ)) ∧ (∀y:ℕx1. ((beta y) = 0 ∈ ℤ))))
6. y : ℕx + 1
7. ¬((beta y) = 0 ∈ ℤ)
8. ∃k:ℕ(x - 1) + 1. (¬((beta k) = 0 ∈ ℤ))
⊢ ∃x1:ℕx + 1. ((¬((beta x1) = 0 ∈ ℤ)) ∧ (∀y:ℕx1. ((beta y) = 0 ∈ ℤ)))
BY
{ ((D (-4) THENA Auto) THEN ExRepD THEN InstConcl [⌜x1⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  beta  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
2.  n0  :  finite-nat-seq()
3.  x  :  \mBbbZ{}
4.  [\%1]  :  0  <  x
5.  (\mexists{}y:\mBbbN{}(x  -  1)  +  1.  (\mneg{}((beta  y)  =  0)))
{}\mRightarrow{}  (\mexists{}x1:\mBbbN{}(x  -  1)  +  1.  ((\mneg{}((beta  x1)  =  0))  \mwedge{}  (\mforall{}y:\mBbbN{}x1.  ((beta  y)  =  0))))
6.  y  :  \mBbbN{}x  +  1
7.  \mneg{}((beta  y)  =  0)
8.  \mexists{}k:\mBbbN{}(x  -  1)  +  1.  (\mneg{}((beta  k)  =  0))
\mvdash{}  \mexists{}x1:\mBbbN{}x  +  1.  ((\mneg{}((beta  x1)  =  0))  \mwedge{}  (\mforall{}y:\mBbbN{}x1.  ((beta  y)  =  0)))


By

---

Latex:
((D  (-4)  THENA  Auto)  THEN  ExRepD  THEN  InstConcl  [\mkleeneopen{}x1\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index