Step * 1 1 1 1 of Lemma not-decidable-zero-sequence


1. : ∀s:ℕ ⟶ ℕ((s x.0) ∈ (ℕ ⟶ ℕ)) ∨ (s x.0) ∈ (ℕ ⟶ ℕ))))
2. : ℕ
3. x.0) x.0) ∈ (ℕ ⟶ ℕ)
4. (G x.0)) (inl x) ∈ (((λx.0) x.0) ∈ (ℕ ⟶ ℕ)) ∨ ((λx.0) x.0) ∈ (ℕ ⟶ ℕ))))
⊢ (∀g:ℕ ⟶ ℕ
     (((λx.0) g ∈ (ℕn ⟶ ℕ))
      (case inl of inl(x) => inr(x) => case of inl(x) => inr(x) => 1 ∈ ℕ)))
 False
BY
(Reduce 0
   THEN ThinVar `x'
   THEN (D THENA Auto)
   THEN (InstHyp [⌜λx.if (x) < (n)  then 0  else 1⌝(-1)⋅ THENA Auto)
   THEN Thin (-2)) }

1
1. : ∀s:ℕ ⟶ ℕ((s x.0) ∈ (ℕ ⟶ ℕ)) ∨ (s x.0) ∈ (ℕ ⟶ ℕ))))
2. : ℕ
3. case x.if (x) < (n)  then 0  else 1) of inl(x) => inr(x) => 1 ∈ ℕ
⊢ False


Latex:


Latex:

1.  G  :  \mforall{}s:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((s  =  (\mlambda{}x.0))  \mvee{}  (\mneg{}(s  =  (\mlambda{}x.0))))
2.  n  :  \mBbbN{}
3.  x  :  (\mlambda{}x.0)  =  (\mlambda{}x.0)
4.  (G  (\mlambda{}x.0))  =  (inl  x)
\mvdash{}  (\mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}
          (((\mlambda{}x.0)  =  g)
          {}\mRightarrow{}  (case  inl  x  of  inl(x)  =>  0  |  inr(x)  =>  1  =  case  G  g  of  inl(x)  =>  0  |  inr(x)  =>  1)))
{}\mRightarrow{}  False


By


Latex:
(Reduce  0
  THEN  ThinVar  `x'
  THEN  (D  0  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}\mlambda{}x.if  (x)  <  (n)    then  0    else  1\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  Thin  (-2))




Home Index