---

Step * 1 1 1 1 1 1 of Lemma es-causl_weakening_p-locl


1. es : EO@i'
2. p : E ─→ (E + Top)@i
3. causal-predecessor(es;p)@i
4. n : ℕ+@i
⊢ ∀e,e':E.  (((↑can-apply(p;e')) c∧ (e = do-apply(p;e') ∈ E)) ⇒ (e < e'))
BY
{ (Auto THEN Unfold `causal-predecessor` 3) }

---

Latex:



1.  es  :  EO@i'
2.  p  :  E  {}\mrightarrow{}  (E  +  Top)@i
3.  causal-predecessor(es;p)@i
4.  n  :  \mBbbN{}\msupplus{}@i
\mvdash{}  \mforall{}e,e':E.    (((\muparrow{}can-apply(p;e'))  c\mwedge{}  (e  =  do-apply(p;e')))  {}\mRightarrow{}  (e  <  e'))


By

(Auto  THEN  Unfold  `causal-predecessor`  3)

---

Home Index