Nuprl Lemma : State-comb-invariant

∀[Info,A,S:Type]. ∀[init:Id ⟶ bag(S)]. ∀[f: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-class(f;init;X)(e') ⇒ P[s] ⇒ P[f a s]))))
    ⇒ v ∈ State-comb(init;f;X)(e)
    ⇒ P[v])

Proof

Definitions occuring in Statement : State-comb: State-comb(init;f;X), Memory-class: Memory-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)
Definitions unfolded in proof : uall: ∀[x:A]. B[x], all: ∀x:A. B[x], implies: P ⇒ Q, member: t ∈ T, sq_stable: SqStable(P), iff: P ⇐⇒ Q, and: P ∧ Q, rev_implies: P ⇐ Q, prior_iterated_classrel: s ∈ prior(X*(f,init,e)), prop: ℙ, so_apply: x[s], subtype_rel: A ⊆r B, squash: ↓T, so_lambda: λ₂x.t[x], so_lambda: λ₂x y.t[x; y], so_apply: x[s1;s2]

Latex:
\mforall{}[Info,A,S:Type]. \mforall{}[init:Id {}\mrightarrow{} bag(S)]. \mforall{}[f: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-class(f;init;X)(e') {}\mRightarrow{} P[s] {}\mRightarrow{} P[f a s])))) {}\mRightarrow{} v \mmember{} State-comb(init;f;X)(e) {}\mRightarrow{} P[v]) Date html generated: 2016_05_17-AM-09_59_38 Last ObjectModification: 2016_01_17-PM-11_05_53 Theory : classrel!lemmas Home Index