### Nuprl Lemma : es-pplus_functionality_wrt_rev_implies

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

Proof

Definitions occuring in Statement :  es-pplus: `[e1,e2]~([a,b].p[a; b])+` es-interval: `[e, e']` es-loc: `loc(e)` es-E: `E` event_ordering: `EO` Id: `Id` l_member: `(x ∈ l)` uall: `∀[x:A]. B[x]` prop: `ℙ` guard: `{T}` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` rev_implies: `P `` Q` implies: `P `` Q` set: `{x:A| B[x]} ` function: `x:A ─→ B[x]` equal: `s = t ∈ T`
Lemmas :  es-pstar-q_functionality_wrt_rev_implies all_wf es-E_wf Id_wf es-loc_wf l_member_wf es-interval_wf rev_implies_wf set_wf event_ordering_wf
\mforall{}es:EO.  \mforall{}e1:E.  \mforall{}e2:\{e:E|  loc(e)  =  loc(e1)\}  .
\mforall{}[p,p':\{e:E|  loc(e)  =  loc(e1)\}    {}\mrightarrow{}  \{e:E|  loc(e)  =  loc(e1)\}    {}\mrightarrow{}  \mBbbP{}].
((\mforall{}a,b:\{e:E|  loc(e)  =  loc(e1)\}  .    ((a  \mmember{}  [e1,  e2])  {}\mRightarrow{}  (b  \mmember{}  [e1,  e2])  {}\mRightarrow{}  \{p[a;b]  \mLeftarrow{}{}  p'[a;b]\}))
{}\mRightarrow{}  \{[e1,e2]\msim{}([a,b].p[a;b])+  \mLeftarrow{}{}  [e1,e2]\msim{}([a,b].p'[a;b])+\})

Date html generated: 2015_07_17-AM-08_54_48
Last ObjectModification: 2015_01_27-PM-01_18_23

Home Index