---

Step * of Lemma global-order-pairwise-compat-msg-and-classrel

∀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. ∀[e:E]. ∀[v:Interface].  (v ∈ X(e) ⇐⇒ v ∈ X(g e))))))))
BY
{ (InstLemma `global-order-pairwise-compat-msg-interface-constraint` []
   THEN RepeatFor 12 ((ParallelLast' THENA Auto))
   THEN InstLemma `embedding-preserves-local-class`
    [⌈Message(f)⌉;⌈Interface⌉;⌈X⌉;⌈global-eo(LL[i])⌉;⌈global-eo(G)⌉;⌈g⌉]⋅
   THEN Auto) }

---

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.  \mforall{}[e:E].  \mforall{}[v:Interface].    (v  \mmember{}  X(e)  \mLeftarrow{}{}\mRightarrow{}  v  \mmember{}  X(g  e))))))))


By

---

Latex:
(InstLemma  `global-order-pairwise-compat-msg-interface-constraint`  []
  THEN  RepeatFor  12  ((ParallelLast'  THENA  Auto))
  THEN  InstLemma  `embedding-preserves-local-class`
    [\mkleeneopen{}Message(f)\mkleeneclose{};\mkleeneopen{}Interface\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}global-eo(LL[i])\mkleeneclose{};\mkleeneopen{}global-eo(G)\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index