Nuprl Lemma : Memory-loc-class-trans2

∀[Info,B,A:Type].

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

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

Proof

Definitions occuring in Statement : Memory-loc-class: Memory-loc-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, trans: Trans(T;x,y.E[x; y]), sq_stable: SqStable(P), uall: ∀[x:A]. B[x], prop: ℙ, so_apply: x[s1;s2], all: ∀x:A. B[x], not: ¬A, implies: 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)
Definitions unfolded in proof : uall: ∀[x:A]. B[x], member: t ∈ T, all: ∀x:A. B[x], implies: P ⇒ Q, uiff: uiff(P;Q), and: P ∧ Q, uimplies: b supposing a, subtype_rel: A ⊆r B, prop: ℙ, es-locl: (e <loc e'), so_lambda: λ₂x y.t[x; y], so_apply: x[s1;s2], so_lambda: λ₂x.t[x], so_apply: x[s]

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