---

Step * 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)))
⊢ ∀[v:Interface]
    (↑has-header-and-in-locs(info(ee[i]);hdr;locs)) ∧ (∃e':E. v ∈ X(e')) 
    supposing v ∈ local-simulation-class(X;locs;hdr)(ee[i])
BY
{ ((InstLemma `local-simulation-event_wf` [⌈f⌉;⌈Message(g)⌉;⌈es⌉;⌈hdr⌉;⌈locs⌉]⋅ THENA Auto) THEN RWO "-2" 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. ∀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')

---

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)))
\mvdash{}  \mforall{}[v:Interface]
        (\muparrow{}has-header-and-in-locs(info(ee[i]);hdr;locs))  \mwedge{}  (\mexists{}e':E.  v  \mmember{}  X(e')) 
        supposing  v  \mmember{}  local-simulation-class(X;locs;hdr)(ee[i])


By

---

Latex:
((InstLemma  `local-simulation-event\_wf`  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}Message(g)\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}hdr\mkleeneclose{};\mkleeneopen{}locs\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RWO  "-2"  0
  THEN  Auto)

---

Home Index