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