---

Step * of 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)))))
BY
{ (RepeatFor 3 (Intro)
   THEN (InstLemma `squash-causal-invariant_wf` [⌈Info⌉;⌈R⌉;⌈P⌉]⋅ THENA Auto)
   THEN (Assert ⌈∀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
                        ((∀L':(Id × Info) List. ((∀L∈LL.L || L') ⇒ G || L'))
                        ∧ (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)))))⌉⋅
   THENM (ParallelLast THEN Auto)
   )) }

1
.....assertion..... 
1. [Info] : Type
2. [P] : Id ─→ Info List+ ─→ ℙ
3. [R] : Id ─→ Id ─→ Info List+ ─→ Info List+ ─→ ℙ
4. squash-causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2]) ∈ EO+(Info) ─→ ℙ
⊢ ∀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
         ((∀L':(Id × Info) List. ((∀L∈LL.L || L') ⇒ G || L'))
         ∧ (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)))))

---

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{}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)))))


By

---

Latex:
(RepeatFor  3  (Intro)
  THEN  (InstLemma  `squash-causal-invariant\_wf`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}\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
                                            ((\mforall{}L':(Id  \mtimes{}  Info)  List.  ((\mforall{}L\mmember{}LL.L  ||  L')  {}\mRightarrow{}  G  ||  L'))
                                            \mwedge{}  (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)))))\mkleeneclose{}\mcdot{}
  THENM  (ParallelLast  THEN  Auto)
  ))

---

Home Index