---

Step * 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. ↑has-header-and-in-locs(info(e);hdr;locs)
⊢ (fst(msg-body(info(e)))) = (fst(msg-body(info(e)))) ∈ Id
BY
{ (RWO  "assert-has-header-and-in-locs" (-1) THEN Auto) }

1
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)

---

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.  \muparrow{}has-header-and-in-locs(info(e);hdr;locs)
\mvdash{}  (fst(msg-body(info(e))))  =  (fst(msg-body(info(e))))


By

---

Latex:
(RWO    "assert-has-header-and-in-locs"  (-1)  THEN  Auto)

---

Home Index