---

Step * 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))][||v|| - ||v||])) = (fst(msg-body(info(e)))) ∈ Id
BY
{ ((Subst' ||v|| - ||v|| ~ 0 0 THENA Auto) THEN Reduce 0) }

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. ↑has-header-and-in-locs(info(e);hdr;locs)
⊢ (fst(msg-body(info(e)))) = (fst(msg-body(info(e)))) ∈ Id

---

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))][||v||  -  ||v||]))  =  (fst(msg-body(info(e))))


By

---

Latex:
((Subst'  ||v||  -  ||v||  \msim{}  0  0  THENA  Auto)  THEN  Reduce  0)

---

Home Index