---

Step * of Lemma local-simulation-event_wf

∀[f:Name ─→ Type]. ∀[Info:Type]. ∀[es:EO+(Message(f))]. ∀[hdr:Name]. ∀[locs:bag(Id)].
  ∀[e:E]. local-simulation-event(es;e;hdr;locs) ∈ E supposing ↑has-header-and-in-locs(info(e);hdr;locs) 
  supposing hdr encodes Id × Info
BY
{ (Auto
   THEN Unfold `local-simulation-eo` 0
   THEN BLemma `global-eo-E`
   THEN RepUR ``local-simulation-event local-simulation-inputs es-le-before`` 0
   THEN RWW "length-mapfilter map_append_sq filter_append_sq length-append" 0
   THEN Auto) }

---

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]
        local-simulation-event(es;e;hdr;locs)  \mmember{}  E  supposing  \muparrow{}has-header-and-in-locs(info(e);hdr;locs) 
    supposing  hdr  encodes  Id  \mtimes{}  Info


By

---

Latex:
(Auto
  THEN  Unfold  `local-simulation-eo`  0
  THEN  BLemma  `global-eo-E`
  THEN  RepUR  ``local-simulation-event  local-simulation-inputs  es-le-before``  0
  THEN  RWW  "length-mapfilter  map\_append\_sq  filter\_append\_sq  length-append"  0
  THEN  Auto)

---

Home Index