### Nuprl Lemma : es-pplus_wf

`∀[es:EO]. ∀[e1:E]. ∀[e2:{e:E| loc(e) = loc(e1) ∈ Id} ]. ∀[p:{e:E| loc(e) = loc(e1) ∈ Id} `
`                                                           ─→ {e:E| loc(e) = loc(e1) ∈ Id} `
`                                                           ─→ ℙ].`
`  ([e1,e2]~([a,b].p[a;b])+ ∈ ℙ)`

Proof

Definitions occuring in Statement :  es-pplus: `[e1,e2]~([a,b].p[a; b])+` es-loc: `loc(e)` es-E: `E` event_ordering: `EO` Id: `Id` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` member: `t ∈ T` set: `{x:A| B[x]} ` function: `x:A ─→ B[x]` equal: `s = t ∈ T`
Lemmas :  es-pstar-q_wf Id_wf es-loc_wf es-E_wf set_wf event_ordering_wf
\mforall{}[es:EO].  \mforall{}[e1:E].  \mforall{}[e2:\{e:E|  loc(e)  =  loc(e1)\}  ].  \mforall{}[p:\{e:E|  loc(e)  =  loc(e1)\}
{}\mrightarrow{}  \{e:E|  loc(e)  =  loc(e1)\}
{}\mrightarrow{}  \mBbbP{}].
([e1,e2]\msim{}([a,b].p[a;b])+  \mmember{}  \mBbbP{})

Date html generated: 2015_07_17-AM-08_54_42
Last ObjectModification: 2015_01_27-PM-01_16_00

Home Index