---

Step * of Lemma es-le-before-split-last

∀[es:EO]. ∀[e:E].  ≤loc(e) ~ ≤loc(pred(e)) @ [e] supposing ¬↑first(e)
BY
{ (Auto THEN UnfoldAtAddr [1] 0 THEN MemCD THEN Try (Complete (Auto)) THEN RWO "es-le-before-pred" 0 THEN Auto) }

---

Latex:


\mforall{}[es:EO].  \mforall{}[e:E].    \mleq{}loc(e)  \msim{}  \mleq{}loc(pred(e))  @  [e]  supposing  \mneg{}\muparrow{}first(e)


By

(Auto
  THEN  UnfoldAtAddr  [1]  0
  THEN  MemCD
  THEN  Try  (Complete  (Auto))
  THEN  RWO  "es-le-before-pred"  0
  THEN  Auto)

---

Home Index