---

Step * of Lemma local-simulation-event-loc

∀[f:Name ─→ Type]. ∀[Info:Type]. ∀[es:EO+(Message(f))]. ∀[hdr:Name]. ∀[locs:bag(Id)].
  ∀[e:E]
    loc(local-simulation-event(es;e;hdr;locs)) = (fst(msg-body(info(e)))) ∈ Id 
    supposing ↑has-header-and-in-locs(info(e);hdr;locs) 
  supposing hdr encodes Id × Info
BY
{ (Auto
   THEN RepUR ``local-simulation-eo`` 0
   THEN (RWO "global-eo-loc" 0 THENA Auto)
   THEN RepUR ``local-simulation-event local-simulation-inputs mapfilter`` 0
   THEN Unfold `es-le-before` 0
   THEN (RWW "map_append_sq filter_append_sq" 0 THENA Auto)
   THEN (GenConclTerm ⌈filter(λm.has-header-and-in-locs(m;hdr;locs);map(λe.info(e);before(e)))⌉⋅ THENA Auto)
   THEN Reduce 0
   THEN AutoSplit
   THEN (RWW "select-append length-map" 0 THENA Auto)
   THEN AutoSplit) }

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

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[Info:Type].  \mforall{}[es:EO+(Message(f))].  \mforall{}[hdr:Name].  \mforall{}[locs:bag(Id)].
    \mforall{}[e:E]
        loc(local-simulation-event(es;e;hdr;locs))  =  (fst(msg-body(info(e)))) 
        supposing  \muparrow{}has-header-and-in-locs(info(e);hdr;locs) 
    supposing  hdr  encodes  Id  \mtimes{}  Info


By

---

Latex:
(Auto
  THEN  RepUR  ``local-simulation-eo``  0
  THEN  (RWO  "global-eo-loc"  0  THENA  Auto)
  THEN  RepUR  ``local-simulation-event  local-simulation-inputs  mapfilter``  0
  THEN  Unfold  `es-le-before`  0
  THEN  (RWW  "map\_append\_sq  filter\_append\_sq"  0  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}filter(\mlambda{}m.has-header-and-in-locs(m;hdr;locs);map(\mlambda{}e.info(e);before(e)))\mkleeneclose{}\mcdot{}
              THENA  Auto
              )
  THEN  Reduce  0
  THEN  AutoSplit
  THEN  (RWW  "select-append  length-map"  0  THENA  Auto)
  THEN  AutoSplit)

---

Home Index