---

pRun(S0;env;nat2msg;loc2msg) ==
  Y 
  (pRun,t.
    if (t = 0)
    then <inr  , S0>
    else let n,m,nm = env t pRun in 
         do-chosen-command(nat2msg;loc2msg;t;snd((pRun (t - 1)));n;m;nm)
    fi )

---

Definitions :  ycomb: Y,  lambda: x.A[x],  ifthenelse: if b then t else f fi ,  eq_int: (i = j),  pair: <a, b>,  inr: inr x ,  it: ,  spreadn: spread3,  do-chosen-command: do-chosen-command(nat2msg;loc2msg;t;S;n;m;nm),  pi2: snd(t),  apply: f a,  subtract: n - m,  natural_number: $n
FDL editor aliases :  pRun

---

pRun(S0;env;nat2msg;loc2msg)  ==
    Y 
    (\mlambda{}pRun,t.
        if  (t  =\msubz{}  0)
        then  <inr  \mcdot{}  ,  S0>
        else  let  n,m,nm  =  env  t  pRun  in 
                  do-chosen-command(nat2msg;loc2msg;t;snd((pRun  (t  -  1)));n;m;nm)
        fi  )


Date html generated: 2010_08_27-PM-03_53_18
Last ObjectModification: 2010_05_05-AM-11_56_24

Home Index