---

Step * of Lemma base-process-inputs-non-null

∀[f:Name ⟶ Type]. ∀[Info,T:Type]. ∀[X:EClass(T)]. ∀[loc:Id]. ∀[hdr:Name].
  ∀[es:EO+(Message(f))]. ∀[e:E].
    0 < ||base-process-inputs(loc;hdr;es;e)|| supposing ↑test-msg-header-and-loc(info(e);hdr;loc) 
  supposing hdr encodes Id × Info
BY
{ (Intros
   THEN Unfold `base-process-inputs` 0
   THEN (RWO "length-map" 0 THENA Auto)
   THEN (RW assert_pushdownC 0 THENA Auto)
   THEN BLemma `length-filter-pos`
   THEN Auto
   THEN Reduce 0
   THEN (RWO "l_exists_map" 0 THENA Auto)
   THEN Reduce 0) }

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. ↑test-msg-header-and-loc(info(e);hdr;loc)
⊢ (∃x∈≤loc(e). ↑test-msg-header-and-loc(info(x);hdr;loc))

---

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].
        0  <  ||base-process-inputs(loc;hdr;es;e)||  supposing  \muparrow{}test-msg-header-and-loc(info(e);hdr;loc) 
    supposing  hdr  encodes  Id  \mtimes{}  Info


By

---

Latex:
(Intros
  THEN  Unfold  `base-process-inputs`  0
  THEN  (RWO  "length-map"  0  THENA  Auto)
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  BLemma  `length-filter-pos`
  THEN  Auto
  THEN  Reduce  0
  THEN  (RWO  "l\_exists\_map"  0  THENA  Auto)
  THEN  Reduce  0)

---

Home Index