### Nuprl Lemma : es-pstar-q_functionality_wrt_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]` implies: `P `` Q` set: `{x:A| B[x]} ` function: `x:A ─→ B[x]` equal: `s = t ∈ T`
Lemmas :  es-pstar-q_wf decidable__lt false_wf less-iff-le condition-implies-le add-associates minus-add minus-one-mul add-swap add-commutes add_functionality_wrt_le le-add-cancel2 lelt_wf decidable__le not-le-2 sq_stable__le zero-add add-zero le-add-cancel es-loc-pred assert_elim es-first_wf2 es-locl-first btrue_neq_bfalse assert_wf es-pred_wf Id_wf es-loc_wf es-locl_wf equal_wf int_seg_wf subtract_wf minus-minus subtract-is-less es-le_wf all_wf exists_wf es-E_wf l_member_wf es-interval_wf set_wf event_ordering_wf es-increasing-sequence2 subtype_rel_dep_function less_than_transitivity2 le_weakening2 member-es-interval squash_wf true_wf iff_weakening_equal es-le_transitivity es-le-pred es-le_weakening_eq es-locl_transitivity1 es-pred-locl es-locl_transitivity2 subtype_base_sq bool_subtype_base bool_wf es-le-self
\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]  {}\mRightarrow{}  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]  {}\mRightarrow{}  q'[a;b]\}))
{}\mRightarrow{}  \{[e1;e2]\msim{}([a,b].p[a;b])*[a,b].q[a;b]  {}\mRightarrow{}  [e1;e2]\msim{}([a,b].p'[a;b])*[a,b].q'[a;b]\})

Date html generated: 2015_07_17-AM-08_53_50
Last ObjectModification: 2015_02_04-PM-06_30_18

Home Index