---

Step * 1 1 1 of Lemma local-simulation-event-loc


1. f : Name ─→ Type
2. Info : Type
3. es : EO+(Message(f))
4. hdr : Name
5. locs : bag(Id)
6. hdr encodes Id × Info
7. e : E
8. ↑has-header-and-in-locs(info(e);hdr;locs)
9. v : Message(f) List@i
10. ¬||v|| < ||v||
11. filter(λm.has-header-and-in-locs(m;hdr;locs);map(λe.info(e);before(e))) = v ∈ (Message(f) List)@i
12. msg-header(info(e)) = hdr ∈ Name
13. fst(msg-body(info(e))) ↓∈ locs
⊢ msg-type(info(e);f) ⊆r (Id × Top)
BY
{ (Unfold `msg-type` 0 THEN HypSubst' (-2) 0 THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  Name  {}\mrightarrow{}  Type
2.  Info  :  Type
3.  es  :  EO+(Message(f))
4.  hdr  :  Name
5.  locs  :  bag(Id)
6.  hdr  encodes  Id  \mtimes{}  Info
7.  e  :  E
8.  \muparrow{}has-header-and-in-locs(info(e);hdr;locs)
9.  v  :  Message(f)  List@i
10.  \mneg{}||v||  <  ||v||
11.  filter(\mlambda{}m.has-header-and-in-locs(m;hdr;locs);map(\mlambda{}e.info(e);before(e)))  =  v@i
12.  msg-header(info(e))  =  hdr
13.  fst(msg-body(info(e)))  \mdownarrow{}\mmember{}  locs
\mvdash{}  msg-type(info(e);f)  \msubseteq{}r  (Id  \mtimes{}  Top)


By

---

Latex:
(Unfold  `msg-type`  0  THEN  HypSubst'  (-2)  0  THEN  Auto)

---

Home Index