Nuprl Definition : combinations_aux_rem

combinations_aux_rem(b;n;m;k) ==
  fix((λcombinations_aux_rem,b,n,m. if (n =z 0)
                                   then b
                                   else eval b2 = b * m rem k in
                                        eval n2 = n - 1 in
                                        eval m2 = m - 1 in
                                          combinations_aux_rem b2 n2 m2
                                   fi )) 
  b 
  n 
  m


Definitions occuring in Statement :  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],  remainder: n rem m,  multiply: n * m,  subtract: n - m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  remainder: n rem m,  multiply: n * m,  callbyvalue: callbyvalue,  subtract: n - m,  natural_number: $n,  apply: f a
FDL editor aliases :  combinations_aux_rem
Latex:
combinations\_aux\_rem(b;n;m;k)  ==
    fix((\mlambda{}combinations\_aux$_{rem}$,b,n,m.  if  (n  =\msubz{}  0)
                                                                    then  b
                                                                    else  eval  b2  =  b  *  m  rem  k  in
                                                                              eval  n2  =  n  -  1  in
                                                                              eval  m2  =  m  -  1  in
                                                                                  combinations\_aux$_{rem}$  b2  n2  m2
                                                                    fi  )) 
    b 
    n 
    m


Date html generated: 2016_05_15-PM-06_00_12
Last ObjectModification: 2015_09_23-AM-08_00_38

Theory : general


Home Index