---

Step * 1 1 1 1 of Lemma consistent-local-simulation


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. ∀i:ℕ||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)
19. i : ℕ||ee||@i
20. h : E ─→ E
21. ∀[e:E]. ∀[v:Interface].  (v ∈ X(e) ⇐⇒ v ∈ X(h e))
22. ∀[v:Interface]
      uiff(v ∈ local-simulation-class(X;locs;hdr)(ee[i]);(↑has-header-and-in-locs(info(ee[i]);hdr;locs))
      ∧ v ∈ X(local-simulation-event(es;ee[i];hdr;locs)))
23. ∀[e:E]. local-simulation-event(es;e;hdr;locs) ∈ E supposing ↑has-header-and-in-locs(info(e);hdr;locs)
24. [v] : Interface
25. ↑has-header-and-in-locs(info(ee[i]);hdr;locs)
26. v ∈ X(local-simulation-event(es;ee[i];hdr;locs))
27. ↑has-header-and-in-locs(info(ee[i]);hdr;locs)
⊢ ∃e':E. v ∈ X(e')
BY
{ (With ⌈h local-simulation-event(es;ee[i];hdr;locs)⌉ (D 0)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  Name  {}\mrightarrow{}  Type@i'
2.  f  :  Name  {}\mrightarrow{}  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  \mtimes{}  Message(g)
8.  es  :  EO+(Message(f))@i'
9.  \mforall{}[e:E].  (local-simulation-inputs(es;e;hdr;locs)  \mmember{}  (\{i:Id|  i  \mdownarrow{}\mmember{}  locs\}    \mtimes{}  Message(g))  List)
10.  \mforall{}e:E
            \mforall{}[v:Interface]
                uiff(v  \mmember{}  local-simulation-class(X;locs;hdr)(e);(\muparrow{}has-header-and-in-locs(info(e);hdr;locs))
                \mwedge{}  v  \mmember{}  X(local-simulation-event(es;e;hdr;locs))) 
            supposing  LocalClass(X)
11.  ee  :  E  List@i
12.  (\mforall{}e1,e2\mmember{}ee.
          local-simulation-inputs(es;e1;hdr;locs)  ||  local-simulation-inputs(es;e2;hdr;locs))@i'
13.  hdrs  :  Name  List@i
14.  (\mforall{}e\mmember{}ee.eo-msg-interface-constraint(local-simulation-eo(es;e;hdr;locs);X;hdrs;g))@i
15.  G  :  (Id  \mtimes{}  Message(g))  List
16.  eo-msg-interface-constraint(global-eo(G);X;hdrs;g)
17.  \mforall{}i:\mBbbN{}||ee||.  \mexists{}g@0:E  {}\mrightarrow{}  E.  \mforall{}[e:E].  \mforall{}[v:Interface].    (v  \mmember{}  X(e)  \mLeftarrow{}{}\mRightarrow{}  v  \mmember{}  X(g@0  e))
18.  eo-msg-interface-constraint(global-eo(G);X;hdrs;g)
19.  i  :  \mBbbN{}||ee||@i
20.  h  :  E  {}\mrightarrow{}  E
21.  \mforall{}[e:E].  \mforall{}[v:Interface].    (v  \mmember{}  X(e)  \mLeftarrow{}{}\mRightarrow{}  v  \mmember{}  X(h  e))
22.  \mforall{}[v:Interface]
            uiff(v  \mmember{}  local-simulation-class(X;locs;hdr)(
                              ee[i]);(\muparrow{}has-header-and-in-locs(info(ee[i]);hdr;locs))
            \mwedge{}  v  \mmember{}  X(local-simulation-event(es;ee[i];hdr;locs)))
23.  \mforall{}[e:E]
            local-simulation-event(es;e;hdr;locs)  \mmember{}  E  supposing  \muparrow{}has-header-and-in-locs(info(e);hdr;locs)
24.  [v]  :  Interface
25.  \muparrow{}has-header-and-in-locs(info(ee[i]);hdr;locs)
26.  v  \mmember{}  X(local-simulation-event(es;ee[i];hdr;locs))
27.  \muparrow{}has-header-and-in-locs(info(ee[i]);hdr;locs)
\mvdash{}  \mexists{}e':E.  v  \mmember{}  X(e')


By

---

Latex:
(With  \mkleeneopen{}h  local-simulation-event(es;ee[i];hdr;locs)\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index