---

Step * of Lemma base-process-inputs_wf

∀[f:Name ─→ Type]. ∀[Info,T:Type]. ∀[X:EClass(T)]. ∀[loc:Id]. ∀[hdr:Name].
  ∀[es:EO+(Message(f))]. ∀[e:E].  (base-process-inputs(loc;hdr;es;e) ∈ Info List) supposing hdr encodes Id × Info
BY
{ (Auto
   THEN Unfold `base-process-inputs` 0
   THEN (GenConclAtAddrType ⌈{msg:Message(f)| ↑((λmsg.test-msg-header-and-loc(msg;hdr;loc)) msg)}  List⌉ [2;2]⋅
         THENA (Try ((BLemma `filter_type` THEN Auto)) 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
⊢ map(λmsg.(snd(msg-body(msg)));v) ∈ Info List

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[Info,T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[loc:Id].  \mforall{}[hdr:Name].
    \mforall{}[es:EO+(Message(f))].  \mforall{}[e:E].    (base-process-inputs(loc;hdr;es;e)  \mmember{}  Info  List) 
    supposing  hdr  encodes  Id  \mtimes{}  Info


By

---

Latex:
(Auto
  THEN  Unfold  `base-process-inputs`  0
  THEN  (GenConclAtAddrType 
              \mkleeneopen{}\{msg:Message(f)|  \muparrow{}((\mlambda{}msg.test-msg-header-and-loc(msg;hdr;loc))  msg)\}    List\mkleeneclose{}  [2;2]\mcdot{}
              THENA  (Try  ((BLemma  `filter\_type`  THEN  Auto))  THEN  Auto)
              ))

---

Home Index