---

Step * of Lemma global-order-compat-invariant

∀[Info:Type]. ∀[P:Id ─→ Info List+ ─→ ℙ]. ∀[R:Id ─→ Id ─→ Info List+ ─→ Info List+ ─→ ℙ].
  ∀L1,L2:(Id × Info) List.
    (L1 || L2
    ⇒ (causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2]) global-eo(L1))
    ⇒ (causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2]) global-eo(L2))
    ⇒ (∃L:(Id × Info) List
         ((causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2]) global-eo(L))
         ∧ (∀L':(Id × Info) List. (L1 || L' ⇒ L2 || L' ⇒ L || L'))
         ∧ (∃f:E ─→ E. es-local-embedding(Info;global-eo(L1);global-eo(L);f))
         ∧ (∃g:E ─→ E. es-local-embedding(Info;global-eo(L2);global-eo(L);g)))))
BY
{ (RepeatFor 6 (Intro)
   THEN (InstLemma `causal-invariant_wf` [⌈Info⌉;⌈R⌉;⌈P⌉]⋅ THENA Auto)
   THEN RepeatFor 2 (Intro)
   THEN (InstLemma `global-order-compat-joint-embedding` [⌈Info⌉;⌈L1⌉;⌈L2⌉]⋅ THENA Auto)
   THEN ParallelLast
   THEN Auto
   THEN ExRepD
   THEN FLemma `weak-joint-embedding-preserves-causal-invariant` [13;8;9]
   THEN Auto) }

---

Latex:

---

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{}L1,L2:(Id  \mtimes{}  Info)  List.
        (L1  ||  L2
        {}\mRightarrow{}  (causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2])  global-eo(L1))
        {}\mRightarrow{}  (causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2])  global-eo(L2))
        {}\mRightarrow{}  (\mexists{}L:(Id  \mtimes{}  Info)  List
                  ((causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2])  global-eo(L))
                  \mwedge{}  (\mforall{}L':(Id  \mtimes{}  Info)  List.  (L1  ||  L'  {}\mRightarrow{}  L2  ||  L'  {}\mRightarrow{}  L  ||  L'))
                  \mwedge{}  (\mexists{}f:E  {}\mrightarrow{}  E.  es-local-embedding(Info;global-eo(L1);global-eo(L);f))
                  \mwedge{}  (\mexists{}g:E  {}\mrightarrow{}  E.  es-local-embedding(Info;global-eo(L2);global-eo(L);g)))))


By

---

Latex:
(RepeatFor  6  (Intro)
  THEN  (InstLemma  `causal-invariant\_wf`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (Intro)
  THEN  (InstLemma  `global-order-compat-joint-embedding`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}L1\mkleeneclose{};\mkleeneopen{}L2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ParallelLast
  THEN  Auto
  THEN  ExRepD
  THEN  FLemma  `weak-joint-embedding-preserves-causal-invariant`  [13;8;9]
  THEN  Auto)

---

Home Index