---

Step * 1 1 of Lemma causal-pred-wellfounded


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

1
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))

---

Latex:



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


By

Unfold  `causal-predecessor`  -1

---

Home Index