---

Step * 1 of Lemma local-simulation-event_wf


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]))||
BY
{ ((GenConclTerm ⌜filter(λm.has-header-and-in-locs(m;hdr;locs);map(λe.info(e);before(e)))⌝⋅ THENA Auto)
   THEN Reduce 0
   THEN SplitOnConclITE
   THEN Auto) }

---

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.  local-simulation-inputs(es;e;hdr;locs)  \mmember{}  (\{i:Id|  i  \mdownarrow{}\mmember{}  locs\}    \mtimes{}  Info)  List
\mvdash{}  ||filter(\mlambda{}m.has-header-and-in-locs(m;hdr;locs);map(\mlambda{}e.info(e);before(e)))||
    \mmember{}  \mBbbN{}||filter(\mlambda{}m.has-header-and-in-locs(m;hdr;locs);map(\mlambda{}e.info(e);before(e)))||
    +  ||filter(\mlambda{}m.has-header-and-in-locs(m;hdr;locs);map(\mlambda{}e.info(e);[e]))||


By

---

Latex:
((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  SplitOnConclITE
  THEN  Auto)

---

Home Index