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