Nuprl Definition : rsc5_possmajstep

rsc5_possmajstep(Cmd;cmdeq) ==
  dc,c'.
   if isl(dc)
   then let n,c = outl(dc) 
        in if eqof(cmdeq) c c' then <n + 1, c>
           if eqof(IntDeq) n 0 then <1, c'>
           else <n - 1, c>
           fi 
   else <1, c'>
   fi 


Definitions occuring in Statement :  outl: outl(x),  isl: isl(x),  ifthenelse: if b then t else f fi ,  apply: f a,  lambda: x.A[x],  spread: spread def,  pair: <a, b>,  subtract: n - m,  add: n + m,  natural_number: $n,  int-deq: IntDeq,  eqof: eqof(d)
FDL editor aliases :  rsc5_possmajstep
rsc5\_possmajstep(Cmd;cmdeq)  ==
    \mlambda{}dc,c'.
      if  isl(dc)
      then  let  n,c  =  outl(dc) 
                in  if  eqof(cmdeq)  c  c'  then  <n  +  1,  c>
                      if  eqof(IntDeq)  n  0  then  ə,  c'>
                      else  <n  -  1,  c>
                      fi 
      else  ə,  c'>
      fi 


Date html generated: 2012_02_20-PM-05_05_09
Last ObjectModification: 2012_02_02-PM-02_17_55

Home Index