Nuprl Lemma : weak-joint-embedding-preserves-squash-causal-invariant

[Info:Type]. ∀[R:Id ─→ Id ─→ Info List+ ─→ Info List+ ─→ ℙ]. ∀[P:Id ─→ Info List+ ─→ ℙ].
  ∀eo1,eo2,eo:EO+(Info). ∀f:E ─→ E. ∀g:E ─→ E.
    (es-weak-joint-embedding(Info;eo1;eo2;eo;f;g)
     (squash-causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2]) eo1)
     (squash-causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2]) eo2)
     (squash-causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2]) eo))


Proof




Definitions occuring in Statement :  squash-causal-invariant: squash-causal-invariant(i,L.P[i; L];a,b,L1,L2.R[a; b; L1; L2]) es-weak-joint-embedding: es-weak-joint-embedding(Info;eo1;eo2;eo;f;g) event-ordering+: EO+(Info) es-E: E Id: Id listp: List+ uall: [x:A]. B[x] prop: so_apply: x[s1;s2;s3;s4] so_apply: x[s1;s2] all: x:A. B[x] implies:  Q apply: a function: x:A ─→ B[x] universe: Type
Lemmas :  squash-causal-invariant_wf es-local-property_wf listp_wf Id_wf es-E_wf event-ordering+_subtype es-weak-joint-embedding_wf event-ordering+_wf embedding-preserves-local-property es-causl_wf es-local-relation_wf and_wf equal_wf embedding-preserves-local-relation squash_wf true_wf event_ordering_wf iff_weakening_equal
\mforall{}[Info:Type].  \mforall{}[R:Id  {}\mrightarrow{}  Id  {}\mrightarrow{}  Info  List\msupplus{}  {}\mrightarrow{}  Info  List\msupplus{}  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[P:Id  {}\mrightarrow{}  Info  List\msupplus{}  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}eo1,eo2,eo:EO+(Info).  \mforall{}f:E  {}\mrightarrow{}  E.  \mforall{}g:E  {}\mrightarrow{}  E.
        (es-weak-joint-embedding(Info;eo1;eo2;eo;f;g)
        {}\mRightarrow{}  (squash-causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2])  eo1)
        {}\mRightarrow{}  (squash-causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2])  eo2)
        {}\mRightarrow{}  (squash-causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2])  eo))



Date html generated: 2015_07_17-PM-00_13_30
Last ObjectModification: 2015_02_04-PM-05_37_09

Home Index