---

Step * 2 1 of Lemma local-simulation-agreement


1. correct : Id ─→ ℙ@i'
2. g : Name ─→ Type@i'
3. f : Name ─→ Type@i'
4. X : EClass(Interface)@i'
5. LocalClass(X)@i'
6. locs : bag(Id)@i
7. hdr : Name@i
8. hdr encodes Id × Message(g)
9. hdrs : Name List@i
10. R : Interface ─→ Interface ─→ ℙ@i'
11. es : EO+(Message(f))@i'
12. ∀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)))))))
13. ∀[e:E]. (local-simulation-inputs(es;e;hdr;locs) ∈ ({i:Id| i ↓∈ locs}  × Message(g)) List)
14. ∀i,j:Id.  ((correct i) ⇒ (correct j) ⇒ local-simulation-input-consistency(g;X;hdr;locs;es;i;j))@i
15. ∀i:Id. ((correct i) ⇒ local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i))@i
16. ∀eo:EO+(Message(g)). (eo-msg-interface-constraint(eo;X;hdrs;g) ⇒ any v1,v2 from X satisfy R[v1;v2])@i'
17. e1 : E@i
18. e2 : E@i
19. correct loc(e1)@i
20. correct loc(e2)@i
21. v1 : Interface@i
22. v2 : Interface@i
23. v1 ∈ local-simulation-class(X;locs;hdr)(e1)@i
24. v2 ∈ local-simulation-class(X;locs;hdr)(e2)@i
25. eo : EO+(Message(g))
26. eo-msg-interface-constraint(eo;X;hdrs;g)
27. ↑has-header-and-in-locs(info(e2);hdr;locs)
28. e3 : E
29. v2 ∈ X(e3)
30. ↑has-header-and-in-locs(info(e1);hdr;locs)
31. e' : E
32. v1 ∈ X(e')
⊢ R[v1;v2]
BY
{ OnMaybeHyp 16 (\h. (Unfold `consistent-class` h THEN InstHyp [⌈eo⌉;⌈e'⌉;⌈e3⌉;⌈v1⌉;⌈v2⌉] h⋅ THEN Complete (Auto))) }

---

Latex:

---

Latex:

1.  correct  :  Id  {}\mrightarrow{}  \mBbbP{}@i'
2.  g  :  Name  {}\mrightarrow{}  Type@i'
3.  f  :  Name  {}\mrightarrow{}  Type@i'
4.  X  :  EClass(Interface)@i'
5.  LocalClass(X)@i'
6.  locs  :  bag(Id)@i
7.  hdr  :  Name@i
8.  hdr  encodes  Id  \mtimes{}  Message(g)
9.  hdrs  :  Name  List@i
10.  R  :  Interface  {}\mrightarrow{}  Interface  {}\mrightarrow{}  \mBbbP{}@i'
11.  es  :  EO+(Message(f))@i'
12.  \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)))))))
13.  \mforall{}[e:E].  (local-simulation-inputs(es;e;hdr;locs)  \mmember{}  (\{i:Id|  i  \mdownarrow{}\mmember{}  locs\}    \mtimes{}  Message(g))  List)
14.  \mforall{}i,j:Id.
            ((correct  i)  {}\mRightarrow{}  (correct  j)  {}\mRightarrow{}  local-simulation-input-consistency(g;X;hdr;locs;es;i;j))@i
15.  \mforall{}i:Id.  ((correct  i)  {}\mRightarrow{}  local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i))@i
16.  \mforall{}eo:EO+(Message(g))
            (eo-msg-interface-constraint(eo;X;hdrs;g)  {}\mRightarrow{}  any  v1,v2  from  X  satisfy  R[v1;v2])@i'
17.  e1  :  E@i
18.  e2  :  E@i
19.  correct  loc(e1)@i
20.  correct  loc(e2)@i
21.  v1  :  Interface@i
22.  v2  :  Interface@i
23.  v1  \mmember{}  local-simulation-class(X;locs;hdr)(e1)@i
24.  v2  \mmember{}  local-simulation-class(X;locs;hdr)(e2)@i
25.  eo  :  EO+(Message(g))
26.  eo-msg-interface-constraint(eo;X;hdrs;g)
27.  \muparrow{}has-header-and-in-locs(info(e2);hdr;locs)
28.  e3  :  E
29.  v2  \mmember{}  X(e3)
30.  \muparrow{}has-header-and-in-locs(info(e1);hdr;locs)
31.  e'  :  E
32.  v1  \mmember{}  X(e')
\mvdash{}  R[v1;v2]


By

---

Latex:
OnMaybeHyp  16  (\mbackslash{}h.  (Unfold  `consistent-class`  h
                                        THEN  InstHyp  [\mkleeneopen{}eo\mkleeneclose{};\mkleeneopen{}e'\mkleeneclose{};\mkleeneopen{}e3\mkleeneclose{};\mkleeneopen{}v1\mkleeneclose{};\mkleeneopen{}v2\mkleeneclose{}]  h\mcdot{}
                                        THEN  Complete  (Auto)))

---

Home Index