Nuprl 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]) ∈ ℙ)


Proof




Definitions occuring in Statement :  es-first-at-since': es-first-at-since'(es;i;e;e.R[e];e.P[e]) es-loc: loc(e) es-E: E event_ordering: EO Id: Id uall: [x:A]. B[x] prop: so_apply: x[s] member: t ∈ T set: {x:A| B[x]}  function: x:A ─→ B[x] equal: t ∈ T
Lemmas :  es-loc_wf exists_wf es-locl_wf all_wf es-le_wf not_wf es-le-loc es-E_wf Id_wf event_ordering_wf
\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{})



Date html generated: 2015_07_17-AM-08_50_32
Last ObjectModification: 2015_01_27-PM-01_19_45

Home Index