---

Step * of Lemma not-btrue-sqle-bfalse

¬(tt ≤ ff)
BY
{ (D 0
   THEN Auto
   THEN (Assert ⌜(λb.if b then 0 else ⊥ fi ) tt ≤ (λb.if b then 0 else ⊥ fi ) ff⌝⋅ THENA Auto)
   THEN Reduce (-1)
   THEN FLemma `has-value-monotonic` [-1]
   THEN Auto
   THEN BotDiv) }

---

Latex:

---

Latex:
\mneg{}(tt  \mleq{}  ff)


By

---

Latex:
(D  0
  THEN  Auto
  THEN  (Assert  \mkleeneopen{}(\mlambda{}b.if  b  then  0  else  \mbot{}  fi  )  tt  \mleq{}  (\mlambda{}b.if  b  then  0  else  \mbot{}  fi  )  ff\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  FLemma  `has-value-monotonic`  [-1]
  THEN  Auto
  THEN  BotDiv)

---

Home Index