---

Step * 1 1 1 of Lemma causal-pred-wellfounded


1. es : EO@i'
2. p : E ─→ (E + Top)@i
3. ∀e:E. ((↑can-apply(p;e)) ⇒ (do-apply(p;e) < e))@i
⊢ ∀x,y:E.  (((↑can-apply(p;y)) c∧ (x = do-apply(p;y) ∈ E)) ⇒ (x < y))
BY
{ Auto }

---

Latex:



1.  es  :  EO@i'
2.  p  :  E  {}\mrightarrow{}  (E  +  Top)@i
3.  \mforall{}e:E.  ((\muparrow{}can-apply(p;e))  {}\mRightarrow{}  (do-apply(p;e)  <  e))@i
\mvdash{}  \mforall{}x,y:E.    (((\muparrow{}can-apply(p;y))  c\mwedge{}  (x  =  do-apply(p;y)))  {}\mRightarrow{}  (x  <  y))


By

Auto

---

Home Index