---

Step * 1 3 1 1 1 2 2 1 1 of Lemma local-simulation-msg-constraint


1. f : Name ─→ Type
2. g : Name ─→ Type
3. X : EClass(Interface)
4. LocalClass(X)
5. es : EO+(Message(f))
6. hdr : Name
7. locs : bag(Id)
8. hdr encodes Id × Message(g)
9. hdrs : Name List
10. i : Id
11. ∀e:E
      ((loc(e) = i ∈ Id)
      ⇒ (↑has-header-and-in-locs(info(e);hdr;locs))
      ⇒ (msg-header(snd(msgval(e))) ∈ hdrs)
      ⇒ (↓∃e':E. ((e' <loc e) ∧ (∃del:ℤ. <del, msgval(e)> ∈ local-simulation-class(X;locs;hdr)(e')))))@i
12. e : E@i
13. loc(e) = i ∈ Id@i
14. local-simulation-eo(es;e;hdr;locs) ∈ EO+(Message(g))
15. j : ℕ||filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))||@i
16. (header(j) ∈ hdrs)@i
17. j ∈ E
18. filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j] ≤loc e 
19. ↑has-header-and-in-locs(info(filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j]);hdr;locs)
20. e' : E
21. (e' <loc filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j])
22. del : ℤ
23. ↑has-header-and-in-locs(info(e');hdr;locs)
24. <del, msgval(filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j])> ∈
     X(local-simulation-event(es;e';hdr;locs))
25. msgval(filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j]) ∈ Id × Message(g)
26. (e' <loc e)
27. E ⊆r E
28. λx.x ∈ E ─→ E
29. local-simulation-event(es;e';hdr;locs) ∈ E
⊢ <loc(j), info(j)> ~ msgval(filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j])
BY
{ (Unfold `local-simulation-eo` 0
   THEN (RWO "global-eo-loc global-eo-info" 0 THENA Auto)
   THEN RepUR ``local-simulation-inputs mapfilter`` 0
   THEN (RWO "select-map" 0 THENA Auto)) }

1
1. f : Name ─→ Type
2. g : Name ─→ Type
3. X : EClass(Interface)
4. LocalClass(X)
5. es : EO+(Message(f))
6. hdr : Name
7. locs : bag(Id)
8. hdr encodes Id × Message(g)
9. hdrs : Name List
10. i : Id
11. ∀e:E
      ((loc(e) = i ∈ Id)
      ⇒ (↑has-header-and-in-locs(info(e);hdr;locs))
      ⇒ (msg-header(snd(msgval(e))) ∈ hdrs)
      ⇒ (↓∃e':E. ((e' <loc e) ∧ (∃del:ℤ. <del, msgval(e)> ∈ local-simulation-class(X;locs;hdr)(e')))))@i
12. e : E@i
13. loc(e) = i ∈ Id@i
14. local-simulation-eo(es;e;hdr;locs) ∈ EO+(Message(g))
15. j : ℤ@i
16. 0 ≤ j@i
17. j < ||filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))||@i
18. (header(j) ∈ hdrs)@i
19. j ∈ E
20. filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j] ≤loc e 
21. ↑has-header-and-in-locs(info(filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j]);hdr;locs)
22. e' : E
23. (e' <loc filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j])
24. del : ℤ
25. ↑has-header-and-in-locs(info(e');hdr;locs)
26. <del, msgval(filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j])> ∈
     X(local-simulation-event(es;e';hdr;locs))
27. msgval(filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j]) ∈ Id × Message(g)
28. (e' <loc e)
29. E ⊆r E
30. λx.x ∈ E ─→ E
31. local-simulation-event(es;e';hdr;locs) ∈ E
⊢ j < ||filter(λm.has-header-and-in-locs(m;hdr;locs);map(λe.info(e);≤loc(e)))||

2
1. f : Name ─→ Type
2. g : Name ─→ Type
3. X : EClass(Interface)
4. LocalClass(X)
5. es : EO+(Message(f))
6. hdr : Name
7. locs : bag(Id)
8. hdr encodes Id × Message(g)
9. hdrs : Name List
10. i : Id
11. ∀e:E
      ((loc(e) = i ∈ Id)
      ⇒ (↑has-header-and-in-locs(info(e);hdr;locs))
      ⇒ (msg-header(snd(msgval(e))) ∈ hdrs)
      ⇒ (↓∃e':E. ((e' <loc e) ∧ (∃del:ℤ. <del, msgval(e)> ∈ local-simulation-class(X;locs;hdr)(e')))))@i
12. e : E@i
13. loc(e) = i ∈ Id@i
14. local-simulation-eo(es;e;hdr;locs) ∈ EO+(Message(g))
15. j : ℕ||filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))||@i
16. (header(j) ∈ hdrs)@i
17. j ∈ E
18. filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j] ≤loc e 
19. ↑has-header-and-in-locs(info(filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j]);hdr;locs)
20. e' : E
21. (e' <loc filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j])
22. del : ℤ
23. ↑has-header-and-in-locs(info(e');hdr;locs)
24. <del, msgval(filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j])> ∈
     X(local-simulation-event(es;e';hdr;locs))
25. msgval(filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j]) ∈ Id × Message(g)
26. (e' <loc e)
27. E ⊆r E
28. λx.x ∈ E ─→ E
29. local-simulation-event(es;e';hdr;locs) ∈ E
⊢ <fst(((λm.msg-body(m)) filter(λm.has-header-and-in-locs(m;hdr;locs);map(λe.info(e);≤loc(e)))[j]))
  , snd(((λm.msg-body(m)) filter(λm.has-header-and-in-locs(m;hdr;locs);map(λe.info(e);≤loc(e)))[j]))
  > ~ msgval(filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j])

---

Latex:

---

Latex:

1.  f  :  Name  {}\mrightarrow{}  Type
2.  g  :  Name  {}\mrightarrow{}  Type
3.  X  :  EClass(Interface)
4.  LocalClass(X)
5.  es  :  EO+(Message(f))
6.  hdr  :  Name
7.  locs  :  bag(Id)
8.  hdr  encodes  Id  \mtimes{}  Message(g)
9.  hdrs  :  Name  List
10.  i  :  Id
11.  \mforall{}e:E
            ((loc(e)  =  i)
            {}\mRightarrow{}  (\muparrow{}has-header-and-in-locs(info(e);hdr;locs))
            {}\mRightarrow{}  (msg-header(snd(msgval(e)))  \mmember{}  hdrs)
            {}\mRightarrow{}  (\mdownarrow{}\mexists{}e':E
                        ((e'  <loc  e)  \mwedge{}  (\mexists{}del:\mBbbZ{}.  <del,  msgval(e)>  \mmember{}  local-simulation-class(X;locs;hdr)(e')))))@i
12.  e  :  E@i
13.  loc(e)  =  i@i
14.  local-simulation-eo(es;e;hdr;locs)  \mmember{}  EO+(Message(g))
15.  j  :  \mBbbN{}||filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);\mleq{}loc(e))||@i
16.  (header(j)  \mmember{}  hdrs)@i
17.  j  \mmember{}  E
18.  filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);\mleq{}loc(e))[j]  \mleq{}loc  e 
19.  \muparrow{}has-header-and-in-locs(info(filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);
                                                                                \mleq{}loc(e))[j]);hdr;locs)
20.  e'  :  E
21.  (e'  <loc  filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);\mleq{}loc(e))[j])
22.  del  :  \mBbbZ{}
23.  \muparrow{}has-header-and-in-locs(info(e');hdr;locs)
24.  <del,  msgval(filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);\mleq{}loc(e))[j])>  \mmember{}
          X(local-simulation-event(es;e';hdr;locs))
25.  msgval(filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);\mleq{}loc(e))[j])  \mmember{}  Id  \mtimes{}  Message(g)
26.  (e'  <loc  e)
27.  E  \msubseteq{}r  E
28.  \mlambda{}x.x  \mmember{}  E  {}\mrightarrow{}  E
29.  local-simulation-event(es;e';hdr;locs)  \mmember{}  E
\mvdash{}  <loc(j),  info(j)>  \msim{}  msgval(filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);\mleq{}loc(e))[j])


By

---

Latex:
(Unfold  `local-simulation-eo`  0
  THEN  (RWO  "global-eo-loc  global-eo-info"  0  THENA  Auto)
  THEN  RepUR  ``local-simulation-inputs  mapfilter``  0
  THEN  (RWO  "select-map"  0  THENA  Auto))

---

Home Index