---

Step * 1 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
⊢ (↑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)
BY
{ (GenConclAtAddr [2;1;2;2;1;2;1]⋅ THEN D -2 THEN Reduce 0 THEN Try (Complete (Auto))) }

---

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{}isl(if  isl(w  e)  then  p  outl(w  e)  else  w  e  fi  ))
{}\mRightarrow{}  ((\muparrow{}isl(p  outl(w  e)))  {}\mRightarrow{}  (outl(p  outl(w  e))  <  outl(w  e)))
{}\mRightarrow{}  ((\muparrow{}isl(w  e))  {}\mRightarrow{}  outl(w  e)  c\mleq{}  e)
{}\mRightarrow{}  (outl(if  isl(w  e)  then  p  outl(w  e)  else  w  e  fi  )  <  e)


By

(GenConclAtAddr  [2;1;2;2;1;2;1]\mcdot{}  THEN  D  -2  THEN  Reduce  0  THEN  Try  (Complete  (Auto)))

---

Home Index