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