Nuprl Lemma : State-loc-comb-invariant

`∀[Info,A,S:Type]. ∀[init:Id ─→ bag(S)]. ∀[f:Id ─→ A ─→ S ─→ S]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[P:S ─→ ℙ]. ∀[e:E].`
`  ∀v:S`
`    ((∀s:S. SqStable(P[s]))`
`    `` (∀s:S. (s ↓∈ init loc(e) `` P[s]))`
`    `` (∀a:A. ∀e':E.`
`          (e' ≤loc e  `` a ∈ X(e') `` (∀s:S. (s ∈ Memory-loc-class(f;init;X)(e') `` P[s] `` P[f loc(e') a s]))))`
`    `` v ∈ State-loc-comb(init;f;X)(e)`
`    `` P[v])`

Proof

Definitions occuring in Statement :  State-loc-comb: `State-loc-comb(init;f;X)` Memory-loc-class: `Memory-loc-class(f;init;X)` classrel: `v ∈ X(e)` eclass: `EClass(A[eo; e])` event-ordering+: `EO+(Info)` es-le: `e ≤loc e' ` es-loc: `loc(e)` es-E: `E` Id: `Id` sq_stable: `SqStable(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` apply: `f a` function: `x:A ─→ B[x]` universe: `Type` bag-member: `x ↓∈ bs` bag: `bag(T)`
Lemmas :  State-loc-comb-classrel-non-loc State-comb-invariant es-loc_wf es-le-loc Memory-classrel-loc and_wf equal_wf Id_wf Memory-class_wf eclass_wf es-E_wf event-ordering+_subtype event-ordering+_wf classrel_wf es-le_wf State-loc-comb_wf all_wf Memory-loc-class_wf bag-member_wf sq_stable_wf bag_wf

Latex:
\mforall{}[Info,A,S:Type].  \mforall{}[init:Id  {}\mrightarrow{}  bag(S)].  \mforall{}[f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  S  {}\mrightarrow{}  S].  \mforall{}[X:EClass(A)].  \mforall{}[es:EO+(Info)].
\mforall{}[P:S  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[e:E].
\mforall{}v:S
((\mforall{}s:S.  SqStable(P[s]))
{}\mRightarrow{}  (\mforall{}s:S.  (s  \mdownarrow{}\mmember{}  init  loc(e)  {}\mRightarrow{}  P[s]))
{}\mRightarrow{}  (\mforall{}a:A.  \mforall{}e':E.
(e'  \mleq{}loc  e
{}\mRightarrow{}  a  \mmember{}  X(e')
{}\mRightarrow{}  (\mforall{}s:S.  (s  \mmember{}  Memory-loc-class(f;init;X)(e')  {}\mRightarrow{}  P[s]  {}\mRightarrow{}  P[f  loc(e')  a  s]))))
{}\mRightarrow{}  v  \mmember{}  State-loc-comb(init;f;X)(e)
{}\mRightarrow{}  P[v])

Date html generated: 2015_07_22-PM-00_24_25
Last ObjectModification: 2015_01_28-AM-10_09_43

Home Index