Nuprl Lemma : Memory-class-mem

∀[Info,B,A:Type].

  ∀R:A ⟶ B ⟶ B ⟶ ℙ. ∀f:A ⟶ B ⟶ B. ∀init:Id ⟶ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e1,e2:E. ∀v1,v2:B. ∀a:A.

    ((∀a:A. ∀s:B. ∀e:E.  (e1 ≤loc e  ⇒ (e <loc e2) ⇒ a ∈ X(e) ⇒ s ∈ Memory-class(f;init;X)(e) ⇒ R[a;s;f a s]))
    ⇒ (∀a1,a2:A. ∀s1,s2:B. ∀e,e':E.
          (e1 ≤loc e
          ⇒ (e <loc e')
          ⇒ (e' <loc e2)
          ⇒ a1 ∈ X(e)
          ⇒ s1 ∈ Memory-class(f;init;X)(e)
          ⇒ a2 ∈ X(e')
          ⇒ s2 ∈ Memory-class(f;init;X)(e')
          ⇒ R[a1;s1;s2]
          ⇒ R[a1;s1;f a2 s2]))
    ⇒ single-valued-classrel(es;X;A)
    ⇒ single-valued-bag(init loc(e1);B)
    ⇒ (e1 <loc e2)
    ⇒ a ∈ X(e1)
    ⇒ v1 ∈ Memory-class(f;init;X)(e1)
    ⇒ v2 ∈ Memory-class(f;init;X)(e2)
    ⇒ R[a;v1;v2])

Proof

Definitions occuring in Statement : Memory-class: Memory-class(f;init;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-loc: loc(e), es-E: E, Id: Id, uall: ∀[x:A]. B[x], prop: ℙ, so_apply: x[s1;s2;s3], all: ∀x:A. B[x], implies: P ⇒ Q, apply: f a, function: x:A ⟶ B[x], universe: Type, single-valued-bag: single-valued-bag(b;T), bag: bag(T)
Definitions unfolded in proof : uall: ∀[x:A]. B[x], all: ∀x:A. B[x], implies: P ⇒ Q, member: t ∈ T, uimplies: b supposing a, es-locl: (e <loc e'), and: P ∧ Q, prop: ℙ, uiff: uiff(P;Q), prior-iterated-classrel: prior-iterated-classrel(es;A;S;s;X;f;init;e), or: P ∨ Q, subtype_rel: A ⊆r B, not: ¬A, false: False, so_lambda: λ₂x.t[x], so_apply: x[s1;s2;s3], so_apply: x[s], so_lambda: λ₂x y.t[x; y], so_apply: x[s1;s2], cand: A c∧ B, iff: P ⇐⇒ Q, rev_implies: P ⇐ Q, guard: {T}

Latex:
\mforall{}[Info,B,A:Type]. \mforall{}R:A {}\mrightarrow{} B {}\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{}a:A. \mforall{}s:B. \mforall{}e:E. (e1 \mleq{}loc e {}\mRightarrow{} (e <loc e2) {}\mRightarrow{} a \mmember{} X(e) {}\mRightarrow{} s \mmember{} Memory-class(f;init;X)(e) {}\mRightarrow{} R[a;s;f a s])) {}\mRightarrow{} (\mforall{}a1,a2:A. \mforall{}s1,s2:B. \mforall{}e,e':E. (e1 \mleq{}loc e {}\mRightarrow{} (e <loc e') {}\mRightarrow{} (e' <loc e2) {}\mRightarrow{} a1 \mmember{} X(e) {}\mRightarrow{} s1 \mmember{} Memory-class(f;init;X)(e) {}\mRightarrow{} a2 \mmember{} X(e') {}\mRightarrow{} s2 \mmember{} Memory-class(f;init;X)(e') {}\mRightarrow{} R[a1;s1;s2] {}\mRightarrow{} R[a1;s1;f a2 s2])) {}\mRightarrow{} single-valued-classrel(es;X;A) {}\mRightarrow{} single-valued-bag(init loc(e1);B) {}\mRightarrow{} (e1 <loc e2) {}\mRightarrow{} a \mmember{} X(e1) {}\mRightarrow{} v1 \mmember{} Memory-class(f;init;X)(e1) {}\mRightarrow{} v2 \mmember{} Memory-class(f;init;X)(e2) {}\mRightarrow{} R[a;v1;v2]) Date html generated: 2016_05_17-AM-09_25_19 Last ObjectModification: 2015_12_29-PM-04_06_09 Theory : classrel!lemmas Home Index