---

Step * 1 of Lemma base-process-class_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))]. ∀[e:E].  (base-process-inputs(loc;hdr;es;e) ∈ Info List)
9. es : EO+(Message(f))@i'
10. e : E@i
11. ↑test-msg-header-and-loc(info(e);hdr;loc)
⊢ X(||base-process-inputs(loc;hdr;es;e)|| - 1) ∈ bag(T)
BY
{ (InstLemma `base-process-inputs-non-null`  [⌈f⌉;⌈Info⌉;⌈T⌉;⌈X⌉;⌈loc⌉;⌈hdr⌉;⌈es⌉;⌈e⌉]⋅ 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))]. ∀[e:E].  (base-process-inputs(loc;hdr;es;e) ∈ Info List)
9. es : EO+(Message(f))@i'
10. e : E@i
11. ↑test-msg-header-and-loc(info(e);hdr;loc)
12. 0 < ||base-process-inputs(loc;hdr;es;e)||
⊢ X(||base-process-inputs(loc;hdr;es;e)|| - 1) ∈ bag(T)

---

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.  \mforall{}[es:EO+(Message(f))].  \mforall{}[e:E].    (base-process-inputs(loc;hdr;es;e)  \mmember{}  Info  List)
9.  es  :  EO+(Message(f))@i'
10.  e  :  E@i
11.  \muparrow{}test-msg-header-and-loc(info(e);hdr;loc)
\mvdash{}  X(||base-process-inputs(loc;hdr;es;e)||  -  1)  \mmember{}  bag(T)


By

---

Latex:
(InstLemma  `base-process-inputs-non-null`    [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}loc\mkleeneclose{};\mkleeneopen{}hdr\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index