---

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

∀[f:Name ⟶ Type]. ∀[Info,T:Type]. ∀[loc:Id]. ∀[hdr:Name].
  ∀[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 ) 
  supposing hdr encodes Id × Info
BY
{ (InstLemma `base-process-class-program-ap` []
   THEN RepeatFor 6 (ParallelLast')
   THEN (UnivCD THENA Auto)
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN MoveToConcl (-2)
   THEN ListInd (-1)
   THEN Reduce 0
   THEN (UnivCD THENA Auto)
   THEN (RWO "7" 0 THENA Auto)
   THEN ((BoolCase ⌜hdf-halted(P loc)⌝⋅ THENA Auto)
         THENL [((FLemma `hdf-halted-is-inr` [-1] THENA Auto)
                 THEN Fold `hdf-halt` (-1)
                 THEN HypSubst' (-1) 0
                 THEN (RWW "iterate-hdf-halt" 0 THENA Auto)
                 THEN Reduce 0
                 THEN AutoSplit)
               ; Id]
   )) }

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. P : Id ⟶ hdataflow(Info;T)@i
9. ¬↑hdf-halted(P loc)
10. m : Message(f)@i
11. i : Top@i
⊢ snd(if test-msg-header-and-loc(m;hdr;loc)
then let P',b = P loc(snd(msg-body(m))) 
     in <base-process-class-program(λi.P';loc;hdr) i, b>
else <base-process-class-program(P;loc;hdr) i, {}>
fi ) ~ if test-msg-header-and-loc(m;hdr;loc) then snd(P loc(snd(msg-body(m)))) else {} fi 

2
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 

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[Info,T:Type].  \mforall{}[loc:Id].  \mforall{}[hdr:Name].
    \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  ) 
    supposing  hdr  encodes  Id  \mtimes{}  Info


By

---

Latex:
(InstLemma  `base-process-class-program-ap`  []
  THEN  RepeatFor  6  (ParallelLast')
  THEN  (UnivCD  THENA  Auto)
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  MoveToConcl  (-2)
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  (UnivCD  THENA  Auto)
  THEN  (RWO  "7"  0  THENA  Auto)
  THEN  ((BoolCase  \mkleeneopen{}hdf-halted(P  loc)\mkleeneclose{}\mcdot{}  THENA  Auto)
              THENL  [((FLemma  `hdf-halted-is-inr`  [-1]  THENA  Auto)
                              THEN  Fold  `hdf-halt`  (-1)
                              THEN  HypSubst'  (-1)  0
                              THEN  (RWW  "iterate-hdf-halt"  0  THENA  Auto)
                              THEN  Reduce  0
                              THEN  AutoSplit)
                          ;  Id]
  ))

---

Home Index