[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,

Theorem base summary for Specification int-fac

BertrandsPostulate(28,16)binomlist-def2(0,0)coef-neg(1,0)coef-sub-mult(30,17)fac-add(11,6)fac-zero-01(2,1)max_exp-lez(1,0)max_exp-same(2,1)middle-coef-max_exp-equality(16,10)prime-product-between(6,3)
Binom-theorem(2,2)binomlist-less(0,0)coef-neg-03(1,0)coef-succ(4,2)fac-divides(2,1)fac-zero-02(3,2)max_exp-mult(2,1)max_exp-smaller(1,0)middle-coef-max_exp-le(12,7)primes-divide(12,7)
Binom-theorem-countFun(43,26)binomlist-rec(0,0)coef-nls-zero(6,3)coef-switch(3,2)fac-le(18,9)max_exp-def(0,0)max_exp-mult-01(15,9)max_exp-zero(4,2)middle-coef-max_exp-stronger(6,4)product-all-elems-le(19,9)
bertrand-big-primes(4,2)coef-divides-rec(2,1)coef-one(4,2)coef-zero(2,1)fac-le-one(6,3)max_exp-div(4,2)max_exp-not-div(16,9)max_exp-zero-01(2,1)middle-coef-not-one(4,3)product-pot-no-dups(26,13)
bertrand-estimate(15,10)coef-divides-rec-lower(2,1)coef-pred-01(4,2)countFun-add(11,7)fac-le-zero(1,1)max_exp-div-not(15,7)max_exp-not-neg(3,2)max_exp-zero-02(4,2)middle-coef-not-one-01(5,3)product-pot-rec(10,3)
bertrand-holds-lower(24,12)coef-eq-zero(7,4)coef-product-le(12,6)countFun-pot(15,8)fac-ls-zero(2,1)max_exp-divides(9,6)max_exp-one(1,0)middle-coef-divides-not(13,8)prime-divides-coef(18,11)small-primes(20,10)
bertrand-middle-coef-smaller(42,22)coef-fac-divides(12,6)coef-rec(2,1)countFun-pot-01(13,8)fac-not-neg(6,3)max_exp-fac-01(10,5)max_exp-pos(1,1)middle-coef-larger(6,3)prime-divides-pot(10,4)
bertrand-middle-primes(25,16)coef-fac-divides-h(13,10)coef-rec-add-01(25,14)countFun-shift(23,13)fac-not-zero(2,1)max_exp-fac-add(12,6)max_exp-pos-01(2,1)middle-coef-larger-stronger(6,3)prime-divides-pot-01(10,4)
bertrand-prime-factors(25,12)coef-gcd(4,2)coef-rec-add-02(1,1)divides-pot(2,1)fac-one(1,1)max_exp-fac-gen(47,27)max_exp-pos-02(1,1)middle-coef-larger-strongest(35,19)prime-fac-divides(8,4)
bertrand-small-primes(18,9)coef-le-2pot(21,14)coef-rec-lower(2,1)divides-sum(5,3)fac-pos(1,0)max_exp-fac-gen-stronger(4,2)max_exp-pos-03(4,3)middle-coef-largest(9,5)prime-fac-divides-01(2,1)
binom-def(0,0)coef-le-zero(1,0)coef-same(2,1)est-4-big(9,5)fac-pos-01(6,3)max_exp-fac-rec(21,13)max_exp-pos-04(2,1)middle-coef-largest-01(17,10)prime-fac-divides-not(6,4)
binom-less(0,0)coef-mult-rec(20,14)coef-same-01(2,1)est-4-big-01(11,6)fac-rec(0,0)max_exp-fac-same(5,3)max_exp-primes-two(4,2)middle-coef-max_exp(34,21)prime-pot-eq(17,11)
binomlist-def(0,0)coef-mult-rec-lower(28,19)coef-sub(4,2)est-4-big-02(11,7)fac-zero(0,0)max_exp-fac-smaller(7,4)max_exp-rec(5,3)middle-coef-max_exp-big-primes(30,15)prime-product(36,21)