Step
*
of Lemma
es-bless-not-ble
∀[es:EO]. ∀[e,e':E].  e <loc e' ~ ¬be' ≤loc e supposing loc(e) = loc(e') ∈ Id
BY
{ (Auto THEN OldAutoBoolCase ⌜e <loc e'⌝⋅ THEN OldAutoBoolCase ⌜e' ≤loc e⌝⋅ THEN Try ((RelRST THEN Auto))) }
Latex:
Latex:
\mforall{}[es:EO].  \mforall{}[e,e':E].    e  <loc  e'  \msim{}  \mneg{}\msubb{}e'  \mleq{}loc  e  supposing  loc(e)  =  loc(e')
By
Latex:
(Auto
  THEN  OldAutoBoolCase  \mkleeneopen{}e  <loc  e'\mkleeneclose{}\mcdot{}
  THEN  OldAutoBoolCase  \mkleeneopen{}e'  \mleq{}loc  e\mkleeneclose{}\mcdot{}
  THEN  Try  ((RelRST  THEN  Auto)))
Home
Index