---

Step * 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
7. ↑can-apply(p o w;e)@i
⊢ (do-apply(p o w;e) < e)
BY
{ ((SimpleInstHyp ⌈e⌉ (-3)⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN ((SimpleInstHyp ⌈do-apply(w;e)⌉ (-4)⋅
          THENA (Auto
                 THEN (MoveToConcl (-1)
                       ⋅
                       THEN RepUR ``can-apply do-apply p-compose`` 0
                       THEN (GenConclAtAddr [2;1;1] THENM (D -2 THEN Reduce 0))
                       THEN Auto)⋅
                 )
          )
         THEN RepeatFor 2 (MoveToConcl (-1))
         )⋅) }

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
⊢ (↑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)

---

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
7.  \muparrow{}can-apply(p  o  w;e)@i
\mvdash{}  (do-apply(p  o  w;e)  <  e)


By

((SimpleInstHyp  \mkleeneopen{}e\mkleeneclose{}  (-3)\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  ((SimpleInstHyp  \mkleeneopen{}do-apply(w;e)\mkleeneclose{}  (-4)\mcdot{}
                THENA  (Auto
                              THEN  (MoveToConcl  (-1)
                                          \mcdot{}
                                          THEN  RepUR  ``can-apply  do-apply  p-compose``  0
                                          THEN  (GenConclAtAddr  [2;1;1]  THENM  (D  -2  THEN  Reduce  0))
                                          THEN  Auto)\mcdot{}
                              )
                )
              THEN  RepeatFor  2  (MoveToConcl  (-1))
              )\mcdot{})

---

Home Index