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