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' = j + m in
                                       eval i' = j + 1 in
                                       eval b' = b - 1 in
                                         proper-divisor-aux b' i' j'
                                 fi )) 
  b 
  i 
  j


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


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

Theory : general


Home Index