---

Step * 1 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
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)
BY
{ (RepUR ``let`` 0
   THEN (RWO  "map_append_sq" 0 THENA Auto)
   THEN (GenConcl ⌈map(λmsg.(snd(msg-body(msg)));ms) = ms' ∈ (Info List)⌉⋅
         THENA (Auto
                THEN (RWO "assert-test-msg-header-and-loc" (-1) THENA Auto)
                THEN Assert ⌈msg-body(msg) ∈ Id × Info⌉⋅
                THEN Auto)
         )
   THEN Reduce 0) }

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


By

---

Latex:
(RepUR  ``let``  0
  THEN  (RWO    "map\_append\_sq"  0  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}map(\mlambda{}msg.(snd(msg-body(msg)));ms)  =  ms'\mkleeneclose{}\mcdot{}
              THENA  (Auto
                            THEN  (RWO  "assert-test-msg-header-and-loc"  (-1)  THENA  Auto)
                            THEN  Assert  \mkleeneopen{}msg-body(msg)  \mmember{}  Id  \mtimes{}  Info\mkleeneclose{}\mcdot{}
                            THEN  Auto)
              )
  THEN  Reduce  0)

---

Home Index