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:
2016_05_15-PM-04_48_04
Last ObjectModification:
2015_09_23-AM-07_50_27
Theory : general
Home
Index