Nuprl Lemma : global-order-pairwise-compat-squash-invariant

[Info:Type]. ∀[P:Id ─→ Info List+ ─→ ℙ]. ∀[R:Id ─→ Id ─→ Info List+ ─→ Info List+ ─→ ℙ].
  ∀LL:(Id × Info) List List
    ((∀L1,L2∈LL.  L1 || L2)
     (∀L∈LL.squash-causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2]) global-eo(L))
     (∃G:(Id × Info) List
         ((squash-causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2]) global-eo(G))
         ∧ (∀L∈LL.∃f:E ─→ E. es-local-embedding(Info;global-eo(L);global-eo(G);f)))))


Proof




Definitions occuring in Statement :  global-order-compat: L1 || L2 global-eo: global-eo(L) squash-causal-invariant: squash-causal-invariant(i,L.P[i; L];a,b,L1,L2.R[a; b; L1; L2]) es-local-embedding: es-local-embedding(Info;eo1;eo2;f) es-E: E Id: Id pairwise: (∀x,y∈L.  P[x; y]) listp: List+ l_all: (∀x∈L.P[x]) list: List uall: [x:A]. B[x] prop: so_apply: x[s1;s2;s3;s4] so_apply: x[s1;s2] all: x:A. B[x] exists: x:A. B[x] implies:  Q and: P ∧ Q apply: a function: x:A ─→ B[x] product: x:A × B[x] universe: Type
Lemmas :  list_induction list_wf pairwise_wf global-order-compat_wf l_all_wf2 l_member_wf global-eo_wf exists_wf all_wf es-E_wf event-ordering+_subtype es-local-embedding_wf nil_wf cons_wf Id_wf global-eo-E-sq length_of_nil_lemma es-local-property_wf subtype_rel-equal listp_wf int_seg_wf l_all_nil filter_nil_lemma nil_iseg filter_wf5 eq_id_wf iseg_wf pairwise-cons l_all-cons global-order-compat-squash-invariant compat_symmetry length_wf compose_wf select_wf sq_stable__le es-local-embedding-compose

Latex:
\mforall{}[Info:Type].  \mforall{}[P:Id  {}\mrightarrow{}  Info  List\msupplus{}  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[R:Id  {}\mrightarrow{}  Id  {}\mrightarrow{}  Info  List\msupplus{}  {}\mrightarrow{}  Info  List\msupplus{}  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}LL:(Id  \mtimes{}  Info)  List  List
        ((\mforall{}L1,L2\mmember{}LL.    L1  ||  L2)
        {}\mRightarrow{}  (\mforall{}L\mmember{}LL.squash-causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2])  global-eo(L))
        {}\mRightarrow{}  (\mexists{}G:(Id  \mtimes{}  Info)  List
                  ((squash-causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2])  global-eo(G))
                  \mwedge{}  (\mforall{}L\mmember{}LL.\mexists{}f:E  {}\mrightarrow{}  E.  es-local-embedding(Info;global-eo(L);global-eo(G);f)))))



Date html generated: 2015_07_21-PM-04_41_25
Last ObjectModification: 2015_01_27-PM-05_04_47

Home Index