---

Step * 1 of Lemma base-process-inputs_wf


1. f : Name ─→ Type
2. Info : Type
3. T : Type
4. X : EClass(T)
5. loc : Id
6. hdr : Name
7. hdr encodes Id × Info
8. es : EO+(Message(f))
9. e : E
10. v : {msg:Message(f)| ↑((λmsg.test-msg-header-and-loc(msg;hdr;loc)) msg)}  List@i
11. filter(λmsg.test-msg-header-and-loc(msg;hdr;loc);map(λe.info(e);≤loc(e)))
= v
∈ ({msg:Message(f)| ↑((λmsg.test-msg-header-and-loc(msg;hdr;loc)) msg)}  List)@i
⊢ map(λmsg.(snd(msg-body(msg)));v) ∈ Info List
BY
{ (Auto THEN Reduce (-1) THEN RWO "assert-test-msg-header-and-loc" (-1) THEN Auto) }

1
1. f : Name ─→ Type
2. Info : Type
3. T : Type
4. X : EClass(T)
5. loc : Id
6. hdr : Name
7. hdr encodes Id × Info
8. es : EO+(Message(f))
9. e : E
10. v : {msg:Message(f)| ↑((λmsg.test-msg-header-and-loc(msg;hdr;loc)) msg)}  List@i
11. filter(λmsg.test-msg-header-and-loc(msg;hdr;loc);map(λe.info(e);≤loc(e)))
= v
∈ ({msg:Message(f)| ↑((λmsg.test-msg-header-and-loc(msg;hdr;loc)) msg)}  List)@i
12. ∀msg:Message(f). (↑((λmsg.test-msg-header-and-loc(msg;hdr;loc)) msg) ∈ Type)
13. msg : Message(f)@i
14. msg-header(msg) = hdr ∈ Name
15. loc = (fst(msg-body(msg))) ∈ Id
⊢ snd(msg-body(msg)) ∈ Info

---

Latex:

---

Latex:

1.  f  :  Name  {}\mrightarrow{}  Type
2.  Info  :  Type
3.  T  :  Type
4.  X  :  EClass(T)
5.  loc  :  Id
6.  hdr  :  Name
7.  hdr  encodes  Id  \mtimes{}  Info
8.  es  :  EO+(Message(f))
9.  e  :  E
10.  v  :  \{msg:Message(f)|  \muparrow{}((\mlambda{}msg.test-msg-header-and-loc(msg;hdr;loc))  msg)\}    List@i
11.  filter(\mlambda{}msg.test-msg-header-and-loc(msg;hdr;loc);map(\mlambda{}e.info(e);\mleq{}loc(e)))  =  v@i
\mvdash{}  map(\mlambda{}msg.(snd(msg-body(msg)));v)  \mmember{}  Info  List


By

---

Latex:
(Auto  THEN  Reduce  (-1)  THEN  RWO  "assert-test-msg-header-and-loc"  (-1)  THEN  Auto)

---

Home Index