---

Step * of Lemma no-halt-decider

¬(∃h:partial(ℤ) ⟶ 𝔹. (h 0 = tt ∧ h ⊥ = ff))
BY
{ Assert ⌜⊥ ∈ partial(ℤ)⌝⋅ }

1
.....assertion..... 
⊥ ∈ partial(ℤ)

2
1. ⊥ ∈ partial(ℤ)
⊢ ¬(∃h:partial(ℤ) ⟶ 𝔹. (h 0 = tt ∧ h ⊥ = ff))

---

Latex:

---

Latex:
\mneg{}(\mexists{}h:partial(\mBbbZ{})  {}\mrightarrow{}  \mBbbB{}.  (h  0  =  tt  \mwedge{}  h  \mbot{}  =  ff))


By

---

Latex:
Assert  \mkleeneopen{}\mbot{}  \mmember{}  partial(\mBbbZ{})\mkleeneclose{}\mcdot{}

---

Home Index