---

Step * 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. e : E@i
5. e' : E@i
6. ∃n:ℕ+. (p-graph(E;p^n) e' e)@i
⊢ (e < e')
BY
{ (D -1 THEN skip{NatInd (-2)⋅}) }

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 : ℕ+@i
7. 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.  \mexists{}n:\mBbbN{}\msupplus{}.  (p-graph(E;p\^{}n)  e'  e)@i
\mvdash{}  (e  <  e')


By

(D  -1  THEN  skip\{NatInd  (-2)\mcdot{}\})

---

Home Index