Nuprl Definition : exp-rem

exp-rem(i;n;m) ==
  fix((λexp-rem,n. if n=1
                   then rem m
                   else if n=0
                        then rem m
                        else eval n' n ÷ in
                             eval exp-rem n' in
                               if rem 2=0 then rem else (i rem m))) 
  n



Definitions occuring in Statement :  callbyvalue: callbyvalue int_eq: if a=b then else d apply: a fix: fix(F) lambda: λx.A[x] remainder: rem m divide: n ÷ m multiply: m natural_number: $n
Definitions occuring in definition :  fix: fix(F) lambda: λx.A[x] divide: n ÷ m callbyvalue: callbyvalue apply: a int_eq: if a=b then else d natural_number: $n remainder: rem m multiply: m
FDL editor aliases :  exp-rem

Latex:
exp-rem(i;n;m)  ==
    fix((\mlambda{}exp-rem,n.  if  n=1
                                      then  i  rem  m
                                      else  if  n=0
                                                then  1  rem  m
                                                else  eval  n'  =  n  \mdiv{}  2  in
                                                          eval  x  =  exp-rem  n'  in
                                                              if  n  rem  2=0  then  x  *  x  rem  m  else  (i  *  x  *  x  rem  m))) 
    n



Date html generated: 2018_05_21-PM-01_07_52
Last ObjectModification: 2018_01_28-PM-02_02_50

Theory : num_thy_1


Home Index