---

Step * 1 1 1 2 1 2 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
5. 0 < n
6. ∀e,e':E.  ((p-graph(E;p^n) e' e) ⇒ (e < e'))@i
7. e : E@i
8. e' : E@i
9. p-graph(E;p^n + 1) e' e@i
10. ↑can-apply(p;e')
⊢ (e < e')
BY
{ Assert ⌈(e < do-apply(p;e')) ∧ (do-apply(p;e') < e')⌉⋅ }

1
.....assertion..... 
1. es : EO@i'
2. p : E ─→ (E + Top)@i
3. causal-predecessor(es;p)@i
4. n : ℤ@i
5. 0 < n
6. ∀e,e':E.  ((p-graph(E;p^n) e' e) ⇒ (e < e'))@i
7. e : E@i
8. e' : E@i
9. p-graph(E;p^n + 1) e' e@i
10. ↑can-apply(p;e')
⊢ (e < do-apply(p;e')) ∧ (do-apply(p;e') < e')

2
1. es : EO@i'
2. p : E ─→ (E + Top)@i
3. causal-predecessor(es;p)@i
4. n : ℤ@i
5. 0 < n
6. ∀e,e':E.  ((p-graph(E;p^n) e' e) ⇒ (e < e'))@i
7. e : E@i
8. e' : E@i
9. p-graph(E;p^n + 1) e' e@i
10. ↑can-apply(p;e')
11. (e < do-apply(p;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  :  \mBbbZ{}@i
5.  0  <  n
6.  \mforall{}e,e':E.    ((p-graph(E;p\^{}n)  e'  e)  {}\mRightarrow{}  (e  <  e'))@i
7.  e  :  E@i
8.  e'  :  E@i
9.  p-graph(E;p\^{}n  +  1)  e'  e@i
10.  \muparrow{}can-apply(p;e')
\mvdash{}  (e  <  e')


By

Assert  \mkleeneopen{}(e  <  do-apply(p;e'))  \mwedge{}  (do-apply(p;e')  <  e')\mkleeneclose{}\mcdot{}

---

Home Index