---

Step * 1 of Lemma base-process-class-program_wf


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)
BY
{ (Unfold `base-process-inputs` 0
   THEN Unfold `es-le-before` 0
   THEN (RWO "map_append_sq" 0 THENA Auto)
   THEN Reduce 0
   THEN (RWO "filter_append_sq" 0 THENA Auto)
   THEN Reduce 0
   THEN AutoSplit
   THEN Unfold `mapfilter` 0
   THEN (GenConcl ⌈map(λe.info(e);before(e)) = L ∈ (Message(f) List)⌉⋅ THENA Auto)) }

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)
14. ↑test-msg-header-and-loc(info(e);hdr;loc)
15. L : Message(f) List@i
16. map(λe.info(e);before(e)) = L ∈ (Message(f) List)@i
⊢ let Infos = map(λmsg.(snd(msg-body(msg)));filter(λmsg.test-msg-header-and-loc(msg;hdr;loc);L) @ [info(e)]) in
      X list-eo(Infos;loc) (||Infos|| - 1)
= (snd(P loc*(map(λmsg.(snd(msg-body(msg)));filter(λmsg.test-msg-header-and-loc(msg;hdr;loc);
                                                   L)))(snd(msg-body(info(e))))))
∈ bag(T)

---

Latex:

---

Latex:

1.  f  :  Name  {}\mrightarrow{}  Type
2.  Info  :  Type
3.  T  :  Type
4.  loc  :  Id
5.  hdr  :  Name
6.  hdr  encodes  Id  \mtimes{}  Info
7.  \mforall{}[P:Id  {}\mrightarrow{}  hdataflow(Info;T)].  \mforall{}[L:Message(f)  List].  \mforall{}[m:Message(f)].  \mforall{}[i:Top].
          (snd(base-process-class-program(P;loc;hdr)  i*(L)(m))  \msim{}  if  test-msg-header-and-loc(m;hdr;loc)
          then  snd(P  loc*(mapfilter(\mlambda{}msg.(snd(msg-body(msg)));
                                                              \mlambda{}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)  \mmember{}  EClass(T)
11.  es  :  EO+(Message(f))@i'
12.  e  :  E@i
13.  \muparrow{}test-msg-header-and-loc(info(e);hdr;loc)
\mvdash{}  let  Infos  =  base-process-inputs(loc;hdr;es;e)  in
            X  list-eo(Infos;loc)  (||Infos||  -  1)
=  (snd(P  loc*(mapfilter(\mlambda{}msg.(snd(msg-body(msg)));
                                                \mlambda{}msg.test-msg-header-and-loc(msg;hdr;loc);
                                                map(\mlambda{}x.info(x);before(e))))(snd(msg-body(info(e))))))


By

---

Latex:
(Unfold  `base-process-inputs`  0
  THEN  Unfold  `es-le-before`  0
  THEN  (RWO  "map\_append\_sq"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (RWO  "filter\_append\_sq"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  AutoSplit
  THEN  Unfold  `mapfilter`  0
  THEN  (GenConcl  \mkleeneopen{}map(\mlambda{}e.info(e);before(e))  =  L\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index