---

Step * 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. e : E@i
5. e' : E@i
6. e p< e'@i
⊢ (e < e')
BY
{ Unfold `es-p-locl` (-1) }

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. ∃n:ℕ+. (p-graph(E;p^n) e' e)@i
⊢ (e < e')

---

Latex:



1.  es  :  EO@i'
2.  p  :  E  {}\mrightarrow{}  (E  +  Top)@i
3.  causal-predecessor(es;p)@i
4.  e  :  E@i
5.  e'  :  E@i
6.  e  p<  e'@i
\mvdash{}  (e  <  e')


By

Unfold  `es-p-locl`  (-1)

---

Home Index