---

Step * of Lemma local-simulation-inputs_wf

∀[f:Name ⟶ Type]. ∀[Info:Type]. ∀[es:EO+(Message(f))]. ∀[hdr:Name]. ∀[locs:bag(Id)].
  ∀[e:E]. (local-simulation-inputs(es;e;hdr;locs) ∈ ({i:Id| i ↓∈ locs}  × Info) List) supposing hdr encodes Id × Info
BY
{ (Auto THEN Unfold `local-simulation-inputs` 0 THEN MemCD THEN Try (Complete (Auto))) }

1
.....subterm..... T:t
1:n
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
⊢ λm.msg-body(m) ∈ {x:Message(f)| ↑((λm.has-header-and-in-locs(m;hdr;locs)) x)}  ⟶ ({i:Id| i ↓∈ locs}  × Info)

---

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-inputs(es;e;hdr;locs)  \mmember{}  (\{i:Id|  i  \mdownarrow{}\mmember{}  locs\}    \mtimes{}  Info)  List)  supposing  hdr  \000Cencodes  Id  \mtimes{}  Info


By

---

Latex:
(Auto  THEN  Unfold  `local-simulation-inputs`  0  THEN  MemCD  THEN  Try  (Complete  (Auto)))

---

Home Index