---

Step * 2 of Lemma iterate-base-process-class-program


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)]. ∀[a:Message(f)]. ∀[i:Top].
     (base-process-class-program(P;loc;hdr) i(a) ~ if hdf-halted(P loc) then <hdf-halt(), {}>
     if test-msg-header-and-loc(a;hdr;loc)
       then let P',b = P loc(snd(msg-body(a))) 
            in <base-process-class-program(λi.P';loc;hdr) i, b>
     else <base-process-class-program(P;loc;hdr) i, {}>
     fi )
8. u : Message(f)
9. v : Message(f) List
10. ∀P:Id ─→ hdataflow(Info;T). ∀m:Message(f). ∀i:Top.
      (snd(base-process-class-program(P;loc;hdr) i*(v)(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);
                                v))(snd(msg-body(m))))
      else {}
      fi )
11. P : Id ─→ hdataflow(Info;T)@i
12. ¬↑hdf-halted(P loc)
13. m : Message(f)@i
14. i : Top@i
⊢ snd(fst(if test-msg-header-and-loc(u;hdr;loc)
then let P',b = P loc(snd(msg-body(u))) 
     in <base-process-class-program(λi.P';loc;hdr) i, b>
else <base-process-class-program(P;loc;hdr) i, {}>
fi )*(v)(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);
                          [u / v]))(snd(msg-body(m))))
else {}
fi 
BY
{ ((RWO "mapfilter-cons" 0 THENA Auto)
   THEN (RWO "mapfilter-singleton" 0 THENA Auto)
   THEN Reduce 0
   THEN AutoSplit
   THEN Try (BackThruSomeHyp)) }

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)]. ∀[a:Message(f)]. ∀[i:Top].
     (base-process-class-program(P;loc;hdr) i(a) ~ if hdf-halted(P loc) then <hdf-halt(), {}>
     if test-msg-header-and-loc(a;hdr;loc)
       then let P',b = P loc(snd(msg-body(a))) 
            in <base-process-class-program(λi.P';loc;hdr) i, b>
     else <base-process-class-program(P;loc;hdr) i, {}>
     fi )
8. u : Message(f)
9. v : Message(f) List
10. ∀P:Id ─→ hdataflow(Info;T). ∀m:Message(f). ∀i:Top.
      (snd(base-process-class-program(P;loc;hdr) i*(v)(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);
                                v))(snd(msg-body(m))))
      else {}
      fi )
11. P : Id ─→ hdataflow(Info;T)@i
12. ¬↑hdf-halted(P loc)
13. m : Message(f)@i
14. i : Top@i
15. ↑test-msg-header-and-loc(u;hdr;loc)
⊢ snd(fst(let P',b = P loc(snd(msg-body(u))) 
          in <base-process-class-program(λi.P';loc;hdr) i, b>)*(v)(m)) ~ if test-msg-header-and-loc(m;hdr;loc)
then snd(fst(P loc(snd(msg-body(u))))*(mapfilter(λmsg.(snd(msg-body(msg)));
                                                 λmsg.test-msg-header-and-loc(msg;hdr;loc);
                                                 v))(snd(msg-body(m))))
else {}
fi 

---

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{}[a:Message(f)].  \mforall{}[i:Top].
          (base-process-class-program(P;loc;hdr)  i(a)  \msim{}  if  hdf-halted(P  loc)  then  <hdf-halt(),  \{\}>
          if  test-msg-header-and-loc(a;hdr;loc)
              then  let  P',b  =  P  loc(snd(msg-body(a))) 
                        in  <base-process-class-program(\mlambda{}i.P';loc;hdr)  i,  b>
          else  <base-process-class-program(P;loc;hdr)  i,  \{\}>
          fi  )
8.  u  :  Message(f)
9.  v  :  Message(f)  List
10.  \mforall{}P:Id  {}\mrightarrow{}  hdataflow(Info;T).  \mforall{}m:Message(f).  \mforall{}i:Top.
            (snd(base-process-class-program(P;loc;hdr)  i*(v)(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);
                                                                v))(snd(msg-body(m))))
            else  \{\}
            fi  )
11.  P  :  Id  {}\mrightarrow{}  hdataflow(Info;T)@i
12.  \mneg{}\muparrow{}hdf-halted(P  loc)
13.  m  :  Message(f)@i
14.  i  :  Top@i
\mvdash{}  snd(fst(if  test-msg-header-and-loc(u;hdr;loc)
then  let  P',b  =  P  loc(snd(msg-body(u))) 
          in  <base-process-class-program(\mlambda{}i.P';loc;hdr)  i,  b>
else  <base-process-class-program(P;loc;hdr)  i,  \{\}>
fi  )*(v)(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);
                                                    [u  /  v]))(snd(msg-body(m))))
else  \{\}
fi 


By

---

Latex:
((RWO  "mapfilter-cons"  0  THENA  Auto)
  THEN  (RWO  "mapfilter-singleton"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  AutoSplit
  THEN  Try  (BackThruSomeHyp))

---

Home Index