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

`∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .`
`  ∀[Q:{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])+ `⇐⇒` e1 ≤loc e2  ∧ Q[e2]))`

Proof

Definitions occuring in Statement :  es-pplus: `[e1,e2]~([a,b].p[a; b])+` es-first-since: `e2 = first e ≥ e1.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` implies: `P `` Q` and: `P ∧ Q` set: `{x:A| B[x]} ` function: `x:A ─→ B[x]` equal: `s = t ∈ T`
Lemmas :  less_than_transitivity1 less_than_irreflexivity int_seg_wf decidable__equal_int subtype_rel-int_seg false_wf le_weakening subtract_wf int_seg_properties le_wf es-le-loc Id_wf es-loc_wf es-le_wf length_wf es-interval_wf equal_wf all_wf es-pplus_wf es-first-since_wf decidable__lt not-equal-2 condition-implies-le minus-add minus-minus minus-one-mul add-swap add-commutes add-associates add_functionality_wrt_le zero-add le-add-cancel-alt less-iff-le le-add-cancel lelt_wf es-E_wf set_wf less_than_wf primrec-wf2 decidable__le not-le-2 sq_stable__le add-zero add-mul-special zero-mul nat_wf decidable__existse-between1 es-next es-pred-locl es-le_transitivity es-pred_wf es-le_weakening_eq es-locl_transitivity1 es-interval-partition list_wf append_wf es-interval-non-zero length-append es-loc-pred and_wf es-pplus-partition member_wf es-pplus-trivial es-locl_wf length_wf_nat
\mforall{}es:EO.  \mforall{}e1:E.  \mforall{}e2:\{e:E|  loc(e)  =  loc(e1)\}  .
\mforall{}[Q:\{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])+  \mLeftarrow{}{}\mRightarrow{}  e1  \mleq{}loc  e2    \mwedge{}  Q[e2]))

Date html generated: 2015_07_17-AM-08_55_21
Last ObjectModification: 2015_01_27-PM-01_05_25

Home Index