[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification int-fac
enrich
   intlist
with
   

   
   
   functions  fac : int → int;
             comment: faculty.;
              binom_coef : int × int → int;
             comment: n choose k, 0 ≤ k ≤ n. 
                                           For other values of n and k the result is 0,
                                           which is consistent with the set definition.;
              binom_list : int × int × int × int → intlist;
              binom_list : int × int × int → intlist;
              max_exp : int × int → int;
             comment: max_exp(p, n): largest exponent of p (usually a prime) that divides n.;
   
   
   
   
   

   

   axioms fac-zero :  ⊦ i ≤ 0 → fac(i) = 1;
          used for: s, ls;
          fac-rec :  ⊦ 0 < i → fac(i) = i * fac(i - 1);
          binom-def :  ⊦ 0 ≤ j ∧ j ≤ i → binom_coef(i, j) = fac(i) / (fac(i - j) * fac(j));
          binom-less :  ⊦ ¬(0 ≤ j ∧ j ≤ i) → binom_coef(i, j) = 0;
          binomlist-def :  ⊦ binom_list(i, i0, j) = binom_list(i, i0, j, j);
          comment: (i + i0)^j ⇒ Σ (j choose j0) * i^j0 * j^(j-j0);
          binomlist-def2 :  ⊦ binom_list(i, i0, j) = countFun(0, j, λ j0. binom_coef(j, j0) * i ^ j0 * i0 ^ (j - j0));
          comment: (i + i0)^j ⇒ Σ (j choose j0) * i^j0 * j^(j-j0);
          binomlist-less :  ⊦ j0 < 0 → binom_list(i, i0, j, j0) = [];
          binomlist-rec :  ⊦ 0 ≤ j0 → binom_list(i, i0, j, j0) = binom_list(i, i0, j, j0 - 1) + (binom_coef(j, j0) * i ^ j0 * i0 ^ (j - j0))';
          max_exp-def :  ⊦ max_exp(i, j) = n→i(#oc(i, all_prime_divisors(j)));

   

   
end enrich