---

Step * of Lemma not-decidable-zero-sequence

¬(∀s:ℕ ⟶ ℕ. ((s = (λx.0) ∈ (ℕ ⟶ ℕ)) ∨ (¬(s = (λx.0) ∈ (ℕ ⟶ ℕ)))))
BY
{ ((D 0 THENA Auto) THEN RenameVar `G' (-1)) }

1
1. G : ∀s:ℕ ⟶ ℕ. ((s = (λx.0) ∈ (ℕ ⟶ ℕ)) ∨ (¬(s = (λx.0) ∈ (ℕ ⟶ ℕ))))
⊢ False

---

Latex:

---

Latex:
\mneg{}(\mforall{}s:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((s  =  (\mlambda{}x.0))  \mvee{}  (\mneg{}(s  =  (\mlambda{}x.0)))))


By

---

Latex:
((D  0  THENA  Auto)  THEN  RenameVar  `G'  (-1))

---

Home Index