---

Step * of Lemma causal-pred-wellfounded

∀es:EO. ∀p:E ⟶ (E + Top).  (causal-predecessor(es;p) ⇒ SWellFounded(p-graph(E;p) y x))
BY
{ ((Auto THEN Using [`R1',⌜λ2x y.(x < y)⌝] (BackThruLemma `strongwf-monotone`)⋅) THEN Auto) }

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

---

Latex:

---

Latex:
\mforall{}es:EO.  \mforall{}p:E  {}\mrightarrow{}  (E  +  Top).    (causal-predecessor(es;p)  {}\mRightarrow{}  SWellFounded(p-graph(E;p)  y  x))


By

---

Latex:
((Auto  THEN  Using  [`R1',\mkleeneopen{}\mlambda{}\msubtwo{}x  y.(x  <  y)\mkleeneclose{}]  (BackThruLemma  `strongwf-monotone`)\mcdot{})  THEN  Auto)

---

Home Index