---

Step * 1 of Lemma local-simulation-agreement

.....antecedent..... 
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)))))
⊢ (∀e∈[e1; e2].eo-msg-interface-constraint(local-simulation-eo(es;e;hdr;locs);X;hdrs;g))
BY
{ (BLemma `l_all_cons` 
   THEN Auto
   THEN Try ((Using [`i', ⌈loc(e1)⌉] (BLemma `local-simulation-msg-constraint`)⋅ THEN Complete (Auto)))
   THEN Try ((Using [`i', ⌈loc(e2)⌉] (BLemma `local-simulation-msg-constraint`)⋅ THEN Complete (Auto)))) }

---

Latex:

---

Latex:
.....antecedent..... 
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)))))
\mvdash{}  (\mforall{}e\mmember{}[e1;  e2].eo-msg-interface-constraint(local-simulation-eo(es;e;hdr;locs);X;hdrs;g))


By

---

Latex:
(BLemma  `l\_all\_cons` 
  THEN  Auto
  THEN  Try  ((Using  [`i',  \mkleeneopen{}loc(e1)\mkleeneclose{}]  (BLemma  `local-simulation-msg-constraint`)\mcdot{}
                        THEN  Complete  (Auto)
                        ))
  THEN  Try  ((Using  [`i',  \mkleeneopen{}loc(e2)\mkleeneclose{}]  (BLemma  `local-simulation-msg-constraint`)\mcdot{}
                        THEN  Complete  (Auto)
                        )))

---

Home Index