### Nuprl Lemma : State-comb-progress

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

Proof

Definitions occuring in Statement :  State-comb: `State-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])` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` implies: `P `` Q` and: `P ∧ Q` apply: `f a` function: `x:A ─→ B[x]` universe: `Type` equal: `s = t ∈ T` single-valued-bag: `single-valued-bag(b;T)` bag: `bag(T)`
Lemmas :  iterated-classrel-progress State-comb-classrel es-pred_wf iterated-classrel-iff es-locl-first assert_elim btrue_neq_bfalse assert_wf es-first_wf2 not_wf iterated-classrel_wf classrel_wf es-le_wf es-locl_wf sq_stable__single-valued-iterated-classrel and_wf equal_wf Id_wf bag_wf single-valued-bag_wf es-loc-pred exists_wf es-E_wf event-ordering+_subtype State-comb_wf es-loc_wf single-valued-classrel_wf all_wf trans_wf decidable_wf event-ordering+_wf eclass_wf

Latex:
\mforall{}[Info,B,A:Type].
\mforall{}R:B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}.  \mforall{}P:A  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}.  \mforall{}f: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.
((\mforall{}a:A.  \mforall{}s:B.    Dec(P[a;s]))
{}\mRightarrow{}  Trans(B;x,y.R[x;y])
{}\mRightarrow{}  (\mforall{}a:A.  \mforall{}e:E.  \mforall{}s:B.
((e1  <loc  e)
{}\mRightarrow{}  e  \mleq{}loc  e2
{}\mRightarrow{}  a  \mmember{}  X(e)
{}\mRightarrow{}  s  \mmember{}  State-comb(init;f;X)(pred(e))
{}\mRightarrow{}  ((P[a;s]  {}\mRightarrow{}  R[s;f  a  s])  \mwedge{}  ((\mneg{}P[a;s])  {}\mRightarrow{}  (s  =  (f  a  s))))))
{}\mRightarrow{}  single-valued-classrel(es;X;A)
{}\mRightarrow{}  single-valued-bag(init  loc(e1);B)
{}\mRightarrow{}  v1  \mmember{}  State-comb(init;f;X)(e1)
{}\mRightarrow{}  v2  \mmember{}  State-comb(init;f;X)(e2)
{}\mRightarrow{}  (e1  <loc  e2)
{}\mRightarrow{}  (\mexists{}e:E
\mexists{}a:A
\mexists{}s:B.  ((e1  <loc  e)  \mwedge{}  e  \mleq{}loc  e2    \mwedge{}  s  \mmember{}  State-comb(init;f;X)(pred(e))  \mwedge{}  a  \mmember{}  X(e)  \mwedge{}  P[a;s]))
{}\mRightarrow{}  R[v1;v2])

Date html generated: 2015_07_22-PM-00_22_42
Last ObjectModification: 2015_01_28-AM-10_14_28

Home Index