---

Step * of Lemma es-causl-p-locl-test

∀es:EO. ∀p:E ─→ (E + Top).  (causal-predecessor(es;p) ⇒ (∀e,e',a,b:E.  (a c≤ e ⇒ e p≤ e' ⇒ e' p< b ⇒ (a < b))))
BY
{ Auto }

---

Latex:


\mforall{}es:EO.  \mforall{}p:E  {}\mrightarrow{}  (E  +  Top).
    (causal-predecessor(es;p)  {}\mRightarrow{}  (\mforall{}e,e',a,b:E.    (a  c\mleq{}  e  {}\mRightarrow{}  e  p\mleq{}  e'  {}\mRightarrow{}  e'  p<  b  {}\mRightarrow{}  (a  <  b))))


By

Auto

---

Home Index