---

Step * of Lemma es-first-at-since_wf

∀[es:EO]. ∀[i:Id]. ∀[e':E]. ∀[P,R:{e:E| loc(e) = i ∈ Id}  ─→ ℙ].  (es-first-at-since(es;i;e';e.R[e];e.P[e]) ∈ ℙ)
BY
{ ((Auto THEN Unfold `es-first-at-since` 0 THEN UnivCD) THENA Auto) }

1
1. es : EO
2. i : Id
3. e' : E
4. P : {e:E| loc(e) = i ∈ Id}  ─→ ℙ
5. R : {e:E| loc(e) = i ∈ Id}  ─→ ℙ
⊢ (loc(e') = i ∈ Id) ∧ (P[e'] ∧ (¬R[e'])) ∧ ∀e'@0<e'.P[e'@0] ⇒ (∃e'':E. (e'@0 ≤loc e''  ∧ (e'' <loc e') ∧ R[e''])) ∈ ℙ

---

Latex:


\mforall{}[es:EO].  \mforall{}[i:Id].  \mforall{}[e':E].  \mforall{}[P,R:\{e:E|  loc(e)  =  i\}    {}\mrightarrow{}  \mBbbP{}].
    (es-first-at-since(es;i;e';e.R[e];e.P[e])  \mmember{}  \mBbbP{})


By

((Auto  THEN  Unfold  `es-first-at-since`  0  THEN  UnivCD)  THENA  Auto)

---

Home Index