Step
*
1
of Lemma
local-simulation-inputs_wf
.....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)
BY
{ ((MemCD THENA Auto) THEN Reduce (-1) THEN D -1 THEN (RWO "assert-has-header-and-in-locs" (-1) THENA Auto)) }
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. m : Message(f)@i
9. (msg-header(m) = hdr ∈ Name) ∧ fst(msg-body(m)) ↓∈ locs
⊢ msg-body(m) ∈ {i:Id| i ↓∈ locs} × Info
Latex:
Latex:
.....subterm..... T:t
1:n
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
\mvdash{} \mlambda{}m.msg-body(m) \mmember{} \{x:Message(f)| \muparrow{}((\mlambda{}m.has-header-and-in-locs(m;hdr;locs)) x)\} {}\mrightarrow{} (\{i:Id| i \mdownarrow{}\mmember{} loc\000Cs\} \mtimes{} Info)
By
Latex:
((MemCD THENA Auto)
THEN Reduce (-1)
THEN D -1
THEN (RWO "assert-has-header-and-in-locs" (-1) THENA Auto))
Home
Index