### Nuprl Lemma : State-loc-comb-invariant-sv2

`∀[Info,A,S:Type].`
`  ∀es:EO+(Info). ∀P:E ─→ S ─→ ℙ. ∀init:Id ─→ bag(S). ∀f:Id ─→ A ─→ S ─→ S. ∀X:EClass(A). ∀e:E. ∀v:S.`
`    (single-valued-bag(init loc(e);S)`
`    `` single-valued-classrel(es;X;A)`
`    `` (∀s:S. ∀e':E.`
`          (e' ≤loc e `
`          `` if first(e') then s ↓∈ init loc(e') else s ∈ State-loc-comb(init;f;X)(pred(e')) ∧ P[pred(e');s] fi `
`          `` if e' ∈b X then ∀a:A. (a ∈ X(e') `` P[e';f loc(e') a s]) else P[e';s] fi ))`
`    `` v ∈ State-loc-comb(init;f;X)(e)`
`    `` P[e;v])`

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)` member-eclass: `e ∈b X` eclass: `EClass(A[eo; e])` event-ordering+: `EO+(Info)` es-le: `e ≤loc e' ` es-first: `first(e)` es-pred: `pred(e)` es-loc: `loc(e)` es-E: `E` Id: `Id` ifthenelse: `if b then t else f fi ` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` all: `∀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-member: `x ↓∈ bs` bag: `bag(T)`
Lemmas :  member-eclass_wf bool_wf eqtt_to_assert eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot bool_cases es-first_wf2 event-ordering+_subtype assert_of_bnot State-loc-comb-classrel2 es-pred_wf es-le-loc es-loc-pred and_wf Id_wf iterated-classrel_wf bag-member_wf es-loc_wf sq_stable__single-valued-iterated-classrel

Latex:
\mforall{}[Info,A,S:Type].
\mforall{}es:EO+(Info).  \mforall{}P:E  {}\mrightarrow{}  S  {}\mrightarrow{}  \mBbbP{}.  \mforall{}init:Id  {}\mrightarrow{}  bag(S).  \mforall{}f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  S  {}\mrightarrow{}  S.  \mforall{}X:EClass(A).  \mforall{}e:E.  \mforall{}v:S.
(single-valued-bag(init  loc(e);S)
{}\mRightarrow{}  single-valued-classrel(es;X;A)
{}\mRightarrow{}  (\mforall{}s:S.  \mforall{}e':E.
(e'  \mleq{}loc  e
{}\mRightarrow{}  if  first(e')
then  s  \mdownarrow{}\mmember{}  init  loc(e')
else  s  \mmember{}  State-loc-comb(init;f;X)(pred(e'))  \mwedge{}  P[pred(e');s]
fi
{}\mRightarrow{}  if  e'  \mmember{}\msubb{}  X  then  \mforall{}a:A.  (a  \mmember{}  X(e')  {}\mRightarrow{}  P[e';f  loc(e')  a  s])  else  P[e';s]  fi  ))
{}\mRightarrow{}  v  \mmember{}  State-loc-comb(init;f;X)(e)
{}\mRightarrow{}  P[e;v])

Date html generated: 2015_07_22-PM-00_24_38
Last ObjectModification: 2015_01_28-AM-10_10_37

Home Index