---

Step * of Lemma eo-forward-causle

∀[Info:Type]. ∀[eo:EO+(Info)]. ∀[e,e1,e2:E].
  e1 c≤ e2 ⇐⇒ e1 c≤ e2 supposing ((loc(e1) = loc(e) ∈ Id) ⇒ e ≤loc e1 ) ∧ ((loc(e2) = loc(e) ∈ Id) ⇒ e ≤loc e2 )
BY
{ (Auto
   THEN Try (Unfold `label` 0)
   THEN RepeatFor 2 (ParallelLast)
   THEN RWW "eo-forward-less" (-1)
   THEN Auto
   THEN RWW "eo-forward-less" 0⋅
   THEN Auto) }

---

Latex:


\mforall{}[Info:Type].  \mforall{}[eo:EO+(Info)].  \mforall{}[e,e1,e2:E].
    e1  c\mleq{}  e2  \mLeftarrow{}{}\mRightarrow{}  e1  c\mleq{}  e2 
    supposing  ((loc(e1)  =  loc(e))  {}\mRightarrow{}  e  \mleq{}loc  e1  )  \mwedge{}  ((loc(e2)  =  loc(e))  {}\mRightarrow{}  e  \mleq{}loc  e2  )


By

(Auto
  THEN  Try  (Unfold  `label`  0)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  RWW  "eo-forward-less"  (-1)
  THEN  Auto
  THEN  RWW  "eo-forward-less"  0\mcdot{}
  THEN  Auto)

---

Home Index