---

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


1. G : ∀s:ℕ ⟶ ℕ. ((s = (λx.0) ∈ (ℕ ⟶ ℕ)) ∨ (¬(s = (λx.0) ∈ (ℕ ⟶ ℕ))))
2. n : ℕ
3. 0 = case G (λx.if (x) < (n)  then 0  else 1) of inl(x) => 0 | inr(x) => 1 ∈ ℕ
⊢ False
BY
{ (MoveToConcl (-1)
   THEN (GenConclTerm ⌜G (λx.if (x) < (n)  then 0  else 1)⌝⋅ THENA Auto)
   THEN DProdsAndUnions
   THEN AllReduce
   THEN Auto
   THEN (Assert ⌜((λx.if (x) < (n)  then 0  else 1) n) = ((λx.0) n) ∈ ℕ⌝⋅ THENA Auto)
   THEN AllReduce
   THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}G  (\mlambda{}x.if  (x)  <  (n)    then  0    else  1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  DProdsAndUnions
  THEN  AllReduce
  THEN  Auto
  THEN  (Assert  \mkleeneopen{}((\mlambda{}x.if  (x)  <  (n)    then  0    else  1)  n)  =  ((\mlambda{}x.0)  n)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  AllReduce
  THEN  Auto)

---

Home Index