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:
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
Latex:
((Auto THEN Unfold `es-first-at-since` 0 THEN UnivCD) THENA Auto)
Home
Index