---

Step * 2 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. ∀hdrs:Name List
      ((∀e∈[e1; e2].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∈[e1; e2].∀[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)))))
26. ∃eo:EO+(Message(g))
     (eo-msg-interface-constraint(eo;X;hdrs;g)
     ∧ (∀e∈[e1; e2].∀[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)))
⊢ R[v1;v2]
BY
{ (Thin (-2)
   THEN ExRepD
   THEN RWW "l_all_cons" (-1)
   THEN Auto
   THEN Thin (-1)
   THEN ((InstHyp [⌈v2⌉] (-1)⋅ THENA Auto) THEN Thin (-2))
   THEN (InstHyp [⌈v1⌉] (-2)⋅ THENA Auto)
   THEN Thin (-3)
   THEN ExRepD) }

1
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]

---

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.  \mforall{}hdrs:Name  List
            ((\mforall{}e\mmember{}[e1;  e2].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{}[e1;  e2].\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)))))
26.  \mexists{}eo:EO+(Message(g))
          (eo-msg-interface-constraint(eo;X;hdrs;g)
          \mwedge{}  (\mforall{}e\mmember{}[e1;  e2].\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)))
\mvdash{}  R[v1;v2]


By

---

Latex:
(Thin  (-2)
  THEN  ExRepD
  THEN  RWW  "l\_all\_cons"  (-1)
  THEN  Auto
  THEN  Thin  (-1)
  THEN  ((InstHyp  [\mkleeneopen{}v2\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)  THEN  Thin  (-2))
  THEN  (InstHyp  [\mkleeneopen{}v1\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  Thin  (-3)
  THEN  ExRepD)

---

Home Index