---

Step * of Lemma eo-forward-E-member

∀[Info:Type]. ∀eo:EO+(Info). ∀e:E. ∀e':E.  ((e' ∈ E) ∧ ((loc(e') = loc(e) ∈ Id) ⇒ e ≤loc e' ))
BY
{ (Auto
   THEN (RWO "eo-forward-E" (-3)⋅ THENA Auto)
   THEN D -3
   THEN Unhide
   THEN Auto
   THEN RW assert_pushdownC (-3)⋅
   THEN Auto
   THEN D -3
   THEN Auto) }

---

Latex:


\mforall{}[Info:Type].  \mforall{}eo:EO+(Info).  \mforall{}e:E.  \mforall{}e':E.    ((e'  \mmember{}  E)  \mwedge{}  ((loc(e')  =  loc(e))  {}\mRightarrow{}  e  \mleq{}loc  e'  ))


By

(Auto
  THEN  (RWO  "eo-forward-E"  (-3)\mcdot{}  THENA  Auto)
  THEN  D  -3
  THEN  Unhide
  THEN  Auto
  THEN  RW  assert\_pushdownC  (-3)\mcdot{}
  THEN  Auto
  THEN  D  -3
  THEN  Auto)

---

Home Index