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