---

Step * 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.  (((↑isl(p e')) c∧ (e = outl(p e') ∈ E)) ⇒ (e < e'))
BY
{ Folds ``can-apply do-apply`` 0 }

1
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'))

---

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{}isl(p  e'))  c\mwedge{}  (e  =  outl(p  e')))  {}\mRightarrow{}  (e  <  e'))


By

Folds  ``can-apply  do-apply``  0

---

Home Index