---

Step * of Lemma consistent-local-simulation

∀g,f:Name ⟶ Type. ∀X:EClass(Interface).
  (LocalClass(X)
  ⇒ (∀locs:bag(Id). ∀hdr:Name.
        ∀es:EO+(Message(f)). ∀ee:E List.
          ((∀e1,e2∈ee.  local-simulation-inputs(es;e1;hdr;locs) || local-simulation-inputs(es;e2;hdr;locs))
          ⇒ (∀hdrs:Name List
                ((∀e∈ee.eo-msg-interface-constraint(local-simulation-eo(es;e;hdr;locs);X;hdrs;g))
                ⇒ (∃eo:EO+(Message(g))
                     (eo-msg-interface-constraint(eo;X;hdrs;g)
                     ∧ (∀e∈ee.∀[v:Interface]
                                (↑has-header-and-in-locs(info(e);hdr;locs)) ∧ (∃e':E. v ∈ X(e')) 
                                supposing v ∈ local-simulation-class(X;locs;hdr)(e))))))) 
        supposing hdr encodes Id × Message(g)))
BY
{ (RepeatFor 8 (Intro⋅)
   THEN (InstLemma `local-simulation-inputs_wf` [⌜f⌝;⌜Message(g)⌝;⌜es⌝;⌜hdr⌝;⌜locs⌝]⋅ THENA Auto)
   THEN InstLemma `local-simulation-classrel` [⌜f⌝;⌜Message(g)⌝;⌜Interface⌝;⌜X⌝;⌜locs⌝;⌜hdr⌝;⌜es⌝]⋅
   THEN Auto
   THEN (InstLemma `global-order-pairwise-compat-msg-and-classrel` [⌜g⌝;⌜hdrs⌝;⌜X⌝;
         ⌜map(λe.local-simulation-inputs(es;e;hdr;locs);ee)⌝]⋅
         THENA (Auto
                THEN Try ((BLemma `pairwise-map` THEN Auto))
                THEN BLemma `l_all_map`
                THEN Auto
                THEN Reduce 0
                THEN Fold `local-simulation-eo` 0
                THEN Auto)
         )
   THEN ExRepD
   THEN With ⌜global-eo(G)⌝ (D 0)⋅
   THEN Auto) }

1
1. g : Name ⟶ Type@i'
2. f : Name ⟶ Type@i'
3. X : EClass(Interface)@i'
4. LocalClass(X)@i'
5. locs : bag(Id)@i
6. hdr : Name@i
7. [%1] : hdr encodes Id × Message(g)
8. es : EO+(Message(f))@i'
9. ∀[e:E]. (local-simulation-inputs(es;e;hdr;locs) ∈ ({i:Id| i ↓∈ locs}  × Message(g)) List)
10. ∀e:E
      ∀[v:Interface]
        uiff(v ∈ local-simulation-class(X;locs;hdr)(e);(↑has-header-and-in-locs(info(e);hdr;locs))
        ∧ v ∈ X(local-simulation-event(es;e;hdr;locs))) 
      supposing LocalClass(X)
11. ee : E List@i
12. (∀e1,e2∈ee.  local-simulation-inputs(es;e1;hdr;locs) || local-simulation-inputs(es;e2;hdr;locs))@i'
13. hdrs : Name List@i
14. (∀e∈ee.eo-msg-interface-constraint(local-simulation-eo(es;e;hdr;locs);X;hdrs;g))@i
15. G : (Id × Message(g)) List
16. eo-msg-interface-constraint(global-eo(G);X;hdrs;g)
17. (∀L∈map(λe.local-simulation-inputs(es;e;hdr;locs);ee).∃g@0:E ⟶ E
                                                           ∀[e:E]. ∀[v:Interface].  (v ∈ X(e) ⇐⇒ v ∈ X(g@0 e)))
18. eo-msg-interface-constraint(global-eo(G);X;hdrs;g)
⊢ (∀e∈ee.∀[v:Interface]
           (↑has-header-and-in-locs(info(e);hdr;locs)) ∧ (∃e':E. v ∈ X(e')) 
           supposing v ∈ local-simulation-class(X;locs;hdr)(e))

---

Latex:

---

Latex:
\mforall{}g,f:Name  {}\mrightarrow{}  Type.  \mforall{}X:EClass(Interface).
    (LocalClass(X)
    {}\mRightarrow{}  (\mforall{}locs:bag(Id).  \mforall{}hdr:Name.
                \mforall{}es:EO+(Message(f)).  \mforall{}ee:E  List.
                    ((\mforall{}e1,e2\mmember{}ee.
                        local-simulation-inputs(es;e1;hdr;locs)  ||  local-simulation-inputs(es;e2;hdr;locs))
                    {}\mRightarrow{}  (\mforall{}hdrs:Name  List
                                ((\mforall{}e\mmember{}ee.eo-msg-interface-constraint(local-simulation-eo(es;e;hdr;locs);X;hdrs;g))
                                {}\mRightarrow{}  (\mexists{}eo:EO+(Message(g))
                                          (eo-msg-interface-constraint(eo;X;hdrs;g)
                                          \mwedge{}  (\mforall{}e\mmember{}ee.\mforall{}[v:Interface]
                                                                (\muparrow{}has-header-and-in-locs(info(e);hdr;locs))  \mwedge{}  (\mexists{}e':E.  v  \mmember{}  X(e')) 
                                                                supposing  v  \mmember{}  local-simulation-class(X;locs;hdr)(e))))))) 
                supposing  hdr  encodes  Id  \mtimes{}  Message(g)))


By

---

Latex:
(RepeatFor  8  (Intro\mcdot{})
  THEN  (InstLemma  `local-simulation-inputs\_wf`  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}Message(g)\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}hdr\mkleeneclose{};\mkleeneopen{}locs\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  InstLemma  `local-simulation-classrel`  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}Message(g)\mkleeneclose{};\mkleeneopen{}Interface\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}locs\mkleeneclose{};\mkleeneopen{}hdr\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  (InstLemma  `global-order-pairwise-compat-msg-and-classrel`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}hdrs\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};
              \mkleeneopen{}map(\mlambda{}e.local-simulation-inputs(es;e;hdr;locs);ee)\mkleeneclose{}]\mcdot{}
              THENA  (Auto
                            THEN  Try  ((BLemma  `pairwise-map`  THEN  Auto))
                            THEN  BLemma  `l\_all\_map`
                            THEN  Auto
                            THEN  Reduce  0
                            THEN  Fold  `local-simulation-eo`  0
                            THEN  Auto)
              )
  THEN  ExRepD
  THEN  With  \mkleeneopen{}global-eo(G)\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto)

---

Home Index