---

Step * of Lemma es-le-before-pred

∀[es:EO]. ∀[e:E].  ≤loc(pred(e)) ~ before(e) supposing ¬↑first(e)
BY
{ ((UnivCD THENA Auto) THEN RecUnfold `es-before` 0 THEN AutoSplit THEN Fold `es-le-before` 0 THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RecUnfold  `es-before`  0
  THEN  AutoSplit
  THEN  Fold  `es-le-before`  0
  THEN  Auto)

---

Home Index