---

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


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))
BY
{ (BLemma `l_exists_iff` THENA 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. ↑test-msg-header-and-loc(info(e);hdr;loc)
⊢ ∃x:{a:E| loc(a) = loc(e) ∈ Id} . ((x ∈ ≤loc(e)) ∧ (↑test-msg-header-and-loc(info(x);hdr;loc)))

---

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.  \muparrow{}test-msg-header-and-loc(info(e);hdr;loc)
\mvdash{}  (\mexists{}x\mmember{}\mleq{}loc(e).  \muparrow{}test-msg-header-and-loc(info(x);hdr;loc))


By

---

Latex:
(BLemma  `l\_exists\_iff`  THENA  Auto)

---

Home Index