---

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


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
⊢ snd(msg-body(info(e))) ∈ Info
BY
{ ((Assert msg-body(info(e)) ∈ Id × Info BY Auto) 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{}  snd(msg-body(info(e)))  \mmember{}  Info


By

---

Latex:
((Assert  msg-body(info(e))  \mmember{}  Id  \mtimes{}  Info  BY  Auto)  THEN  Auto)

---

Home Index