---

Step * of Lemma es-causl_weakening_p-locl

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

1
1. es : EO@i'
2. p : E ─→ (E + Top)@i
3. causal-predecessor(es;p)@i
4. e : E@i
5. e' : E@i
6. e p< e'@i
⊢ (e < e')

---

Latex:


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


By

Auto

---

Home Index