### Nuprl Lemma : es-pstar-q_functionality_wrt_rev_implies

`∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .`
`  ∀[p',q',p,q:{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]}))`
`    `` (∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) `` (b ∈ [e1, e2]) `` {q[a;b] `` q'[a;b]}))`
`    `` {[e1;e2]~([a,b].p[a;b])*[a,b].q[a;b] `` [e1;e2]~([a,b].p'[a;b])*[a,b].q'[a;b]})`

Proof

Definitions occuring in Statement :  es-pstar-q: `[e1;e2]~([a,b].p[a; b])*[a,b].q[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_implies
\mforall{}es:EO.  \mforall{}e1:E.  \mforall{}e2:\{e:E|  loc(e)  =  loc(e1)\}  .
\mforall{}[p',q',p,q:\{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{}  (\mforall{}a,b:\{e:E|  loc(e)  =  loc(e1)\}  .    ((a  \mmember{}  [e1,  e2])  {}\mRightarrow{}  (b  \mmember{}  [e1,  e2])  {}\mRightarrow{}  \{q[a;b]  \mLeftarrow{}{}  q'[a;b]\}))
{}\mRightarrow{}  \{[e1;e2]\msim{}([a,b].p[a;b])*[a,b].q[a;b]  \mLeftarrow{}{}  [e1;e2]\msim{}([a,b].p'[a;b])*[a,b].q'[a;b]\})

Date html generated: 2015_07_17-AM-08_53_53
Last ObjectModification: 2015_01_27-PM-01_15_55

Home Index