---

Step * 1 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)
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)
BY
{ ((GenConcl ⌈filter(λmsg.test-msg-header-and-loc(msg;hdr;loc);L)
              = ms
              ∈ ({m:Message(f)| ↑((λmsg.test-msg-header-and-loc(msg;hdr;loc)) m)}  List)⌉⋅
    THENA Auto
    )
   THEN Thin (-1)
   THEN Reduce (-1)) }

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


By

---

Latex:
((GenConcl  \mkleeneopen{}filter(\mlambda{}msg.test-msg-header-and-loc(msg;hdr;loc);L)  =  ms\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  Reduce  (-1))

---

Home Index