---

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

∀f:Name ─→ Type. ∀hdrs:Name List. ∀X:EClass(Interface).
  (LocalClass(X)
  ⇒ (∀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 4 (Intro)
   THEN Assert ⌈∃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))⌉⋅
   ) }

1
.....assertion..... 
1. f : Name ─→ Type@i'
2. hdrs : Name List@i
3. X : EClass(Interface)@i'
4. LocalClass(X)@i'
⊢ ∃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))

2
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)))))

---

Latex:

---

Latex:
\mforall{}f:Name  {}\mrightarrow{}  Type.  \mforall{}hdrs:Name  List.  \mforall{}X:EClass(Interface).
    (LocalClass(X)
    {}\mRightarrow{}  (\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  4  (Intro)
  THEN  Assert  \mkleeneopen{}\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))\mkleeneclose{}\mcdot{}
  )

---

Home Index