---

Step * 2 of Lemma no-halt-decider


1. ⊥ ∈ partial(ℤ)
⊢ ¬(∃h:partial(ℤ) ⟶ 𝔹. (h 0 = tt ∧ h ⊥ = ff))
BY
{ ((D 0 THEN Auto)
   THEN D -1
   THEN ((InstLemma `fixpoint-induction-bottom` 
          [⌜ℤ⌝;⌜partial(ℤ)⌝;⌜λx.x⌝;⌜λt.if h t then ⊥ else 0 fi ⌝]⋅
         THENM Reduce (-1)⋅
         )
         THENA Auto
         )) }

1
1. ⊥ ∈ partial(ℤ)
2. h : partial(ℤ) ⟶ 𝔹
3. h 0 = tt ∧ h ⊥ = ff
4. fix((λt.if h t then ⊥ else 0 fi )) ∈ partial(ℤ)
⊢ False

---

Latex:

---

Latex:

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


By

---

Latex:
((D  0  THEN  Auto)
  THEN  D  -1
  THEN  ((InstLemma  `fixpoint-induction-bottom` 
                [\mkleeneopen{}\mBbbZ{}\mkleeneclose{};\mkleeneopen{}partial(\mBbbZ{})\mkleeneclose{};\mkleeneopen{}\mlambda{}x.x\mkleeneclose{};\mkleeneopen{}\mlambda{}t.if  h  t  then  \mbot{}  else  0  fi  \mkleeneclose{}]\mcdot{}
              THENM  Reduce  (-1)\mcdot{}
              )
              THENA  Auto
              ))

---

Home Index