---

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:


\mforall{}[es:EO].  \mforall{}[e,e':E].    e  <loc  e'  \msim{}  \mneg{}\msubb{}e'  \mleq{}loc  e  supposing  loc(e)  =  loc(e')


By

(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