---

Step * 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. (∀L∈map(λe.local-simulation-inputs(es;e;hdr;locs);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)
⊢ (∀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))
BY
{ (ParallelOp -2
   THEN (RWO "length-map" (-2) THENA Auto)
   THEN ParallelOp -2
   THEN (RWO "select-map" (-1) THENA Auto)
   THEN Reduce (-1)
   THEN Fold `local-simulation-eo` (-1)
   THEN D -1
   THEN RenameVar `h' (-2)) }

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))
⊢ ∀[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])

---

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{}L\mmember{}map(\mlambda{}e.local-simulation-inputs(es;e;hdr;locs);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)
\mvdash{}  (\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))


By

---

Latex:
(ParallelOp  -2
  THEN  (RWO  "length-map"  (-2)  THENA  Auto)
  THEN  ParallelOp  -2
  THEN  (RWO  "select-map"  (-1)  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  Fold  `local-simulation-eo`  (-1)
  THEN  D  -1
  THEN  RenameVar  `h'  (-2))

---

Home Index