---

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

∀[f:Name ─→ Type]. ∀[Info,T:Type]. ∀[loc:Id]. ∀[hdr:Name].
  ∀[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 ) 
  supposing hdr encodes Id × Top
BY
{ (Auto
   THEN RepUR ``base-process-class-program hdf-ap`` 0
   THEN RW (AddrC [1] (RecUnfoldC `mk-hdf`)) 0
   THEN RepUR ``hdf-run hdf-halt`` 0
   THEN Auto) }

---

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{}[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  ) 
    supposing  hdr  encodes  Id  \mtimes{}  Top


By

---

Latex:
(Auto
  THEN  RepUR  ``base-process-class-program  hdf-ap``  0
  THEN  RW  (AddrC  [1]  (RecUnfoldC  `mk-hdf`))  0
  THEN  RepUR  ``hdf-run  hdf-halt``  0
  THEN  Auto)

---

Home Index