---

Step * of Lemma base-process-class_wf

∀[f:Name ⟶ Type]. ∀[Info,T:Type]. ∀[X:EClass(T)]. ∀[loc:Id]. ∀[hdr:Name].
  base-process-class(X;loc;hdr) ∈ EClass(T) supposing hdr encodes Id × Info
BY
{ (InstLemma `base-process-inputs_wf` []⋅
   THEN RepeatFor 7 (ParallelLast')
   THEN RepUR ``base-process-class eclass let`` 0
   THEN RepeatFor 2 ((MemCD THENA Auto))
   THEN Fold `class-ap` 0
   THEN (BoolCase ⌜test-msg-header-and-loc(info(e);hdr;loc)⌝⋅ 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)
⊢ X(||base-process-inputs(loc;hdr;es;e)|| - 1) ∈ bag(T)

2
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)
⊢ {} ∈ bag(T)

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[Info,T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[loc:Id].  \mforall{}[hdr:Name].
    base-process-class(X;loc;hdr)  \mmember{}  EClass(T)  supposing  hdr  encodes  Id  \mtimes{}  Info


By

---

Latex:
(InstLemma  `base-process-inputs\_wf`  []\mcdot{}
  THEN  RepeatFor  7  (ParallelLast')
  THEN  RepUR  ``base-process-class  eclass  let``  0
  THEN  RepeatFor  2  ((MemCD  THENA  Auto))
  THEN  Fold  `class-ap`  0
  THEN  (BoolCase  \mkleeneopen{}test-msg-header-and-loc(info(e);hdr;loc)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index