Nuprl Definition : exp-rem

exp-rem(i;n;m) ==
  fix((λexp-rem,n. if n=1
                   then i rem m
                   else if n=0
                        then 1 rem m
                        else eval n' = n ÷ 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


Definitions occuring in Statement :  callbyvalue: callbyvalue,  int_eq: if a=b then c else d,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  remainder: n rem m,  divide: n ÷ m,  multiply: n * m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  divide: n ÷ m,  callbyvalue: callbyvalue,  apply: f a,  int_eq: if a=b then c else d,  natural_number: $n,  remainder: n rem m,  multiply: n * 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