### Nuprl Lemma : State-loc-comb-trans1

`∀[Info,B,A:Type]. ∀[R:B ─→ B ─→ ℙ].`
`  ∀f:Id ─→ A ─→ B ─→ B. ∀init:Id ─→ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e1,e2:E. ∀v1,v2:B.`
`    (Trans(B;x,y.R[x;y])`
`    `` (∀a:A. ∀e:E.`
`          ((e1 <loc e)`
`          `` e ≤loc e2 `
`          `` a ∈ X(e)`
`          `` (∀s:B. (s ∈ State-loc-comb(init;f;X)(pred(e)) `` R[s;f loc(e) a s]))))`
`    `` single-valued-classrel(es;X;A)`
`    `` single-valued-bag(init loc(e1);B)`
`    `` v1 ∈ State-loc-comb(init;f;X)(e1)`
`    `` v2 ∈ State-loc-comb(init;f;X)(e2)`
`    `` (e1 <loc e2)`
`    `` (∃e:E. ((e1 <loc e) ∧ e ≤loc e2  ∧ (∃a:A. a ∈ X(e))))`
`    `` R[v1;v2])`

Proof

Definitions occuring in Statement :  State-loc-comb: `State-loc-comb(init;f;X)` single-valued-classrel: `single-valued-classrel(es;X;T)` classrel: `v ∈ X(e)` eclass: `EClass(A[eo; e])` event-ordering+: `EO+(Info)` es-le: `e ≤loc e' ` es-locl: `(e <loc e')` es-pred: `pred(e)` es-loc: `loc(e)` es-E: `E` Id: `Id` trans: `Trans(T;x,y.E[x; y])` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` apply: `f a` function: `x:A ─→ B[x]` universe: `Type` single-valued-bag: `single-valued-bag(b;T)` bag: `bag(T)`
Lemmas :  State-loc-comb-classrel-non-loc State-comb-trans1 es-pred_wf es-loc-pred es-locl-first assert_elim btrue_neq_bfalse and_wf equal_wf Id_wf State-comb_wf classrel_wf squash_wf true_wf es-E_wf event-ordering+_subtype event-ordering+_wf eclass_wf assert_wf es-first_wf2 es-le_wf es-locl_wf exists_wf State-loc-comb_wf single-valued-bag_wf es-loc_wf single-valued-classrel_wf all_wf trans_wf bag_wf

Latex:
\mforall{}[Info,B,A:Type].  \mforall{}[R:B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}].
\mforall{}f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B.  \mforall{}init:Id  {}\mrightarrow{}  bag(B).  \mforall{}X:EClass(A).  \mforall{}es:EO+(Info).  \mforall{}e1,e2:E.  \mforall{}v1,v2:B.
(Trans(B;x,y.R[x;y])
{}\mRightarrow{}  (\mforall{}a:A.  \mforall{}e:E.
((e1  <loc  e)
{}\mRightarrow{}  e  \mleq{}loc  e2
{}\mRightarrow{}  a  \mmember{}  X(e)
{}\mRightarrow{}  (\mforall{}s:B.  (s  \mmember{}  State-loc-comb(init;f;X)(pred(e))  {}\mRightarrow{}  R[s;f  loc(e)  a  s]))))
{}\mRightarrow{}  single-valued-classrel(es;X;A)
{}\mRightarrow{}  single-valued-bag(init  loc(e1);B)
{}\mRightarrow{}  v1  \mmember{}  State-loc-comb(init;f;X)(e1)
{}\mRightarrow{}  v2  \mmember{}  State-loc-comb(init;f;X)(e2)
{}\mRightarrow{}  (e1  <loc  e2)
{}\mRightarrow{}  (\mexists{}e:E.  ((e1  <loc  e)  \mwedge{}  e  \mleq{}loc  e2    \mwedge{}  (\mexists{}a:A.  a  \mmember{}  X(e))))
{}\mRightarrow{}  R[v1;v2])

Date html generated: 2015_07_22-PM-00_24_46
Last ObjectModification: 2015_01_28-AM-10_10_17

Home Index