Nuprl Definition : proper-divisor-aux

proper-divisor-aux(n;m;b;i;j) ==
  fix((λproper-divisor-aux,b,i,j. if (b =z 0)
                                 then inr x.any x) 
                                 else case divisor-test(n;i;j)
                                       of inl(x) =>
                                       inl x
                                       inr(x) =>
                                       eval j' in
                                       eval i' in
                                       eval b' in
                                         proper-divisor-aux b' i' j'
                                 fi )) 

Definitions occuring in Statement :  divisor-test: divisor-test(n;i;j) any: any x callbyvalue: callbyvalue ifthenelse: if then else fi  eq_int: (i =z j) apply: a fix: fix(F) lambda: λx.A[x] decide: case of inl(x) => s[x] inr(y) => t[y] inr: inr  inl: inl x subtract: m add: m natural_number: $n
Definitions occuring in definition :  fix: fix(F) ifthenelse: if then else fi  eq_int: (i =z j) inr: inr  lambda: λx.A[x] any: any x decide: case of inl(x) => s[x] inr(y) => t[y] divisor-test: divisor-test(n;i;j) inl: inl x add: m callbyvalue: callbyvalue subtract: m natural_number: $n apply: a
FDL editor aliases :  proper-divisor-aux

proper-divisor-aux(n;m;b;i;j)  ==
    fix((\mlambda{}proper-divisor-aux,b,i,j.  if  (b  =\msubz{}  0)
                                                                  then  inr  (\mlambda{}x.any  x) 
                                                                  else  case  divisor-test(n;i;j)
                                                                              of  inl(x)  =>
                                                                              inl  x
                                                                              |  inr(x)  =>
                                                                              eval  j'  =  j  +  m  in
                                                                              eval  i'  =  j  +  1  in
                                                                              eval  b'  =  b  -  1  in
                                                                                  proper-divisor-aux  b'  i'  j'
                                                                  fi  )) 

Date html generated: 2016_05_15-PM-06_09_05
Last ObjectModification: 2015_09_23-AM-08_01_33

Theory : general

Home Index