---

Step * of Lemma base-process-class-program_wf

∀[f:Name ⟶ Type]. ∀[Info,T:Type]. ∀[loc:Id]. ∀[hdr:Name].
  ∀[X:EClass(T)]. ∀[P:LocalClass(X)].
    (base-process-class-program(P;loc;hdr) ∈ LocalClass(base-process-class(X;loc;hdr))) 
  supposing hdr encodes Id × Info
BY
{ (InstLemma `iterate-base-process-class-program` []
   THEN RepeatFor 5 (ParallelLast')
   THEN (D 0 THENA Auto)
   THEN (D -2 THENA Auto)
   THEN Auto
   THEN (InstLemma `base-process-class_wf` [⌜f⌝;⌜Info⌝;⌜T⌝;⌜X⌝;⌜loc⌝;⌜hdr⌝]⋅ THENA Auto)
   THEN MemTypeCD
   THEN Auto
   THEN (RWO "7" 0 THENA Auto)
   THEN RepUR ``base-process-class class-ap`` 0
   THEN AutoSplit) }

1
1. f : Name ⟶ Type
2. Info : Type
3. T : Type
4. loc : Id
5. hdr : Name
6. hdr encodes Id × Info
7. ∀[P:Id ⟶ hdataflow(Info;T)]. ∀[L:Message(f) List]. ∀[m:Message(f)]. ∀[i:Top].
     (snd(base-process-class-program(P;loc;hdr) i*(L)(m)) ~ if test-msg-header-and-loc(m;hdr;loc)
     then snd(P loc*(mapfilter(λmsg.(snd(msg-body(msg)));
                               λmsg.test-msg-header-and-loc(msg;hdr;loc);
                               L))(snd(msg-body(m))))
     else {}
     fi )
8. X : EClass(T)
9. P : LocalClass(X)
10. base-process-class(X;loc;hdr) ∈ EClass(T)
11. es : EO+(Message(f))@i'
12. e : E@i
13. ↑test-msg-header-and-loc(info(e);hdr;loc)
⊢ let Infos = base-process-inputs(loc;hdr;es;e) in
      X list-eo(Infos;loc) (||Infos|| - 1)
= (snd(P loc*(mapfilter(λmsg.(snd(msg-body(msg)));
                        λmsg.test-msg-header-and-loc(msg;hdr;loc);
                        map(λx.info(x);before(e))))(snd(msg-body(info(e))))))
∈ bag(T)

---

Latex:

---

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


By

---

Latex:
(InstLemma  `iterate-base-process-class-program`  []
  THEN  RepeatFor  5  (ParallelLast')
  THEN  (D  0  THENA  Auto)
  THEN  (D  -2  THENA  Auto)
  THEN  Auto
  THEN  (InstLemma  `base-process-class\_wf`  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}loc\mkleeneclose{};\mkleeneopen{}hdr\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  MemTypeCD
  THEN  Auto
  THEN  (RWO  "7"  0  THENA  Auto)
  THEN  RepUR  ``base-process-class  class-ap``  0
  THEN  AutoSplit)

---

Home Index