---

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


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
BY
{ ((InstHyp [⌜λx.0⌝] (-1)⋅ THENA Auto) THEN Thin (-2) THEN (UnHalfSquash  THENA Auto) THEN ExRepD) }

1
1. G : ∀s:ℕ ⟶ ℕ. ((s = (λx.0) ∈ (ℕ ⟶ ℕ)) ∨ (¬(s = (λx.0) ∈ (ℕ ⟶ ℕ))))
2. n : ℕ
3. ∀g:ℕ ⟶ ℕ
     (((λx.0) = g ∈ (ℕn ⟶ ℕ))
     ⇒ (case G (λx.0) 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))))
2.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}
          \00D9(\mexists{}n:\mBbbN{}
                \mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}
                    ((f  =  g)
                    {}\mRightarrow{}  (case  G  f  of  inl(x)  =>  0  |  inr(x)  =>  1  =  case  G  g  of  inl(x)  =>  0  |  inr(x)  =>  1)))
\mvdash{}  False


By

---

Latex:
((InstHyp  [\mkleeneopen{}\mlambda{}x.0\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)  THEN  Thin  (-2)  THEN  (UnHalfSquash    THENA  Auto)  THEN  ExRepD)

---

Home Index