---

Step * 1 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
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)
BY
{ ((Assert msg-body(info(e)) ∈ Id × Info BY
          OnMaybeHyp 14 (\h. (RWO "assert-test-msg-header-and-loc" h THEN Complete (Auto))))
   THEN (GenConclTerm ⌈snd(msg-body(info(e)))⌉⋅ THENA Auto)
   THEN All Thin) }

1
1. Info : Type
2. T : Type
3. loc : Id
4. X : EClass(T)
5. P : LocalClass(X)
6. ms' : Info List@i
7. v : Info@i
⊢ (X list-eo(ms' @ [v];loc) (||ms' @ [v]|| - 1)) = (snd(P loc*(ms')(v))) ∈ 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
18.  ms'  :  Info  List@i
19.  map(\mlambda{}msg.(snd(msg-body(msg)));ms)  =  ms'@i
\mvdash{}  (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))))))


By

---

Latex:
((Assert  msg-body(info(e))  \mmember{}  Id  \mtimes{}  Info  BY
                OnMaybeHyp  14  (\mbackslash{}h.  (RWO  "assert-test-msg-header-and-loc"  h  THEN  Complete  (Auto))))
  THEN  (GenConclTerm  \mkleeneopen{}snd(msg-body(info(e)))\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin)

---

Home Index