### Nuprl Lemma : alle-between2-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].¬e = 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-between2: `∀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: `s = t ∈ T`
Lemmas :  es-le_wf not_wf es-le-loc Id_wf es-loc_wf es-E_wf all_wf es-locl_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_22
Last ObjectModification: 2015_01_27-PM-01_18_59

Home Index