Step * 1 of Lemma gamma-neighbourhood-prop2


1. beta : ℕ ⟶ ℕ
2. n0 finite-nat-seq()
3. : ℕ
4. ¬((beta x) 0 ∈ ℤ)
⊢ ∃x1:ℕ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:ℕ1. ((¬((beta x1) 0 ∈ ℤ)) ∧ (∀y:ℕx1. ((beta y) 0 ∈ ℤ)))⌝⋅ }

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

2
1. beta : ℕ ⟶ ℕ
2. n0 finite-nat-seq()
3. : ℕ
4. ¬((beta x) 0 ∈ ℤ)
5. ∃x1:ℕ1. ((¬((beta x1) 0 ∈ ℤ)) ∧ (∀y:ℕx1. ((beta y) 0 ∈ ℤ)))
⊢ ∃x1:ℕ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