Nuprl Definition : proper-divisor
proper-divisor(n) ==
  case trial-division(n;[510510; 14535931; 75186702453419])
   of inl(x) =>
   inl x
   | inr(x) =>
   if n <z 5 then if (n =z 4) then inl 2 else inr (λx.any x)  fi 
   if n <z 16 then proper-divisor-aux(n;2;2;1;2)
   if n <z 81 then proper-divisor-aux(n;3;3;1;3)
   else eval m = iroot(4;n) + 1 in
        proper-divisor-aux(n;m;m;1;m)
   fi 
Definitions occuring in Statement : 
trial-division: trial-division(n;L), 
proper-divisor-aux: proper-divisor-aux(n;m;b;i;j), 
iroot: iroot(n;x), 
cons: [a / b], 
nil: [], 
any: any x, 
callbyvalue: callbyvalue, 
ifthenelse: if b then t else f fi , 
lt_int: i <z j, 
eq_int: (i =z j), 
lambda: λx.A[x], 
decide: case b of inl(x) => s[x] | inr(y) => t[y], 
inr: inr x , 
inl: inl x, 
add: n + m, 
natural_number: $n
Definitions occuring in definition : 
decide: case b of inl(x) => s[x] | inr(y) => t[y], 
trial-division: trial-division(n;L), 
cons: [a / b], 
nil: [], 
eq_int: (i =z j), 
inl: inl x, 
inr: inr x , 
lambda: λx.A[x], 
any: any x, 
ifthenelse: if b then t else f fi , 
lt_int: i <z j, 
callbyvalue: callbyvalue, 
add: n + m, 
iroot: iroot(n;x), 
proper-divisor-aux: proper-divisor-aux(n;m;b;i;j), 
natural_number: $n
FDL editor aliases : 
proper-divisor
Latex:
proper-divisor(n)  ==
    case  trial-division(n;[510510;  14535931;  75186702453419])
      of  inl(x)  =>
      inl  x
      |  inr(x)  =>
      if  n  <z  5  then  if  (n  =\msubz{}  4)  then  inl  2  else  inr  (\mlambda{}x.any  x)    fi 
      if  n  <z  16  then  proper-divisor-aux(n;2;2;1;2)
      if  n  <z  81  then  proper-divisor-aux(n;3;3;1;3)
      else  eval  m  =  iroot(4;n)  +  1  in
                proper-divisor-aux(n;m;m;1;m)
      fi 
Date html generated:
2016_05_15-PM-06_10_16
Last ObjectModification:
2015_09_23-AM-08_01_51
Theory : general
Home
Index