---

pRun2(S0;env;nat2msg;loc2msg;t) ==
  Y 
  (pRun2,t.
    if (t = 0)
    then let S := norm-system S0 in
         [<inr  , S>]
    else let r := pRun2 (t - 1) in
         let nxt := let info,S = let n,m,nm = env t (i.r[i]) in 
                    do-chosen-command(nat2msg;loc2msg;t;snd(last(r));n;m;nm) 
                    in let info' := norm-runinfo(info) in
                       let S' := norm-system S in
                         <info', S'> in
           r @ [nxt]
    fi ) 
  t

---

Definitions occuring in Statement :  norm-runinfo: norm-runinfo(info),  do-chosen-command: do-chosen-command(nat2msg;loc2msg;t;S;n;m;nm),  norm-system: norm-system,  select: l[i],  append: as @ bs,  eq_int: (i = j),  ifthenelse: if b then t else f fi ,  it: ,  spreadn: spread3,  pi2: snd(t),  ycomb: Y,  apply: f a,  lambda: x.A[x],  spread: spread def,  pair: <a, b>,  inr: inr x ,  cons: [car / cdr],  nil: [],  subtract: n - m,  natural_number: $n,  last: last(L),  callbyvalue: callbyvalue
Definitions :  ycomb: Y,  ifthenelse: if b then t else f fi ,  eq_int: (i = j),  inr: inr x ,  it: ,  subtract: n - m,  natural_number: $n,  spread: spread def,  spreadn: spread3,  lambda: x.A[x],  select: l[i],  do-chosen-command: do-chosen-command(nat2msg;loc2msg;t;S;n;m;nm),  pi2: snd(t),  last: last(L),  norm-runinfo: norm-runinfo(info),  callbyvalue: callbyvalue,  apply: f a,  norm-system: norm-system,  pair: <a, b>,  append: as @ bs,  cons: [car / cdr],  nil: []
FDL editor aliases :  pRun2

---

pRun2(S0;env;nat2msg;loc2msg;t)  ==
    Y 
    (\mlambda{}pRun2,t.
        if  (t  =\msubz{}  0)
        then  let  S  :=  norm-system  S0  in
                  [<inr  \mcdot{}  ,  S>]
        else  let  r  :=  pRun2  (t  -  1)  in
                  let  nxt  :=  let  info,S  =  let  n,m,nm  =  env  t  (\mlambda{}i.r[i])  in 
                                        do-chosen-command(nat2msg;loc2msg;t;snd(last(r));n;m;nm) 
                                        in  let  info'  :=  norm-runinfo(info)  in
                                              let  S'  :=  norm-system  S  in
                                                  <info',  S'>  in
                      r  @  [nxt]
        fi  ) 
    t


Date html generated: 2011_08_16-PM-06_56_18
Last ObjectModification: 2010_09_21-PM-05_49_34

Home Index