---

Step * of Lemma eo-forward-not-first2

∀[Info:Type]. ∀eo:EO+(Info). ∀e:E. ∀e':{e':E| e' ≤loc e } .  uiff(¬↑first(e);(e' <loc e))
BY
{ ((UnivCD THENA Auto) THEN (RWO "eo-forward-first2" 0 THENA Auto) THEN D (-1) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}eo:EO+(Info).  \mforall{}e:E.  \mforall{}e':\{e':E|  e'  \mleq{}loc  e  \}  .    uiff(\mneg{}\muparrow{}first(e);(e'  <loc  e))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (RWO  "eo-forward-first2"  0  THENA  Auto)  THEN  D  (-1)  THEN  Auto)

---

Home Index