---

Step * 1 1 of Lemma p-compose-causal-predecessor1


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
⊢ (↑can-apply(p o w;e))
⇒ ((↑can-apply(p;do-apply(w;e))) ⇒ (do-apply(p;do-apply(w;e)) < do-apply(w;e)))
⇒ ((↑can-apply(w;e)) ⇒ do-apply(w;e) c≤ e)
⇒ (do-apply(p o w;e) < e)
BY
{ RepUR ``can-apply do-apply p-compose`` 0⋅ }

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
⊢ (↑isl(if isl(w e) then p outl(w e) else w e fi ))
⇒ ((↑isl(p outl(w e))) ⇒ (outl(p outl(w e)) < outl(w e)))
⇒ ((↑isl(w e)) ⇒ outl(w e) c≤ e)
⇒ (outl(if isl(w e) then p outl(w e) else w e fi ) < e)

---

Latex:



1.  es  :  EO@i'
2.  p  :  E  {}\mrightarrow{}  (E  +  Top)@i
3.  w  :  E  {}\mrightarrow{}  (E  +  Top)@i
4.  \mforall{}e:E.  ((\muparrow{}can-apply(p;e))  {}\mRightarrow{}  (do-apply(p;e)  <  e))@i
5.  \mforall{}e:E.  ((\muparrow{}can-apply(w;e))  {}\mRightarrow{}  do-apply(w;e)  c\mleq{}  e)@i
6.  e  :  E@i
\mvdash{}  (\muparrow{}can-apply(p  o  w;e))
{}\mRightarrow{}  ((\muparrow{}can-apply(p;do-apply(w;e)))  {}\mRightarrow{}  (do-apply(p;do-apply(w;e))  <  do-apply(w;e)))
{}\mRightarrow{}  ((\muparrow{}can-apply(w;e))  {}\mRightarrow{}  do-apply(w;e)  c\mleq{}  e)
{}\mRightarrow{}  (do-apply(p  o  w;e)  <  e)


By

RepUR  ``can-apply  do-apply  p-compose``  0\mcdot{}

---

Home Index