---

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


1. G : ∀s:ℕ ⟶ ℕ. ((s = (λx.0) ∈ (ℕ ⟶ ℕ)) ∨ (¬(s = (λx.0) ∈ (ℕ ⟶ ℕ))))
⊢ False
BY
{ ((InstLemma `strong-continuity2-implies-weak` [⌜λf.case G f of inl(x) => 0 | inr(x) => 1⌝]⋅ THENA Auto)
   THEN AllReduce
   ) }

1
1. G : ∀s:ℕ ⟶ ℕ. ((s = (λx.0) ∈ (ℕ ⟶ ℕ)) ∨ (¬(s = (λx.0) ∈ (ℕ ⟶ ℕ))))
2. ∀f:ℕ ⟶ ℕ
     ⇃(∃n:ℕ
        ∀g:ℕ ⟶ ℕ
          ((f = g ∈ (ℕn ⟶ ℕ)) ⇒ (case G f of inl(x) => 0 | inr(x) => 1 = case G g of inl(x) => 0 | inr(x) => 1 ∈ ℕ)))
⊢ False

---

Latex:

---

Latex:

1.  G  :  \mforall{}s:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((s  =  (\mlambda{}x.0))  \mvee{}  (\mneg{}(s  =  (\mlambda{}x.0))))
\mvdash{}  False


By

---

Latex:
((InstLemma  `strong-continuity2-implies-weak`  [\mkleeneopen{}\mlambda{}f.case  G  f  of  inl(x)  =>  0  |  inr(x)  =>  1\mkleeneclose{}]\mcdot{}
    THENA  Auto
    )
  THEN  AllReduce
  )

---

Home Index