---

Step * of Lemma p-compose-causal-predecessor1

∀es:EO. ∀p,w:E ─→ (E + Top).
  (causal-predecessor(es;p) ⇒ causal-weak-predecessor(es;w) ⇒ causal-predecessor(es;p o w))
BY
{ (Unfolds ``causal-predecessor causal-weak-predecessor`` 0 THEN Auto) }

1
1. es : EO@i'
2. p : E ─→ (E + Top)@i
3. w : E ─→ (E + Top)@i
4. ∀e:E. ((↑can-apply(p;e)) ⇒ (do-apply(p;e) < e))@i
5. ∀e:E. ((↑can-apply(w;e)) ⇒ do-apply(w;e) c≤ e)@i
6. e : E@i
7. ↑can-apply(p o w;e)@i
⊢ (do-apply(p o w;e) < e)

---

Latex:


\mforall{}es:EO.  \mforall{}p,w:E  {}\mrightarrow{}  (E  +  Top).
    (causal-predecessor(es;p)  {}\mRightarrow{}  causal-weak-predecessor(es;w)  {}\mRightarrow{}  causal-predecessor(es;p  o  w))


By

(Unfolds  ``causal-predecessor  causal-weak-predecessor``  0  THEN  Auto)

---

Home Index