---

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

.....basecase..... 
1. es : EO@i'
2. p : E ─→ (E + Top)@i
3. causal-predecessor(es;p)@i
4. n : ℕ+@i
⊢ ∀e,e':E.  ((p-graph(E;p^1) e' e) ⇒ (e < e'))
BY
{ RepUR ``p-graph p-fun-exp p-compose p-id 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.  (((↑isl(p e')) c∧ (e = outl(p e') ∈ E)) ⇒ (e < e'))

---

Latex:


.....basecase..... 
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.    ((p-graph(E;p\^{}1)  e'  e)  {}\mRightarrow{}  (e  <  e'))


By

RepUR  ``p-graph  p-fun-exp  p-compose  p-id  can-apply  do-apply``  0

---

Home Index