### Nuprl Lemma : es-pstar-q-partition

`∀es:EO. ∀e1,e2,b:E.`
`  ∀[Q,P:{e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ].`
`    ((e1 <loc b)`
`    `` b ≤loc e2 `
`    `` [e1;pred(b)]~([a,b].P[a;b])*[a,b].P[a;b]`
`    `` [b;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-le: `e ≤loc e' ` es-locl: `(e <loc e')` es-pred: `pred(e)` es-loc: `loc(e)` es-E: `E` event_ordering: `EO` Id: `Id` uall: `∀[x:A]. B[x]` prop: `ℙ` 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 :  exists_wf int_seg_wf false_wf lelt_wf es-le_wf subtract_wf decidable__le not-le-2 less-iff-le condition-implies-le minus-one-mul zero-add minus-add minus-minus add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel subtract-is-less all_wf es-locl_wf decidable__lt le-add-cancel2 sq_stable__le es-le-loc Id_wf es-loc_wf es-pstar-q_wf es-E_wf es-loc-pred es-locl-first assert_elim btrue_neq_bfalse assert_wf es-first_wf2 es-pred_wf lt_int_wf bool_wf equal-wf-T-base less_than_wf le_int_wf le_wf bnot_wf zero-le-nat subtype_rel_sets equal_wf uiff_transitivity eqtt_to_assert assert_of_lt_int eqff_to_assert assert_functionality_wrt_uiff bnot_of_lt_int assert_of_le_int bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot add-mul-special zero-mul and_wf int_subtype_base general_arith_equation1 int_seg_properties squash_wf not_wf member_wf es-le-trans2 es-pred-locl iff_weakening_equal set_wf
\mforall{}es:EO.  \mforall{}e1,e2,b:E.
\mforall{}[Q,P:\{e:E|  loc(e)  =  loc(e1)\}    {}\mrightarrow{}  \{e:E|  loc(e)  =  loc(e1)\}    {}\mrightarrow{}  \mBbbP{}].
((e1  <loc  b)
{}\mRightarrow{}  b  \mleq{}loc  e2
{}\mRightarrow{}  [e1;pred(b)]\msim{}([a,b].P[a;b])*[a,b].P[a;b]
{}\mRightarrow{}  [b;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_54_35
Last ObjectModification: 2015_02_04-PM-06_30_06

Home Index