---

Step * of Lemma not-bfalse-sqle-btrue

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

---

Latex:

---

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


By

---

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

---

Home Index