---

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 InstLemma `local-simulation-inputs_wf` [⌜f⌝;⌜Info⌝;⌜es⌝;⌜hdr⌝;⌜locs⌝;⌜e⌝]⋅
         THEN Auto)
   THEN (BLemma `global-eo-E` THEN Auto)
   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 Try (Trivial)) }

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. local-simulation-inputs(es;e;hdr;locs) ∈ ({i:Id| i ↓∈ locs}  × Info) List
⊢ ||filter(λm.has-header-and-in-locs(m;hdr;locs);map(λe.info(e);before(e)))||
  ∈ ℕ||filter(λm.has-header-and-in-locs(m;hdr;locs);map(λe.info(e);before(e)))||
  + ||filter(λm.has-header-and-in-locs(m;hdr;locs);map(λe.info(e);[e]))||

---

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  InstLemma  `local-simulation-inputs\_wf`  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}hdr\mkleeneclose{};\mkleeneopen{}locs\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}
              THEN  Auto)
  THEN  (BLemma  `global-eo-E`  THEN  Auto)
  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  Try  (Trivial))

---

Home Index