Step
*
of Lemma
es-first-since_wf
∀[es:EO]. ∀[e1:E]. ∀[e2:{e:E| loc(e) = loc(e1) ∈ Id} ]. ∀[p:{e:E| loc(e) = loc(e1) ∈ Id} ─→ ℙ].
(e2 = first e ≥ e1.p[e] ∈ ℙ)
BY
{ (Auto THEN Unfold `es-first-since` 0 THEN Auto) }
Latex:
\mforall{}[es:EO]. \mforall{}[e1:E]. \mforall{}[e2:\{e:E| loc(e) = loc(e1)\} ]. \mforall{}[p:\{e:E| loc(e) = loc(e1)\} {}\mrightarrow{} \mBbbP{}].
(e2 = first e \mgeq{} e1.p[e] \mmember{} \mBbbP{})
By
(Auto THEN Unfold `es-first-since` 0 THEN Auto)
Home
Index