---

Step * 2 of Lemma global-order-pairwise-compat-msg-interface-constraint


1. f : Name ─→ Type@i'
2. hdrs : Name List@i
3. X : EClass(Interface)@i'
4. LocalClass(X)@i'
5. ∃P:Id ─→ Message(f) List+ ─→ ℙ
    ∃R:Id ─→ Id ─→ Message(f) List+ ─→ Message(f) List+ ─→ ℙ
     ∀eo:EO+(Message(f))
       (squash-causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2]) eo ⇐⇒ eo-msg-interface-constraint(eo;X;hdrs;f))
⊢ ∀LL:(Id × Message(f)) List List
    ((∀L1,L2∈LL.  L1 || L2)
    ⇒ (∀L∈LL.eo-msg-interface-constraint(global-eo(L);X;hdrs;f))
    ⇒ (∃G:(Id × Message(f)) List
         (eo-msg-interface-constraint(global-eo(G);X;hdrs;f)
         ∧ (∀L∈LL.∃g:E ─→ E. es-local-embedding(Message(f);global-eo(L);global-eo(G);g)))))
BY
{ (RepeatFor 2 (D -1)
   THEN (InstLemma `global-order-pairwise-compat-squash-invariant` [⌈Message(f)⌉;⌈P⌉;⌈R⌉]⋅ THENA Auto)
   THEN RepeatFor 5 (ParallelLast)
   THEN BackThruSomeHyp
   THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  Name  {}\mrightarrow{}  Type@i'
2.  hdrs  :  Name  List@i
3.  X  :  EClass(Interface)@i'
4.  LocalClass(X)@i'
5.  \mexists{}P:Id  {}\mrightarrow{}  Message(f)  List\msupplus{}  {}\mrightarrow{}  \mBbbP{}
        \mexists{}R:Id  {}\mrightarrow{}  Id  {}\mrightarrow{}  Message(f)  List\msupplus{}  {}\mrightarrow{}  Message(f)  List\msupplus{}  {}\mrightarrow{}  \mBbbP{}
          \mforall{}eo:EO+(Message(f))
              (squash-causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2])  eo
              \mLeftarrow{}{}\mRightarrow{}  eo-msg-interface-constraint(eo;X;hdrs;f))
\mvdash{}  \mforall{}LL:(Id  \mtimes{}  Message(f))  List  List
        ((\mforall{}L1,L2\mmember{}LL.    L1  ||  L2)
        {}\mRightarrow{}  (\mforall{}L\mmember{}LL.eo-msg-interface-constraint(global-eo(L);X;hdrs;f))
        {}\mRightarrow{}  (\mexists{}G:(Id  \mtimes{}  Message(f))  List
                  (eo-msg-interface-constraint(global-eo(G);X;hdrs;f)
                  \mwedge{}  (\mforall{}L\mmember{}LL.\mexists{}g:E  {}\mrightarrow{}  E.  es-local-embedding(Message(f);global-eo(L);global-eo(G);g)))))


By

---

Latex:
(RepeatFor  2  (D  -1)
  THEN  (InstLemma  `global-order-pairwise-compat-squash-invariant`  [\mkleeneopen{}Message(f)\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  5  (ParallelLast)
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index