---

Step * 1 of Lemma causal-pred-wellfounded


1. es : EO@i'
2. p : E ─→ (E + Top)@i
3. causal-predecessor(es;p)@i
⊢ λ2x y.p-graph(E;p) y x => λ2x y.(x < y)
BY
{ RepUR ``rel_implies so_lambda p-graph`` 0 }

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

---

Latex:



1.  es  :  EO@i'
2.  p  :  E  {}\mrightarrow{}  (E  +  Top)@i
3.  causal-predecessor(es;p)@i
\mvdash{}  \mlambda{}\msubtwo{}x  y.p-graph(E;p)  y  x  =>  \mlambda{}\msubtwo{}x  y.(x  <  y)


By

RepUR  ``rel\_implies  so\_lambda  p-graph``  0

---

Home Index