Nuprl Lemma : alle-between1-not-first-since

[es:EO]. ∀[e1:E]. ∀[e2:{e:E| loc(e) loc(e1) ∈ Id} ]. ∀[p:{e:E| loc(e) loc(e1) ∈ Id}  ─→ ℙ].
  uiff(∀e∈[e1,e2).¬first e ≥ e1.p[e];∀e∈[e1,e2).¬p[e])


Proof




Definitions occuring in Statement :  es-first-since: e2 first e ≥ e1.P[e] alle-between1: e∈[e1,e2).P[e] es-loc: loc(e) es-E: E event_ordering: EO Id: Id uiff: uiff(P;Q) uall: [x:A]. B[x] prop: so_apply: x[s] not: ¬A set: {x:A| B[x]}  function: x:A ─→ B[x] equal: t ∈ T
Lemmas :  es-le_wf es-locl_wf not_wf es-le-loc Id_wf es-loc_wf es-E_wf all_wf es-locl-wellfnd es-locl_transitivity2 es-le_weakening es-first-since_wf
\mforall{}[es:EO].  \mforall{}[e1:E].  \mforall{}[e2:\{e:E|  loc(e)  =  loc(e1)\}  ].  \mforall{}[p:\{e:E|  loc(e)  =  loc(e1)\}    {}\mrightarrow{}  \mBbbP{}].
    uiff(\mforall{}e\mmember{}[e1,e2).\mneg{}e  =  first  e  \mgeq{}  e1.p[e];\mforall{}e\mmember{}[e1,e2).\mneg{}p[e])



Date html generated: 2015_07_17-AM-08_53_17
Last ObjectModification: 2015_01_27-PM-01_19_25

Home Index