---

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