---

Step * 1 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
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
BY
{ (Assert ⌈msg-body(msg) ∈ Id × Info⌉⋅ THEN Auto) }

---

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
12.  \mforall{}msg:Message(f).  (\muparrow{}((\mlambda{}msg.test-msg-header-and-loc(msg;hdr;loc))  msg)  \mmember{}  Type)
13.  msg  :  Message(f)@i
14.  msg-header(msg)  =  hdr
15.  loc  =  (fst(msg-body(msg)))
\mvdash{}  snd(msg-body(msg))  \mmember{}  Info


By

---

Latex:
(Assert  \mkleeneopen{}msg-body(msg)  \mmember{}  Id  \mtimes{}  Info\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index