Nuprl Definition : divisor-test

divisor-test(n;i;j) ==
  fix((λdivisor-test,i,j. eval p = iseg_product_rem(i;j;n) in
                          eval g = better-gcd(n;p) in
                            if 1 <z g
                            then if g <z n
                                 then inl g
                                 else eval k = i + ((j - i) ÷ 2) in
                                      case divisor-test i k
                                       of inl(x) =>
                                       inl x
                                       | inr(x) =>
                                       eval k' = k + 1 in
                                       divisor-test k' j
                                 fi 
                            else inr ⋅ 
                            fi )) 
  i 
  j


Definitions occuring in Statement :  iseg_product_rem: iseg_product_rem(i;j;k),  better-gcd: better-gcd(a;b),  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  it: ⋅,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inr: inr x ,  inl: inl x,  divide: n ÷ m,  subtract: n - m,  add: n + m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  iseg_product_rem: iseg_product_rem(i;j;k),  better-gcd: better-gcd(a;b),  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  divide: n ÷ m,  subtract: n - m,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inl: inl x,  callbyvalue: callbyvalue,  add: n + m,  natural_number: $n,  apply: f a,  inr: inr x ,  it: ⋅
FDL editor aliases :  divisor-test
Latex:
divisor-test(n;i;j)  ==
    fix((\mlambda{}divisor-test,i,j.  eval  p  =  iseg\_product\_rem(i;j;n)  in
                                                    eval  g  =  better-gcd(n;p)  in
                                                        if  1  <z  g
                                                        then  if  g  <z  n
                                                                  then  inl  g
                                                                  else  eval  k  =  i  +  ((j  -  i)  \mdiv{}  2)  in
                                                                            case  divisor-test  i  k
                                                                              of  inl(x)  =>
                                                                              inl  x
                                                                              |  inr(x)  =>
                                                                              eval  k'  =  k  +  1  in
                                                                              divisor-test  k'  j
                                                                  fi 
                                                        else  inr  \mcdot{} 
                                                        fi  )) 
    i 
    j


Date html generated: 2016_05_15-PM-06_08_27
Last ObjectModification: 2015_09_23-AM-08_01_23

Theory : general


Home Index