Nuprl Definition : run-local-pred

run-local-pred(r;i;t;t')
==r if (t' =z 0)
    then <t, i>
    else eval p = t' - 1 in
         if is-run-event(r;p;i) then <p, i> else run-local-pred(r;i;t;p) fi 
    fi 
run-local-pred(r;i;t;t') ==
  fix((λrun-local-pred,t'. if (t' =z 0)
                          then <t, i>
                          else eval p = t' - 1 in
                               if is-run-event(r;p;i) then <p, i> else run-local-pred p fi 
                          fi )) 
  t'


Definitions occuring in Statement :  is-run-event: is-run-event(r;t;x),  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  apply: f a,  fix: fix(F),  lambda: λx.A[x],  pair: <a, b>,  subtract: n - m,  natural_number: $n
FDL editor aliases :  run-local-pred
Latex:

run-local-pred(r;i;t;t')
==r  if  (t'  =\msubz{}  0)
        then  <t,  i>
        else  eval  p  =  t'  -  1  in
                  if  is-run-event(r;p;i)  then  <p,  i>  else  run-local-pred(r;i;t;p)  fi 
        fi 

Latex:
run-local-pred(r;i;t;t')  ==
    fix((\mlambda{}run-local-pred,t'.  if  (t'  =\msubz{}  0)
                                                    then  <t,  i>
                                                    else  eval  p  =  t'  -  1  in
                                                              if  is-run-event(r;p;i)  then  <p,  i>  else  run-local-pred  p  fi 
                                                    fi  )) 
    t'


Date html generated: 2015_07_23-AM-11_14_56
Last ObjectModification: 2014_02_23-PM-01_34_17

Home Index