### Nuprl Lemma : es-pplus-first-since-exit

`∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .`
`  ∀[Q,R:{e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ].`
`    ((∀e:{e:E| loc(e) = loc(e1) ∈ Id} . Dec(Q[e]))`
`    `` ([e1,e2]~([a,b].b = first e ≥ a.Q[e] ∧ ∀e∈[a,b).¬R[e])+ `⇐⇒` e1 ≤loc e2  ∧ Q[e2] ∧ ∀e∈[e1,e2].R[e] `` Q[e]))`

Proof

Definitions occuring in Statement :  es-pplus: `[e1,e2]~([a,b].p[a; b])+` es-first-since: `e2 = first e ≥ e1.P[e]` alle-between2: `∀e∈[e1,e2].P[e]` alle-between1: `∀e∈[e1,e2).P[e]` es-le: `e ≤loc e' ` es-loc: `loc(e)` es-E: `E` event_ordering: `EO` Id: `Id` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` not: `¬A` implies: `P `` Q` and: `P ∧ Q` set: `{x:A| B[x]} ` function: `x:A ─→ B[x]` equal: `s = t ∈ T`
Lemmas :  es-pplus_wf Id_wf es-loc_wf es-first-since_wf alle-between1_wf not_wf es-le_wf alle-between2_wf all_wf decidable_wf es-E_wf set_wf event_ordering_wf es-pplus_functionality_wrt_implies subtype_rel_sets equal_wf l_member_wf es-interval_wf es-pplus-first-since es-pplus-alle-between2 es-le-loc es-locl_wf member-es-interval es-le_transitivity es-locl_transitivity2 es-le_weakening
\mforall{}es:EO.  \mforall{}e1:E.  \mforall{}e2:\{e:E|  loc(e)  =  loc(e1)\}  .
\mforall{}[Q,R:\{e:E|  loc(e)  =  loc(e1)\}    {}\mrightarrow{}  \mBbbP{}].
((\mforall{}e:\{e:E|  loc(e)  =  loc(e1)\}  .  Dec(Q[e]))
{}\mRightarrow{}  ([e1,e2]\msim{}([a,b].b  =  first  e  \mgeq{}  a.Q[e]  \mwedge{}  \mforall{}e\mmember{}[a,b).\mneg{}R[e])+
\mLeftarrow{}{}\mRightarrow{}  e1  \mleq{}loc  e2    \mwedge{}  Q[e2]  \mwedge{}  \mforall{}e\mmember{}[e1,e2].R[e]  {}\mRightarrow{}  Q[e]))

Date html generated: 2015_07_17-AM-08_55_28
Last ObjectModification: 2015_01_27-PM-01_05_15

Home Index