Step
*
of Lemma
strictness-atom1_eq-right
∀[a,b,c:Top]. (if a=1 ⊥ then b else c ~ eval x = a in ⊥)
BY
{ (SqReasoning THEN Assert ⌜(⊥)↓⌝⋅ THEN BotDiv) }
Latex:
Latex:
\mforall{}[a,b,c:Top]. (if a=1 \mbot{} then b else c \msim{} eval x = a in \mbot{})
By
Latex:
(SqReasoning THEN Assert \mkleeneopen{}(\mbot{})\mdownarrow{}\mkleeneclose{}\mcdot{} THEN BotDiv)
Home
Index