Step
*
1
of Lemma
gamma-neighbourhood-prop2
1. beta : ℕ ⟶ ℕ
2. n0 : finite-nat-seq()
3. x : ℕ
4. ¬((beta x) = 0 ∈ ℤ)
⊢ ∃x1:ℕx + 1
   ((¬((beta x1) = 0 ∈ ℤ))
   ∧ (∀y:ℕx1. ((beta y) = 0 ∈ ℤ))
   ∧ ((gamma-neighbourhood(beta;n0) n0**λx.x1^(1)) = (inl 1) ∈ (ℕ?))
   ∧ ((gamma-neighbourhood(beta;n0) n0**λx.(x1 + 1)^(1)) = (inl 0) ∈ (ℕ?)))
BY
{ Assert ⌜∃x1:ℕx + 1. ((¬((beta x1) = 0 ∈ ℤ)) ∧ (∀y:ℕx1. ((beta y) = 0 ∈ ℤ)))⌝⋅ }
1
.....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 ∈ ℤ)))
2
1. beta : ℕ ⟶ ℕ
2. n0 : finite-nat-seq()
3. x : ℕ
4. ¬((beta x) = 0 ∈ ℤ)
5. ∃x1:ℕx + 1. ((¬((beta x1) = 0 ∈ ℤ)) ∧ (∀y:ℕx1. ((beta y) = 0 ∈ ℤ)))
⊢ ∃x1:ℕx + 1
   ((¬((beta x1) = 0 ∈ ℤ))
   ∧ (∀y:ℕx1. ((beta y) = 0 ∈ ℤ))
   ∧ ((gamma-neighbourhood(beta;n0) n0**λx.x1^(1)) = (inl 1) ∈ (ℕ?))
   ∧ ((gamma-neighbourhood(beta;n0) n0**λx.(x1 + 1)^(1)) = (inl 0) ∈ (ℕ?)))
Latex:
Latex:
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))
      \mwedge{}  ((gamma-neighbourhood(beta;n0)  n0**\mlambda{}x.x1\^{}(1))  =  (inl  1))
      \mwedge{}  ((gamma-neighbourhood(beta;n0)  n0**\mlambda{}x.(x1  +  1)\^{}(1))  =  (inl  0)))
By
Latex:
Assert  \mkleeneopen{}\mexists{}x1:\mBbbN{}x  +  1.  ((\mneg{}((beta  x1)  =  0))  \mwedge{}  (\mforall{}y:\mBbbN{}x1.  ((beta  y)  =  0)))\mkleeneclose{}\mcdot{}
Home
Index