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:  Q implies:  Q set: {x:A| B[x]}  function: x:A ⟶ B[x] equal: t ∈ T
Definitions unfolded in proof :  rev_implies:  Q

Latex:
\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: 2016_05_16-AM-09_55_53
Last ObjectModification: 2015_12_28-PM-09_31_17

Theory : new!event-ordering


Home Index