Proof of Nuprl Lemma : causal-pred-wellfounded

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',⌈λ₂x 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
⊢ λ₂x y.p-graph(E;p) y x => λ₂x y.(x < y)

Latex:

\mforall{}es:EO. \mforall{}p:E {}\mrightarrow{} (E + Top). (causal-predecessor(es;p) {}\mRightarrow{} SWellFounded(p-graph(E;p) y x)) By ((Auto THEN Using [`R1',\mkleeneopen{}\mlambda{}\msubtwo{}x y.(x < y)\mkleeneclose{}] (BackThruLemma `strongwf-monotone`)\mcdot{}) THEN Auto) Home Index