Used simplifier rules/spec theorems by specification

Used from specification int-basic1

• int-basic1/ls-rec is used by prime-product, max_exp-fac-gen, est-4-big-01,
• int-basic1/lsrec is used by middle-coef-max_exp-big-primes,
• int-basic1/trans is used by middle-coef-largest-01,
• int-basic1/forward-pos is used by primes-divide, prime-product, prime-pot-eq, prime-fac-divides-not, prime-divides-coef, middle-coef-not-one-01, middle-coef-max_exp-le, middle-coef-max_exp-equality, middle-coef-max_exp-big-primes, middle-coef-max_exp, max_exp-zero, max_exp-fac-smaller, max_exp-fac-gen-stronger, max_exp-fac-gen, max_exp-fac-01, fac-le-one, est-4-big-02, est-4-big-01, est-4-big, coef-rec-add-01, coef-product-le, coef-fac-divides-h, coef-fac-divides, bertrand-small-primes, bertrand-prime-factors, bertrand-middle-primes, bertrand-middle-coef-smaller, bertrand-holds-lower, bertrand-estimate, bertrand-big-primes, BertrandsPostulate,
• int-basic1/ls-01 is used by product-all-elems-le, prime-product-between, prime-product, prime-fac-divides-not, prime-divides-coef, middle-coef-max_exp-le, middle-coef-max_exp-equality, middle-coef-max_exp-big-primes, middle-coef-max_exp, middle-coef-larger-strongest, middle-coef-larger, middle-coef-divides-not, max_exp-fac-smaller, max_exp-fac-gen, max_exp-fac-add, max_exp-fac-01, fac-zero-01, fac-le, fac-add, est-4-big-02, est-4-big-01, est-4-big, coef-sub-mult, coef-same-01, coef-rec-add-01, coef-product-le, coef-mult-rec-lower, coef-mult-rec, coef-le-2pot, coef-fac-divides, bertrand-prime-factors, bertrand-middle-coef-smaller, BertrandsPostulate,
• int-basic1/lst-01 is used by product-pot-no-dups, primes-divide, prime-pot-eq, middle-coef-not-one-01, middle-coef-max_exp-big-primes, max_exp-pos-02,
• int-basic1/numlslsdel is used by middle-coef-max_exp-big-primes, bertrand-holds-lower,
• int-basic1/numlslsdel-01 is used by prime-product, middle-coef-max_exp-big-primes, est-4-big-02, est-4-big-01, est-4-big, bertrand-small-primes, bertrand-middle-primes, bertrand-middle-coef-smaller, bertrand-estimate, bertrand-big-primes, BertrandsPostulate,
• int-basic1/two-ls is used by middle-coef-max_exp-big-primes, max_exp-fac-gen, max_exp-divides, bertrand-holds-lower, BertrandsPostulate,

Used from specification int-mult

• int-mult/commutativity is used by product-all-elems-le, coef-mult-rec, coef-fac-divides-h,
• int-mult/dist-lsplit is used by est-4-big-02, coef-sub-mult, coef-rec-add-01, coef-fac-divides-h, bertrand-estimate, Binom-theorem-countFun,
• int-mult/dist-rmerge is used by coef-sub-mult,
• int-mult/dist-rsplit is used by est-4-big, Binom-theorem-countFun,
• int-mult/dist-sub-split is used by coef-sub-mult,
• int-mult/eq-nonzero is used by prime-pot-eq, coef-sub-mult, coef-mult-rec-lower,
• int-mult/eq-nonzero-01 is used by prime-pot-eq, coef-sub-mult,
• int-mult/le-one is used by fac-le,
• int-mult/le-pos is used by middle-coef-larger,
• int-mult/le-two is used by countFun-shift,
• int-mult/ls-add is used by coef-product-le,
• int-mult/ls-pos is used by primes-divide,
• int-mult/ls-pos-01 is used by product-pot-no-dups,
• int-mult/numls-10 is used by middle-coef-max_exp-big-primes,
• int-mult/numsucc is used by middle-coef-larger-strongest,
• int-mult/ple-pos-better is used by prime-product,
• int-mult/pls-pos-02 is used by product-pot-no-dups,
• int-mult/pnle-pos is used by fac-le,
• int-mult/pnls-pos is used by product-all-elems-le, fac-le, bertrand-middle-coef-smaller,
• int-mult/zero-eq is used by fac-not-zero,
• int-mult/zero-le is used by fac-le-zero,
• int-mult/zero-ls-02 is used by fac-ls-zero,
• int-mult/Mult-zero is used by primes-divide, prime-pot-eq, prime-divides-coef, middle-coef-largest-01, middle-coef-larger, max_exp-not-div, max_exp-mult-01, max_exp-fac-rec, max_exp-fac-gen, max_exp-divides, max_exp-div, est-4-big-02, est-4-big, coef-rec-lower, coef-rec-add-01, coef-rec, coef-mult-rec, coef-gcd, coef-fac-divides-h, coef-eq-zero,
• int-mult/add-mult-two is used by prime-product, middle-coef-max_exp-equality, middle-coef-max_exp-big-primes, middle-coef-max_exp, middle-coef-largest, countFun-shift, coef-sub-mult, coef-le-2pot,
• int-mult/associativity is used by product-pot-rec, product-pot-no-dups, primes-divide, prime-product, prime-pot-eq, prime-fac-divides-01, prime-fac-divides, prime-divides-pot-01, prime-divides-pot, prime-divides-coef, middle-coef-not-one-01, middle-coef-max_exp-stronger, middle-coef-max_exp-le, middle-coef-max_exp-equality, middle-coef-max_exp-big-primes, middle-coef-max_exp, middle-coef-largest-01, middle-coef-largest, middle-coef-larger-strongest, middle-coef-larger-stronger, middle-coef-larger, middle-coef-divides-not, max_exp-not-div, max_exp-mult-01, max_exp-fac-rec, max_exp-fac-gen, max_exp-fac-add, max_exp-divides, max_exp-div-not, max_exp-div, fac-pos-01, fac-one, fac-not-neg, fac-ls-zero, fac-le-zero, fac-le-one, fac-le, fac-divides, fac-add, est-4-big-02, est-4-big-01, est-4-big, divides-pot, countFun-shift, countFun-pot-01, countFun-pot, countFun-add, coef-zero, coef-succ, coef-sub-mult, coef-sub, coef-same, coef-rec-lower, coef-rec-add-01, coef-rec, coef-product-le, coef-pred-01, coef-one, coef-nls-zero, coef-mult-rec-lower, coef-mult-rec, coef-le-2pot, coef-gcd, coef-fac-divides-h, coef-fac-divides, coef-eq-zero, coef-divides-rec-lower, coef-divides-rec, bertrand-small-primes, bertrand-prime-factors, bertrand-middle-primes, bertrand-middle-coef-smaller, bertrand-holds-lower, bertrand-estimate, bertrand-big-primes, Binom-theorem-countFun, BertrandsPostulate,
• int-mult/commutativity is used by product-pot-rec, product-pot-no-dups, primes-divide, prime-product, prime-pot-eq, prime-fac-divides-01, prime-fac-divides, prime-divides-pot-01, prime-divides-pot, prime-divides-coef, middle-coef-not-one-01, middle-coef-max_exp-stronger, middle-coef-max_exp-le, middle-coef-max_exp-equality, middle-coef-max_exp-big-primes, middle-coef-max_exp, middle-coef-largest-01, middle-coef-largest, middle-coef-larger-strongest, middle-coef-larger-stronger, middle-coef-larger, middle-coef-divides-not, max_exp-not-div, max_exp-mult-01, max_exp-fac-rec, max_exp-fac-gen, max_exp-fac-add, max_exp-divides, max_exp-div-not, max_exp-div, fac-pos-01, fac-one, fac-not-neg, fac-ls-zero, fac-le-zero, fac-le-one, fac-le, fac-divides, fac-add, est-4-big-02, est-4-big-01, est-4-big, divides-pot, countFun-shift, countFun-pot-01, countFun-pot, countFun-add, coef-zero, coef-switch, coef-succ, coef-sub-mult, coef-sub, coef-same, coef-rec-lower, coef-rec-add-01, coef-rec, coef-product-le, coef-pred-01, coef-one, coef-nls-zero, coef-mult-rec-lower, coef-mult-rec, coef-le-2pot, coef-gcd, coef-fac-divides-h, coef-fac-divides, coef-eq-zero, coef-divides-rec-lower, coef-divides-rec, bertrand-small-primes, bertrand-prime-factors, bertrand-middle-primes, bertrand-middle-coef-smaller, bertrand-holds-lower, bertrand-estimate, bertrand-big-primes, Binom-theorem-countFun, BertrandsPostulate,
• int-mult/eq-dist is used by max_exp-fac-rec, countFun-shift, countFun-add, Binom-theorem-countFun,
• int-mult/eq-nonzero is used by product-pot-rec,
• int-mult/eq-one is used by prime-divides-pot,
• int-mult/eq-pos is used by middle-coef-max_exp-equality, middle-coef-max_exp-big-primes, middle-coef-max_exp, middle-coef-largest, fac-add, est-4-big, coef-le-2pot, BertrandsPostulate,
• int-mult/eq-same is used by fac-add,
• int-mult/le-one is used by fac-le-one,
• int-mult/le-pos is used by max_exp-fac-gen, bertrand-middle-coef-smaller,
• int-mult/le-same is used by prime-product,
• int-mult/le-same-01 is used by prime-divides-coef, middle-coef-max_exp-equality, middle-coef-max_exp, middle-coef-larger-strongest, middle-coef-divides-not, coef-le-2pot,
• int-mult/ls-add is used by max_exp-fac-gen,
• int-mult/ls-forward is used by product-pot-no-dups, primes-divide, middle-coef-max_exp-big-primes, coef-le-2pot,
• int-mult/ls-neg is used by primes-divide,
• int-mult/ls-pos is used by middle-coef-largest-01, est-4-big-02, coef-le-2pot, bertrand-middle-coef-smaller, bertrand-estimate, BertrandsPostulate,
• int-mult/ls-same is used by middle-coef-max_exp-equality, middle-coef-max_exp-big-primes, middle-coef-max_exp, middle-coef-largest-01, est-4-big-02, bertrand-middle-coef-smaller,
• int-mult/ls-same-01 is used by est-4-big-02, BertrandsPostulate,
• int-mult/mod-nle is used by max_exp-fac-gen,
• int-mult/mod-nls is used by max_exp-fac-gen,
• int-mult/neq-not-zero is used by product-pot-rec, coef-sub-mult, coef-le-2pot,
• int-mult/numeq-02 is used by middle-coef-max_exp-big-primes,
• int-mult/numeq-03 is used by coef-le-2pot,
• int-mult/numle-02 is used by middle-coef-larger,
• int-mult/numle-08 is used by prime-divides-coef, coef-product-le,
• int-mult/numle-09 is used by middle-coef-largest,
• int-mult/numle-12 is used by prime-divides-coef, coef-le-2pot,
• int-mult/numls-01 is used by prime-divides-coef, est-4-big-02,
• int-mult/numls-02 is used by middle-coef-largest-01,
• int-mult/numls-03 is used by bertrand-estimate,
• int-mult/numls-05 is used by middle-coef-largest, est-4-big,
• int-mult/numls-07 is used by prime-product,
• int-mult/numls-08 is used by est-4-big-02,
• int-mult/numsub is used by prime-divides-coef, coef-le-2pot,
• int-mult/numsucc is used by est-4-big-02, bertrand-estimate,
• int-mult/one is used by product-pot-rec, prime-product, prime-pot-eq, prime-divides-pot, prime-divides-coef, middle-coef-max_exp-le, middle-coef-max_exp-big-primes, middle-coef-max_exp, middle-coef-largest-01, middle-coef-largest, middle-coef-larger-strongest, middle-coef-larger-stronger, max_exp-fac-rec, fac-divides, est-4-big-02, est-4-big, countFun-add, coef-zero, coef-succ, coef-same, coef-rec-add-01, coef-product-le, coef-pred-01, coef-one, coef-le-2pot, coef-fac-divides-h, coef-fac-divides, bertrand-middle-coef-smaller, Binom-theorem-countFun, BertrandsPostulate,
• int-mult/one-01 is used by prime-pot-eq, max_exp-fac-gen, coef-rec-add-01, coef-product-le, bertrand-holds-lower, BertrandsPostulate,
• int-mult/zero-eq is used by coef-rec-add-01, coef-mult-rec,
• int-mult/zero-ge is used by prime-product, prime-divides-coef, middle-coef-max_exp-big-primes, middle-coef-largest, middle-coef-larger-strongest, middle-coef-larger, max_exp-fac-add, est-4-big-02, est-4-big-01, est-4-big, coef-rec-add-01, coef-le-2pot, bertrand-middle-coef-smaller, bertrand-estimate,
• int-mult/zero-ge-01 is used by fac-ls-zero,
• int-mult/zero-ge-02 is used by middle-coef-larger, coef-rec-add-01,
• int-mult/zero-ge-add is used by prime-product, est-4-big-02, est-4-big, coef-le-2pot, bertrand-estimate,
• int-mult/zero-gr is used by primes-divide, prime-divides-coef, middle-coef-not-one-01, middle-coef-max_exp-stronger, middle-coef-max_exp-le, middle-coef-max_exp-equality, middle-coef-max_exp-big-primes, middle-coef-max_exp, middle-coef-largest-01, middle-coef-larger-strongest, middle-coef-larger-stronger, middle-coef-divides-not, max_exp-not-div, max_exp-mult-01, max_exp-fac-rec, max_exp-fac-gen, max_exp-div, est-4-big-02, est-4-big, coef-rec-add-01, BertrandsPostulate,
• int-mult/zero-gr-01 is used by primes-divide, prime-product,
• int-mult/zero-gr-03 is used by fac-le-zero,
• int-mult/zero-le is used by fac-pos-01,
• int-mult/zero-ls is used by max_exp-fac-add, fac-not-neg,
• int-mult/zero-neq-01 is used by coef-mult-rec, coef-fac-divides-h,

Used from specification int-gcd

• int-gcd/coprime-divides is used by prime-divides-pot, coef-gcd,
• int-gcd/div-eq is used by coef-sub-mult, coef-eq-zero,
• int-gcd/div-mod-zero is used by coef-rec-add-01,
• int-gcd/div-mod-zero-01 is used by divides-pot,
• int-gcd/div-mult is used by max_exp-divides,
• int-gcd/div-mult-01 is used by coef-fac-divides-h,
• int-gcd/div-mult-shift is used by coef-sub-mult, coef-mult-rec,
• int-gcd/divides is used by primes-divide, prime-divides-coef, middle-coef-divides-not, max_exp-not-div, max_exp-mult-01, max_exp-div-not, max_exp-div, coef-sub-mult, coef-mult-rec-lower,
• int-gcd/divides-add is used by max_exp-zero,
• int-gcd/divides-mod is used by max_exp-div-not,
• int-gcd/divides-prime is used by primes-divide, max_exp-div-not,
• int-gcd/gcd-one-prime is used by prime-divides-pot,
• int-gcd/prime-1259 is used by small-primes,
• int-gcd/prime-13 is used by small-primes,
• int-gcd/prime-163 is used by small-primes,
• int-gcd/prime-23 is used by small-primes,
• int-gcd/prime-317 is used by small-primes,
• int-gcd/prime-43 is used by small-primes,
• int-gcd/prime-5 is used by small-primes,
• int-gcd/prime-631 is used by small-primes,
• int-gcd/prime-7 is used by small-primes,
• int-gcd/prime-83 is used by small-primes,
• int-gcd/prime-divides is used by prime-fac-divides-not, prime-divides-coef,
• int-gcd/div-mult is used by coef-sub-mult, coef-fac-divides, coef-divides-rec-lower, coef-divides-rec,
• int-gcd/div-not-ls is used by prime-fac-divides-not, max_exp-zero, max_exp-smaller, max_exp-not-div, max_exp-mult-01, max_exp-fac-add,
• int-gcd/div-one is used by max_exp-divides,
• int-gcd/div-one-one is used by prime-fac-divides,
• int-gcd/div-one-pos is used by prime-fac-divides-not, max_exp-fac-smaller, max_exp-fac-same, max_exp-fac-rec,
• int-gcd/div-zero is used by prime-pot-eq, prime-fac-divides-01, max_exp-zero, fac-divides, coef-fac-divides,
• int-gcd/div-zero-01 is used by divides-sum,
• int-gcd/div-zero-zero is used by max_exp-mult-01, coef-fac-divides-h,
• int-gcd/divides-add is used by divides-sum, coef-fac-divides-h,
• int-gcd/divides-mult-01 is used by prime-divides-pot-01, middle-coef-divides-not, max_exp-not-div, max_exp-mult-01,
• int-gcd/divides-mult-add is used by max_exp-fac-add,
• int-gcd/divides-prime is used by max_exp-zero,
• int-gcd/gcd-one-01 is used by prime-divides-pot,
• int-gcd/gcd-zero-04 is used by coef-gcd,
• int-gcd/prime-11 is used by max_exp-div-not,
• int-gcd/prime-abs is used by primes-divide, prime-divides-pot,
• int-gcd/prime-divides is used by primes-divide, prime-pot-eq, prime-fac-divides-01, prime-fac-divides, prime-divides-pot-01, prime-divides-coef, max_exp-not-div,
• int-gcd/prime-divides-one is used by prime-divides-pot-01, max_exp-one, max_exp-divides,
• int-gcd/prime-le-2 is used by bertrand-holds-lower, BertrandsPostulate,
• int-gcd/prime-not-neg is used by primes-divide, middle-coef-max_exp-big-primes,
• int-gcd/prime-not-neg-01 is used by primes-divide, prime-pot-eq, prime-fac-divides-01, prime-fac-divides, middle-coef-max_exp-le, max_exp-not-div, max_exp-mult-01, max_exp-fac-same, max_exp-fac-gen, bertrand-small-primes, bertrand-middle-coef-smaller,
• int-gcd/prime-one is used by primes-divide, prime-divides-pot, middle-coef-max_exp-stronger, middle-coef-max_exp-big-primes, middle-coef-max_exp, max_exp-fac-same, max_exp-fac-rec, bertrand-small-primes, bertrand-middle-primes,
• int-gcd/prime-small is used by middle-coef-max_exp-big-primes,
• int-gcd/prime-three is used by small-primes, bertrand-holds-lower, BertrandsPostulate,
• int-gcd/prime-two-01 is used by small-primes, prime-product, middle-coef-max_exp-big-primes, max_exp-div-not, bertrand-holds-lower, BertrandsPostulate,

Used from specification intlist

• intlist/all_prime_divisors-ordered is used by bertrand-prime-factors,
• intlist/all_prime_divisors-product is used by max_exp-divides, bertrand-middle-coef-smaller,
• intlist/all_prime_divisors-rec-01 is used by max_exp-rec,
• intlist/countFun-at is used by max_exp-fac-gen,
• intlist/countFun-base is used by middle-coef-max_exp-le, middle-coef-max_exp-big-primes, middle-coef-max_exp, fac-add, countFun-shift, countFun-pot-01, countFun-pot, countFun-add, Binom-theorem-countFun,
• intlist/countFun-dist is used by Binom-theorem-countFun,
• intlist/countFun-in is used by middle-coef-max_exp-le, middle-coef-max_exp, middle-coef-larger-strongest, max_exp-fac-add,
• intlist/countFun-last is used by middle-coef-larger-strongest, max_exp-fac-gen-stronger, fac-add, Binom-theorem-countFun,
• intlist/countFun-length is used by middle-coef-max_exp-le, middle-coef-max_exp, middle-coef-larger-strongest, max_exp-fac-gen,
• intlist/countFun-mult is used by middle-coef-max_exp-equality, middle-coef-max_exp, Binom-theorem-countFun,
• intlist/countFun-rec is used by middle-coef-max_exp-big-primes, middle-coef-larger-strongest, max_exp-fac-gen, countFun-shift, countFun-pot-01, countFun-pot, countFun-add, Binom-theorem-countFun,
• intlist/divide-list-at-value is used by prime-product,
• intlist/nodups-interval-size is used by bertrand-small-primes,
• intlist/primes-def is used by bertrand-middle-primes,
• intlist/product-divide is used by prime-product,
• intlist/product-negative is used by product-all-elems-le,
• intlist/product-positive is used by max_exp-fac-add, bertrand-middle-coef-smaller,
• intlist/product-prime-divides is used by max_exp-fac-add,
• intlist/sum-all-elems-le is used by middle-coef-max_exp-le, middle-coef-max_exp, middle-coef-larger-strongest,
• intlist/sum-constant-countFun is used by max_exp-fac-gen,
• intlist/sum-countFun-sub is used by middle-coef-max_exp-equality, middle-coef-max_exp,
• intlist/sum-countfun-not-ls is used by coef-le-2pot,
• intlist/sum-equal is used by max_exp-fac-gen,
• intlist/all_prime_divisors-base is used by max_exp-divides, bertrand-middle-coef-smaller,
• intlist/all_prime_divisors-in-01 is used by max_exp-zero-01, max_exp-zero, max_exp-divides, bertrand-small-primes, bertrand-prime-factors, bertrand-middle-primes, bertrand-middle-coef-smaller, bertrand-big-primes, BertrandsPostulate,
• intlist/all_prime_divisors-prime is used by max_exp-same,
• intlist/all_prime_divisors-product-del is used by max_exp-divides,
• intlist/countFun-base-01 is used by countFun-shift, countFun-pot-01, countFun-pot, countFun-add,
• intlist/countFun-one is used by middle-coef-max_exp-big-primes, Binom-theorem-countFun,
• intlist/max-empty is used by prime-product, bertrand-middle-primes,
• intlist/max-in-01 is used by bertrand-middle-primes,
• intlist/max-in-not-ls is used by prime-product-between,
• intlist/max-one is used by prime-product,
• intlist/max-perm-ls is used by prime-product,
• intlist/min-empty is used by product-pot-no-dups,
• intlist/min-in is used by product-pot-no-dups,
• intlist/min-in-not-ls is used by prime-product-between,
• intlist/primes-in is used by prime-product-between,
• intlist/primes-le-2 is used by prime-product,
• intlist/primes-max-even is used by prime-product,
• intlist/primes-one is used by prime-product,
• intlist/primes-perm-01 is used by prime-product,
• intlist/primes-perm-02 is used by prime-product,
• intlist/primes-product-not-neg is used by prime-product,
• intlist/prod-empty is used by product-pot-rec, product-pot-no-dups, product-all-elems-le, primes-divide, prime-product, max_exp-divides, fac-add, bertrand-middle-coef-smaller, BertrandsPostulate,
• intlist/prod-rec is used by product-pot-rec, product-all-elems-le, primes-divide, bertrand-middle-primes, bertrand-middle-coef-smaller, BertrandsPostulate,
• intlist/product-app is used by fac-add, bertrand-middle-primes, bertrand-middle-coef-smaller,
• intlist/product-min-nlz is used by product-pot-no-dups,
• intlist/product-one is used by prime-product, fac-add,
• intlist/sum-app is used by middle-coef-larger-strongest, max_exp-fac-gen-stronger, Binom-theorem-countFun,
• intlist/sum-empty is used by middle-coef-max_exp-big-primes, divides-sum, countFun-shift, countFun-pot, Binom-theorem-countFun,
• intlist/sum-one is used by middle-coef-max_exp-big-primes, middle-coef-larger-strongest, max_exp-fac-gen-stronger, Binom-theorem-countFun,
• intlist/sum-rec is used by middle-coef-max_exp-big-primes, middle-coef-larger-strongest, max_exp-fac-gen, divides-sum, countFun-shift, countFun-pot, Binom-theorem-countFun,

Used from specification int-square

• int-square/square-not-neg-03 is used by bertrand-small-primes, BertrandsPostulate,

Used from specification nat

• nat/lels is used by prime-product,
• nat/ls is used by max_exp-fac-gen,
• nat/ls-01 is used by coef-fac-divides,
• nat/pred-03 is used by max_exp-fac-gen, coef-fac-divides,

Used from specification int-pot

• int-pot/Pot-pos is used by product-pot-rec, product-all-elems-le, prime-product, prime-pot-eq, prime-divides-pot-01, prime-divides-pot, middle-coef-max_exp-big-primes, max_exp-fac-gen, countFun-pot-01, countFun-pot, coef-le-2pot, Binom-theorem-countFun, BertrandsPostulate,
• int-pot/exinpot is used by middle-coef-max_exp-stronger, middle-coef-max_exp-big-primes, middle-coef-max_exp,
• int-pot/le-pos is used by bertrand-estimate,
• int-pot/ls-pos is used by product-pot-no-dups, middle-coef-max_exp-stronger, middle-coef-max_exp, bertrand-small-primes, bertrand-middle-primes,
• int-pot/notneg-01 is used by middle-coef-max_exp-le,
• int-pot/pot-dist-pos is used by prime-product,
• int-pot/pot-div is used by bertrand-estimate,
• int-pot/pot-div3-nls is used by middle-coef-max_exp-big-primes,
• int-pot/pot-pot-02 is used by prime-product-between, middle-coef-larger-strongest,
• int-pot/pot-root-est is used by bertrand-estimate,
• int-pot/pot-square-04 is used by middle-coef-max_exp-big-primes,
• int-pot/succ is used by product-pot-no-dups,
• int-pot/Pot-zero is used by product-pot-rec, product-pot-no-dups, product-all-elems-le, prime-pot-eq, prime-divides-pot-01, prime-divides-pot, middle-coef-max_exp-le, middle-coef-max_exp-big-primes, middle-coef-max_exp, max_exp-fac-gen-stronger, max_exp-fac-gen, max_exp-divides, Binom-theorem-countFun,
• int-pot/grz is used by middle-coef-max_exp, max_exp-fac-gen, bertrand-estimate,
• int-pot/le-pos-01 is used by middle-coef-larger-stronger,
• int-pot/ls-pos is used by middle-coef-max_exp,
• int-pot/mod-same is used by divides-pot,
• int-pot/notneg-02 is used by product-pot-no-dups, prime-product, middle-coef-larger-stronger, middle-coef-larger, bertrand-estimate,
• int-pot/one is used by middle-coef-max_exp-le, middle-coef-max_exp-big-primes, middle-coef-max_exp, max_exp-fac-gen, countFun-add, Binom-theorem-countFun,
• int-pot/one-01 is used by product-pot-no-dups, middle-coef-larger-strongest, max_exp-fac-gen, coef-le-2pot, bertrand-small-primes,
• int-pot/pot-lez is used by product-pot-no-dups, prime-product, middle-coef-larger,
• int-pot/pot-nls is used by max_exp-fac-gen,
• int-pot/pot-zero-01 is used by product-pot-no-dups, prime-product, middle-coef-larger,
• int-pot/square-nls is used by bertrand-middle-primes,

Used from specification int-abs

• int-abs/Abs-neg is used by countFun-shift,
• int-abs/Abs-pos is used by middle-coef-larger-strongest, countFun-shift, countFun-pot-01, countFun-pot, countFun-add,
• int-abs/forward-lele is used by bertrand-middle-primes,
• int-abs/forward-lsle is used by max_exp-fac-gen,
• int-abs/le-rec is used by product-pot-no-dups, middle-coef-max_exp-big-primes,
• int-abs/lels-02 is used by max_exp-pos-03, BertrandsPostulate,
• int-abs/zero-eq is used by max_exp-pos-03,
• int-abs/zero-gs is used by max_exp-pos-01,
• int-abs/Abs-pos is used by countFun-shift,
• int-abs/Sub-def is used by middle-coef-max_exp-equality, middle-coef-largest-01, middle-coef-larger-strongest, max_exp-fac-rec, max_exp-fac-gen, coef-sub, coef-rec-add-01, coef-mult-rec, coef-fac-divides-h, coef-fac-divides,
• int-abs/abs is used by max_exp-zero, coef-fac-divides,
• int-abs/abs-03 is used by countFun-shift, countFun-pot-01, countFun-pot, countFun-add,
• int-abs/abs-16 is used by prime-divides-pot-01, max_exp-fac-gen,
• int-abs/abs-le-succ is used by max_exp-not-div, max_exp-mult-01,
• int-abs/absle is used by fac-le, coef-gcd, Binom-theorem-countFun,
• int-abs/abssub is used by countFun-pot-01, countFun-pot, countFun-add,
• int-abs/abssub-01 is used by middle-coef-largest-01, countFun-shift,
• int-abs/abssub-02 is used by middle-coef-largest-01,
• int-abs/anti is used by prime-product, prime-divides-pot, middle-coef-max_exp-le, middle-coef-max_exp, middle-coef-largest, middle-coef-larger-strongest, middle-coef-larger-stronger, middle-coef-larger, max_exp-fac-gen-stronger, max_exp-fac-gen, fac-le, fac-divides, countFun-pot-01, countFun-pot, countFun-add, coef-rec-add-01, coef-gcd, Binom-theorem-countFun,
• int-abs/bet is used by prime-pot-eq, prime-fac-divides-not, prime-fac-divides, middle-coef-max_exp-big-primes, max_exp-fac-smaller, max_exp-fac-same, max_exp-fac-rec, max_exp-fac-gen, fac-le-one, fac-le, coef-rec-add-01, coef-product-le, coef-fac-divides, bertrand-small-primes, BertrandsPostulate,
• int-abs/bet-01 is used by middle-coef-larger-strongest, max_exp-fac-rec, max_exp-fac-gen, est-4-big-02,
• int-abs/elim-sub is used by prime-divides-pot-01, prime-divides-pot, max_exp-fac-rec, fac-le, Binom-theorem-countFun,
• int-abs/forward-le is used by product-all-elems-le, prime-divides-coef, middle-coef-max_exp-le, middle-coef-max_exp, middle-coef-larger-strongest, max_exp-zero, max_exp-fac-gen, est-4-big-02, est-4-big-01, est-4-big, countFun-pot-01, countFun-add, coef-rec-lower, coef-rec-add-01, coef-mult-rec-lower, coef-mult-rec, coef-fac-divides, coef-divides-rec-lower, bertrand-small-primes, bertrand-middle-primes, bertrand-middle-coef-smaller, bertrand-holds-lower, bertrand-estimate, BertrandsPostulate,
• int-abs/forward-le-01 is used by product-pot-no-dups, product-all-elems-le, prime-product, prime-divides-pot-01, prime-divides-pot, prime-divides-coef, middle-coef-max_exp-stronger, middle-coef-max_exp-le, middle-coef-max_exp-equality, middle-coef-max_exp-big-primes, middle-coef-max_exp, middle-coef-largest-01, middle-coef-largest, middle-coef-larger-strongest, middle-coef-larger, middle-coef-divides-not, max_exp-zero, max_exp-fac-rec, max_exp-fac-gen-stronger, max_exp-fac-gen, max_exp-fac-add, max_exp-fac-01, max_exp-divides, fac-le, fac-divides, fac-add, est-4-big-02, est-4-big-01, est-4-big, coef-zero, coef-switch, coef-succ, coef-sub-mult, coef-same, coef-rec-add-01, coef-nls-zero, coef-mult-rec-lower, coef-mult-rec, coef-le-2pot, coef-gcd, coef-fac-divides-h, coef-eq-zero, bertrand-small-primes, bertrand-middle-primes, bertrand-middle-coef-smaller, bertrand-estimate, Binom-theorem-countFun,
• int-abs/forward-le-02 is used by product-pot-no-dups, product-all-elems-le, middle-coef-largest-01, max_exp-pos-04, max_exp-pos-01, fac-zero-01, fac-not-neg, coef-nls-zero, bertrand-middle-coef-smaller,
• int-abs/forward-le-04 is used by product-pot-no-dups, middle-coef-max_exp-le, middle-coef-larger, max_exp-pos-03, max_exp-not-div, max_exp-mult-01, max_exp-fac-gen, max_exp-fac-add, fac-pos-01, fac-add, est-4-big-02, est-4-big, bertrand-middle-coef-smaller,
• int-abs/forward-le-05 is used by product-pot-no-dups, product-all-elems-le, primes-divide, prime-product-between, prime-product, prime-pot-eq, prime-fac-divides-not, prime-fac-divides, prime-divides-pot-01, prime-divides-pot, prime-divides-coef, middle-coef-not-one-01, middle-coef-not-one, middle-coef-max_exp-stronger, middle-coef-max_exp-le, middle-coef-max_exp-equality, middle-coef-max_exp-big-primes, middle-coef-max_exp, middle-coef-largest-01, middle-coef-larger-strongest, middle-coef-larger-stronger, middle-coef-larger, middle-coef-divides-not, max_exp-zero-02, max_exp-zero-01, max_exp-zero, max_exp-rec, max_exp-pos-03, max_exp-pos-02, max_exp-not-div, max_exp-mult-01, max_exp-mult, max_exp-fac-smaller, max_exp-fac-same, max_exp-fac-rec, max_exp-fac-gen-stronger, max_exp-fac-gen, max_exp-fac-add, max_exp-fac-01, max_exp-divides, max_exp-div, fac-pos-01, fac-not-neg, fac-le-one, fac-le, fac-add, est-4-big-02, est-4-big-01, est-4-big, divides-pot, countFun-pot-01, countFun-add, coef-sub-mult, coef-sub, coef-same-01, coef-rec-lower, coef-rec-add-01, coef-rec, coef-product-le, coef-pred-01, coef-one, coef-mult-rec-lower, coef-mult-rec, coef-le-zero, coef-le-2pot, coef-fac-divides-h, coef-fac-divides, coef-divides-rec-lower, coef-divides-rec, bertrand-small-primes, bertrand-prime-factors, bertrand-middle-primes, bertrand-middle-coef-smaller, bertrand-holds-lower, bertrand-estimate, bertrand-big-primes, Binom-theorem-countFun, BertrandsPostulate,
• int-abs/forward-lele is used by product-pot-no-dups, product-all-elems-le, prime-product-between, prime-product, prime-divides-coef, middle-coef-max_exp-le, middle-coef-max_exp-big-primes, middle-coef-largest, middle-coef-larger-stronger, middle-coef-larger, max_exp-fac-gen, max_exp-fac-add, fac-divides, fac-add, countFun-pot-01, countFun-pot, countFun-add, coef-product-le, coef-mult-rec-lower, coef-gcd, bertrand-small-primes, bertrand-estimate,
• int-abs/forward-lels is used by product-pot-no-dups, prime-product-between, prime-product, middle-coef-not-one-01, middle-coef-max_exp-stronger, middle-coef-max_exp-le, middle-coef-max_exp-equality, middle-coef-max_exp-big-primes, middle-coef-max_exp, middle-coef-largest-01, max_exp-not-div, max_exp-mult-01, max_exp-fac-gen, max_exp-fac-add, fac-pos-01, fac-le-one, fac-add, est-4-big-02, est-4-big-01, est-4-big, bertrand-small-primes, bertrand-middle-primes, bertrand-middle-coef-smaller, bertrand-estimate,
• int-abs/forward-lsle is used by prime-product-between, prime-product, prime-divides-coef, middle-coef-max_exp-le, middle-coef-max_exp-equality, middle-coef-max_exp-big-primes, middle-coef-max_exp, middle-coef-largest-01, max_exp-fac-gen, max_exp-fac-add, fac-le, est-4-big-02, est-4-big-01, est-4-big, countFun-shift, coef-sub-mult, coef-sub, coef-rec, coef-nls-zero, coef-divides-rec, bertrand-small-primes, bertrand-middle-coef-smaller, bertrand-estimate, bertrand-big-primes, BertrandsPostulate,
• int-abs/ge-def is used by middle-coef-larger-strongest, middle-coef-larger-stronger, middle-coef-larger, bertrand-estimate, BertrandsPostulate,
• int-abs/int-add-pos is used by prime-divides-coef,
• int-abs/int-simp-07 is used by middle-coef-larger-strongest,
• int-abs/le-add is used by prime-product, prime-divides-coef, fac-le, coef-le-2pot,
• int-abs/le-add-02 is used by coef-le-2pot,
• int-abs/le-add-03 is used by countFun-add, coef-sub-mult, coef-mult-rec-lower,
• int-abs/lels is used by product-pot-no-dups, primes-divide, prime-product, prime-pot-eq, prime-fac-divides-not, prime-fac-divides-01, prime-fac-divides, prime-divides-pot, prime-divides-coef, middle-coef-not-one-01, middle-coef-max_exp-stronger, middle-coef-max_exp-le, middle-coef-max_exp-equality, middle-coef-max_exp-big-primes, middle-coef-max_exp, middle-coef-largest-01, middle-coef-largest, middle-coef-larger-strongest, middle-coef-larger-stronger, middle-coef-larger, max_exp-not-div, max_exp-mult-01, max_exp-fac-smaller, max_exp-fac-same, max_exp-fac-rec, max_exp-fac-gen-stronger, max_exp-fac-gen, max_exp-fac-add, max_exp-fac-01, fac-pos-01, fac-not-neg, fac-ls-zero, fac-le-zero, fac-le, fac-divides, fac-add, est-4-big-02, est-4-big, countFun-shift, countFun-pot-01, countFun-pot, countFun-add, coef-rec-add-01, coef-product-le, coef-nls-zero, coef-le-2pot, coef-gcd, coef-fac-divides-h, coef-fac-divides, coef-eq-zero, bertrand-small-primes, bertrand-middle-primes, bertrand-middle-coef-smaller, bertrand-estimate, Binom-theorem-countFun, BertrandsPostulate,
• int-abs/lels-01 is used by product-pot-no-dups, product-all-elems-le, primes-divide, prime-product-between, prime-product, prime-fac-divides-not, prime-divides-coef, middle-coef-max_exp-stronger, middle-coef-max_exp-le, middle-coef-max_exp-equality, middle-coef-max_exp-big-primes, middle-coef-max_exp, middle-coef-largest-01, middle-coef-larger-strongest, middle-coef-larger-stronger, middle-coef-larger, middle-coef-divides-not, max_exp-pos-03, max_exp-lez, max_exp-fac-smaller, max_exp-fac-gen, max_exp-fac-add, max_exp-fac-01, max_exp-divides, fac-zero-01, fac-ls-zero, fac-le-zero, fac-le-one, fac-le, est-4-big-02, est-4-big-01, est-4-big, countFun-shift, countFun-pot, coef-succ, coef-sub-mult, coef-same-01, coef-rec-add-01, coef-product-le, coef-nls-zero, coef-mult-rec-lower, coef-mult-rec, coef-le-zero, coef-le-2pot, coef-fac-divides, bertrand-small-primes, bertrand-prime-factors, bertrand-middle-primes, bertrand-middle-coef-smaller, bertrand-holds-lower, bertrand-estimate, bertrand-big-primes, Binom-theorem-countFun, BertrandsPostulate,
• int-abs/lels-02 is used by prime-divides-pot-01, middle-coef-max_exp-big-primes, middle-coef-larger-strongest, middle-coef-larger, max_exp-lez, max_exp-fac-gen, max_exp-fac-01, fac-add, est-4-big-02, est-4-big-01, coef-rec-add-01, coef-le-zero, coef-fac-divides, Binom-theorem-countFun,
• int-abs/lels-03 is used by product-all-elems-le, primes-divide, prime-product-between, prime-product, prime-pot-eq, prime-fac-divides-not, prime-fac-divides, middle-coef-not-one-01, middle-coef-max_exp-stronger, middle-coef-max_exp-le, middle-coef-max_exp, middle-coef-larger-strongest, max_exp-fac-smaller, max_exp-fac-rec, max_exp-fac-gen-stronger, max_exp-fac-gen, fac-pos-01, fac-not-neg, fac-le-zero, est-4-big-02, est-4-big, countFun-shift, coef-product-le, coef-le-2pot, coef-fac-divides-h, coef-fac-divides, bertrand-middle-primes, bertrand-middle-coef-smaller,
• int-abs/lenls is used by product-pot-no-dups, prime-product, middle-coef-max_exp-big-primes, max_exp-fac-gen, fac-ls-zero, fac-le, fac-add, countFun-shift, countFun-pot, countFun-add, coef-succ, coef-sub-mult, coef-rec-add-01, coef-mult-rec-lower, coef-eq-zero, bertrand-small-primes, bertrand-estimate, Binom-theorem-countFun, BertrandsPostulate,
• int-abs/leone is used by primes-divide, prime-product, prime-divides-coef, middle-coef-max_exp-le, middle-coef-max_exp-big-primes, middle-coef-max_exp, middle-coef-largest-01, middle-coef-larger-strongest, max_exp-fac-rec, max_exp-fac-gen-stronger, max_exp-fac-gen, max_exp-fac-add, max_exp-fac-01, fac-le, fac-add, coef-sub-mult, coef-sub, coef-rec-add-01, coef-product-le, coef-pred-01, coef-one, coef-mult-rec-lower, coef-mult-rec, coef-fac-divides, bertrand-small-primes, Binom-theorem-countFun,
• int-abs/lep is used by countFun-shift, countFun-pot-01, countFun-pot, countFun-add, coef-switch, coef-succ, coef-pred-01,
• int-abs/lep-01 is used by prime-divides-coef, countFun-shift, countFun-pot-01, countFun-pot, countFun-add,
• int-abs/ler is used by prime-product, prime-fac-divides, middle-coef-max_exp, middle-coef-largest-01, middle-coef-largest, max_exp-fac-same, max_exp-fac-rec, countFun-shift, coef-same, coef-fac-divides,
• int-abs/les is used by prime-fac-divides, prime-divides-coef, middle-coef-largest-01, countFun-shift,
• int-abs/lsone is used by prime-product, prime-pot-eq, prime-fac-divides, middle-coef-not-one-01, max_exp-fac-gen-stronger, max_exp-fac-gen, fac-pos, fac-le-one,
• int-abs/minus-add is used by prime-divides-coef, max_exp-fac-gen, countFun-shift, coef-product-le,
• int-abs/minus-sub is used by countFun-shift,
• int-abs/mone-05 is used by fac-le,
• int-abs/mone-06 is used by product-pot-rec, product-all-elems-le, prime-product, prime-fac-divides, prime-divides-pot-01, prime-divides-pot, prime-divides-coef, middle-coef-largest-01, middle-coef-larger, max_exp-fac-gen, fac-le, coef-succ, coef-le-2pot, Binom-theorem-countFun,
• int-abs/neg-06 is used by countFun-shift, Binom-theorem-countFun,
• int-abs/numadd is used by countFun-shift,
• int-abs/numadd-01 is used by middle-coef-max_exp-big-primes, middle-coef-larger-strongest, max_exp-zero-02, max_exp-fac-same, max_exp-fac-rec, coef-rec-add-01, Binom-theorem-countFun,
• int-abs/numle-01 is used by prime-divides-coef, coef-product-le,
• int-abs/numle-02 is used by prime-product, prime-divides-pot, prime-divides-coef, middle-coef-max_exp-equality, middle-coef-max_exp, middle-coef-largest-01, max_exp-fac-gen, fac-le, coef-le-2pot, Binom-theorem-countFun,
• int-abs/numle-03 is used by fac-le, est-4-big-02, est-4-big, bertrand-middle-primes,
• int-abs/numleledel is used by fac-le-one,
• int-abs/numleledel-01 is used by prime-product, prime-divides-pot, prime-divides-coef, middle-coef-max_exp-equality, middle-coef-max_exp-big-primes, middle-coef-max_exp, middle-coef-largest-01, max_exp-fac-gen, fac-le, coef-le-2pot, Binom-theorem-countFun,
• int-abs/numlelsdel is used by est-4-big-01, bertrand-holds-lower,
• int-abs/numlelsdel-01 is used by primes-divide, prime-pot-eq, middle-coef-max_exp-big-primes, coef-fac-divides, bertrand-middle-coef-smaller, bertrand-big-primes,
• int-abs/numls-02 is used by product-pot-rec, product-all-elems-le, prime-product, prime-fac-divides, prime-divides-pot-01, prime-divides-pot, prime-divides-coef, middle-coef-largest-01, middle-coef-larger, max_exp-fac-gen, fac-le, coef-succ, coef-le-2pot, Binom-theorem-countFun,
• int-abs/numls-03 is used by middle-coef-max_exp-big-primes,
• int-abs/numlsledel is used by bertrand-holds-lower,
• int-abs/numlsledel-01 is used by max_exp-fac-gen, est-4-big-01,
• int-abs/numsub is used by prime-product, prime-fac-divides, middle-coef-max_exp-le, middle-coef-max_exp-equality, middle-coef-max_exp, middle-coef-largest-01, max_exp-fac-gen, countFun-shift, coef-succ, coef-rec-lower, coef-rec-add-02, Binom-theorem-countFun,
• int-abs/sub-add is used by middle-coef-largest-01, countFun-add, coef-switch, coef-succ, coef-sub-mult, coef-pred-01,
• int-abs/sub-add-01 is used by middle-coef-max_exp-big-primes, max_exp-fac-rec, max_exp-fac-01, fac-add, countFun-shift, countFun-pot-01, countFun-pot, countFun-add, coef-sub-mult,
• int-abs/sub-add-05 is used by countFun-pot-01, countFun-pot, countFun-add, Binom-theorem-countFun,
• int-abs/sub-add-06 is used by middle-coef-largest-01, countFun-shift, countFun-pot, coef-sub-mult, coef-mult-rec-lower, coef-le-2pot,
• int-abs/sub-add-09 is used by coef-rec-add-01,
• int-abs/sub-eq is used by middle-coef-max_exp-equality, middle-coef-max_exp-big-primes, middle-coef-max_exp, middle-coef-largest-01, middle-coef-largest, max_exp-fac-rec, max_exp-div-not, max_exp-div, countFun-shift, coef-sub-mult, coef-sub, coef-rec-add-01, coef-mult-rec, coef-le-2pot, coef-fac-divides-h,
• int-abs/sub-eq-01 is used by prime-pot-eq, prime-fac-divides-not, prime-fac-divides, max_exp-fac-smaller, max_exp-fac-same, max_exp-fac-rec, max_exp-fac-gen, coef-rec-add-01, coef-gcd, coef-fac-divides-h,
• int-abs/sub-le is used by coef-switch, coef-sub-mult, coef-rec-add-01, coef-pred-01, coef-mult-rec-lower, coef-mult-rec, coef-fac-divides,
• int-abs/sub-le-01 is used by prime-product, prime-divides-coef, middle-coef-largest, max_exp-fac-rec, max_exp-fac-gen, max_exp-fac-01, fac-add, countFun-shift, countFun-pot-01, countFun-pot, countFun-add, coef-switch, coef-sub-mult, coef-rec-add-01, coef-product-le, coef-pred-01, coef-mult-rec-lower, coef-mult-rec, coef-fac-divides, bertrand-small-primes, bertrand-estimate,
• int-abs/sub-ls is used by prime-fac-divides-not, middle-coef-largest-01, middle-coef-largest, middle-coef-larger-strongest, max_exp-fac-smaller, max_exp-fac-same, max_exp-fac-rec, max_exp-fac-01, countFun-shift, countFun-pot-01, countFun-pot, countFun-add, coef-rec-add-01, bertrand-small-primes,
• int-abs/sub-ls-01 is used by prime-pot-eq, prime-fac-divides-not, prime-fac-divides, middle-coef-max_exp-le, middle-coef-max_exp, middle-coef-larger-strongest, max_exp-fac-smaller, max_exp-fac-same, max_exp-fac-rec, max_exp-fac-gen, countFun-shift, countFun-pot-01, countFun-pot, countFun-add, coef-sub-mult, coef-rec-add-01, coef-mult-rec-lower, coef-fac-divides-h, coef-fac-divides,
• int-abs/sub-pred is used by prime-product, prime-pot-eq, prime-divides-pot-01, prime-divides-pot, max_exp-fac-gen, countFun-pot-01, countFun-pot, Binom-theorem-countFun, BertrandsPostulate,
• int-abs/sub-sub is used by prime-pot-eq, max_exp-fac-gen, countFun-shift, countFun-pot, coef-sub-mult, coef-rec-add-01, coef-mult-rec-lower, coef-mult-rec, coef-fac-divides-h, coef-fac-divides,
• int-abs/sub-sub-03 is used by coef-same, coef-rec-add-01, coef-fac-divides, Binom-theorem-countFun,
• int-abs/sub-sub-04 is used by countFun-shift, countFun-pot-01, coef-switch, coef-sub-mult, coef-pred-01, coef-mult-rec-lower, Binom-theorem-countFun,
• int-abs/sub-zero-01 is used by fac-divides, coef-zero, coef-rec-add-01, coef-mult-rec, coef-fac-divides-h, Binom-theorem-countFun,
• int-abs/succ-01 is used by prime-product, middle-coef-largest-01, fac-le, countFun-shift, countFun-add, coef-rec-add-01, coef-fac-divides, bertrand-small-primes,
• int-abs/succ-02 is used by product-pot-no-dups, prime-product, prime-fac-divides-not, prime-fac-divides, prime-divides-coef, middle-coef-max_exp, middle-coef-largest-01, max_exp-fac-smaller, max_exp-fac-same, max_exp-fac-rec, max_exp-fac-gen, max_exp-fac-01, fac-le, countFun-shift, countFun-pot-01, countFun-pot, countFun-add, coef-sub-mult, coef-rec-add-01, coef-mult-rec-lower, bertrand-small-primes,
• int-abs/zero-gels is used by middle-coef-max_exp,
• int-abs/zero-gels-01 is used by product-all-elems-le, middle-coef-largest-01, coef-nls-zero, coef-neg,
• int-abs/zero-gels-02 is used by est-4-big-02, est-4-big, bertrand-middle-primes,
• int-abs/zero-gels-03 is used by middle-coef-max_exp-big-primes,
• int-abs/zero-gels-04 is used by product-all-elems-le, prime-product, prime-divides-coef, middle-coef-max_exp-stronger, middle-coef-max_exp-le, middle-coef-max_exp-equality, middle-coef-max_exp-big-primes, middle-coef-max_exp, middle-coef-largest-01, middle-coef-largest, middle-coef-larger-strongest, middle-coef-larger, middle-coef-divides-not, max_exp-fac-rec, max_exp-fac-gen-stronger, max_exp-fac-gen, max_exp-fac-add, fac-le-one, fac-le, fac-divides, fac-add, est-4-big-02, est-4-big, coef-zero, coef-switch, coef-succ, coef-sub-mult, coef-same, coef-rec-add-01, coef-nls-zero, coef-mult-rec-lower, coef-mult-rec, coef-le-2pot, coef-eq-zero, bertrand-estimate, Binom-theorem-countFun,
• int-abs/zero-gs is used by prime-product,

Used from specification list-data

• list-data/intlista/elim-list is used by bertrand-middle-coef-smaller, BertrandsPostulate,
• list-data/intlista/elim-list-c is used by product-pot-no-dups,
• list-data/intlista/l is used by middle-coef-max_exp-le, middle-coef-max_exp, max_exp-fac-gen, bertrand-small-primes,
• list-data/intlista/size-01 is used by product-pot-no-dups, product-all-elems-le,

Used from specification list

• list/intlista/Nil is used by prime-product, bertrand-middle-primes, bertrand-middle-coef-smaller,
• list/intlista/a is used by product-pot-rec, product-pot-no-dups, product-all-elems-le, primes-divide, prime-product, middle-coef-max_exp-big-primes, middle-coef-larger-strongest, max_exp-primes-two, max_exp-fac-gen-stronger, max_exp-fac-gen, fac-add, divides-sum, countFun-shift, countFun-pot-01, countFun-pot, countFun-add, bertrand-small-primes, bertrand-prime-factors, bertrand-middle-primes, bertrand-middle-coef-smaller, Binom-theorem-countFun, BertrandsPostulate,
• list/intlista/app is used by countFun-add, BertrandsPostulate,
• list/intlista/app-01 is used by countFun-pot-01,
• list/intlista/app-02-ant is used by bertrand-middle-coef-smaller,
• list/intlista/c is used by product-pot-rec, product-pot-no-dups, product-all-elems-le, primes-divide, divides-sum, bertrand-middle-primes, bertrand-middle-coef-smaller, BertrandsPostulate,
• list/intlista/c-04 is used by countFun-add,
• list/intlista/c-06 is used by countFun-add,
• list/intlista/e is used by prime-product,
• list/intlista/e-01 is used by product-pot-no-dups, bertrand-middle-coef-smaller, BertrandsPostulate,
• list/intlista/in-01 is used by bertrand-middle-primes,
• list/intlista/in-08 is used by product-pot-no-dups, bertrand-middle-coef-smaller,
• list/intlista/in-11 is used by bertrand-small-primes, bertrand-middle-primes, bertrand-middle-coef-smaller,
• list/intlista/in-12 is used by bertrand-prime-factors,
• list/intlista/in-17 is used by product-pot-rec, product-pot-no-dups, product-all-elems-le, primes-divide, middle-coef-larger-strongest, divides-sum, bertrand-middle-primes, bertrand-middle-coef-smaller, BertrandsPostulate,
• list/intlista/in-append is used by product-pot-rec, product-pot-no-dups, product-all-elems-le, primes-divide, middle-coef-larger-strongest, divides-sum, bertrand-prime-factors, bertrand-middle-primes, bertrand-middle-coef-smaller, BertrandsPostulate,
• list/intlista/in-empty is used by bertrand-middle-coef-smaller, BertrandsPostulate,
• list/intlista/len is used by product-pot-no-dups, product-all-elems-le,
• list/intlista/len-02 is used by product-pot-no-dups, product-all-elems-le,
• list/intlista/neq is used by bertrand-middle-primes, bertrand-middle-coef-smaller, BertrandsPostulate,

Used from specification nat-basic2

• nat-basic2/a is used by product-pot-rec, product-pot-no-dups, product-all-elems-le, prime-product, prime-divides-pot-01, max_exp-primes-two, max_exp-fac-gen, fac-le, coef-fac-divides, bertrand-small-primes, Binom-theorem-countFun,
• nat-basic2/c is used by product-pot-rec, product-pot-no-dups, product-all-elems-le, prime-product, prime-divides-pot-01, max_exp-primes-two, max_exp-fac-gen, fac-le, coef-fac-divides, bertrand-small-primes, Binom-theorem-countFun,
• nat-basic2/l-02 is used by max_exp-primes-two, max_exp-fac-gen, bertrand-small-primes,
• nat-basic2/s is used by product-pot-no-dups, prime-divides-pot-01, fac-le, coef-fac-divides, Binom-theorem-countFun,

Used from specification list-dup

• list-dup/intlista/dups is used by bertrand-middle-primes,
• list-dup/intlista/c is used by prime-product,
• list-dup/intlista/dups-cons is used by primes-divide,
• list-dup/intlista/e-01 is used by prime-product,
• list-dup/intlista/rm-empty is used by bertrand-small-primes,
• list-dup/intlista/rm-in-02 is used by bertrand-small-primes,
• list-dup/intlista/rm-nodups is used by bertrand-small-primes,
• list-dup/intlista/rmdup-e is used by product-pot-no-dups,

Used from specification intnat

• intnat/num-i2n-le is used by prime-product,
• intnat/num-i2n-ls-02 is used by max_exp-fac-gen,
• intnat/abs-pred is used by prime-product, prime-pot-eq, prime-fac-divides-not, prime-fac-divides, max_exp-fac-smaller, max_exp-fac-rec, max_exp-fac-01, fac-pos-01, fac-not-neg, fac-add,
• intnat/abs-succ-03 is used by prime-product, prime-divides-pot-01,
• intnat/abs-zero is used by max_exp-fac-gen,
• intnat/i2i-pos is used by prime-product, middle-coef-max_exp-le, middle-coef-max_exp,
• intnat/ini2-abs is used by middle-coef-larger-strongest,
• intnat/labs is used by prime-divides-pot-01, middle-coef-largest-01, max_exp-not-div, max_exp-mult-01, max_exp-fac-gen, fac-le, countFun-shift, countFun-pot-01, countFun-pot, countFun-add, coef-fac-divides, Binom-theorem-countFun,
• intnat/le is used by product-pot-no-dups,
• intnat/ls-int-ls-nat is used by max_exp-fac-gen,
• intnat/n2i-add is used by product-pot-rec, product-pot-no-dups, product-all-elems-le, prime-product, max_exp-fac-gen, bertrand-small-primes,
• intnat/nat2int is used by product-pot-rec, product-pot-no-dups, product-all-elems-le, middle-coef-max_exp, max_exp-pos, max_exp-fac-gen,
• intnat/nat2int-02 is used by max_exp-zero-01, max_exp-zero, bertrand-big-primes,
• intnat/nat2int-04 is used by bertrand-small-primes,
• intnat/nat2int-05 is used by max_exp-rec,
• intnat/nat2int-06 is used by product-pot-no-dups,
• intnat/nat2int-07 is used by max_exp-fac-gen,
• intnat/nat2int-08 is used by max_exp-pos-04,
• intnat/num-i2n-le-02 is used by max_exp-fac-gen, coef-fac-divides,
• intnat/num-n2i-ls is used by max_exp-primes-two,
• intnat/num-n2i-ls-02 is used by middle-coef-max_exp-le, middle-coef-max_exp, max_exp-fac-gen, bertrand-small-primes,
• intnat/num-n2i-ls-03 is used by max_exp-fac-gen,
• intnat/num-n2i-ls-07 is used by max_exp-fac-gen,
• intnat/rax-01 is used by max_exp-fac-gen, coef-fac-divides,
• intnat/rax-04 is used by fac-le, Binom-theorem-countFun,

Used from specification list-perm

• list-perm/intlista/in-05 is used by bertrand-small-primes,
• list-perm/intlista/notin is used by product-pot-rec, max_exp-divides,
• list-perm/intlista/oc-e is used by product-pot-rec, max_exp-divides,
• list-perm/intlista/oc-zero is used by max_exp-zero-01, max_exp-zero, bertrand-big-primes,
• list-perm/intlista/ocappend is used by product-pot-rec, product-pot-no-dups, max_exp-primes-two, bertrand-small-primes,
• list-perm/intlista/ocs-del-length is used by product-pot-no-dups,
• list-perm/intlista/one is used by product-pot-rec, product-pot-no-dups, max_exp-same, max_exp-primes-two,
• list-perm/intlista/one-01 is used by product-pot-rec, product-pot-no-dups,
• list-perm/intlista/perm-dups-02 is used by prime-product,
• list-perm/intlista/perm-dups-03 is used by prime-product,

Used from specification oelem

• oelem/intlista/transitivity is used by est-4-big-02,
• oelem/intlista/irreflexivity is used by prime-product, prime-fac-divides-not, prime-divides-pot-01, middle-coef-max_exp, middle-coef-largest-01, middle-coef-largest, middle-coef-larger-strongest, max_exp-fac-smaller, max_exp-fac-gen, fac-le, coef-rec-add-01, coef-fac-divides, Binom-theorem-countFun,
• oelem/intlista/lel is used by primes-divide, prime-product, prime-pot-eq, prime-fac-divides-not, middle-coef-max_exp-le, middle-coef-max_exp-big-primes, middle-coef-max_exp, middle-coef-largest-01, middle-coef-larger-strongest, middle-coef-larger, max_exp-zero-02, max_exp-pos-03, max_exp-pos-02, max_exp-fac-smaller, max_exp-fac-gen-stronger, max_exp-fac-gen, max_exp-divides, fac-le-one, fac-le, est-4-big-02, countFun-shift, coef-rec-add-01, coef-product-le, coef-le-zero, coef-le-2pot, coef-fac-divides, bertrand-prime-factors, bertrand-middle-coef-smaller, bertrand-big-primes,
• oelem/intlista/transitivity is used by product-pot-no-dups, product-all-elems-le, primes-divide, prime-product, prime-fac-divides-not, prime-divides-coef, middle-coef-max_exp-equality, middle-coef-max_exp-big-primes, middle-coef-max_exp, middle-coef-largest-01, max_exp-zero, max_exp-fac-smaller, max_exp-fac-gen-stronger, max_exp-fac-gen, fac-not-neg, countFun-shift, coef-rec-add-01, bertrand-prime-factors, bertrand-middle-coef-smaller, BertrandsPostulate,

Used from specification int-basic2

• int-basic2/ls-03 is used by middle-coef-largest-01,
• int-basic2/add-a is used by product-pot-rec, product-pot-no-dups, product-all-elems-le, prime-product, prime-pot-eq, prime-fac-divides-not, prime-fac-divides, prime-divides-pot-01, prime-divides-pot, prime-divides-coef, middle-coef-not-one-01, middle-coef-max_exp-le, middle-coef-max_exp-equality, middle-coef-max_exp-big-primes, middle-coef-max_exp, middle-coef-largest-01, middle-coef-largest, middle-coef-larger-strongest, middle-coef-larger, max_exp-zero-02, max_exp-zero, max_exp-rec, max_exp-pos-03, max_exp-not-div, max_exp-mult-01, max_exp-fac-smaller, max_exp-fac-same, max_exp-fac-rec, max_exp-fac-gen-stronger, max_exp-fac-gen, max_exp-fac-add, max_exp-fac-01, max_exp-div-not, fac-le, fac-add, est-4-big-02, est-4-big-01, est-4-big, divides-sum, countFun-shift, countFun-pot-01, countFun-pot, countFun-add, coef-switch, coef-succ, coef-sub-mult, coef-sub, coef-rec-lower, coef-rec-add-02, coef-rec-add-01, coef-product-le, coef-pred-01, coef-mult-rec-lower, coef-mult-rec, coef-le-2pot, coef-fac-divides-h, coef-fac-divides, bertrand-small-primes, bertrand-middle-primes, bertrand-holds-lower, bertrand-estimate, Binom-theorem-countFun,
• int-basic2/add-c is used by product-pot-rec, product-pot-no-dups, product-all-elems-le, prime-product, prime-pot-eq, prime-fac-divides-not, prime-fac-divides, prime-divides-pot-01, prime-divides-pot, prime-divides-coef, middle-coef-not-one-01, middle-coef-max_exp-le, middle-coef-max_exp-equality, middle-coef-max_exp-big-primes, middle-coef-max_exp, middle-coef-largest-01, middle-coef-largest, middle-coef-larger-strongest, middle-coef-larger, max_exp-zero-02, max_exp-zero, max_exp-rec, max_exp-pos-03, max_exp-not-div, max_exp-mult-01, max_exp-fac-smaller, max_exp-fac-same, max_exp-fac-rec, max_exp-fac-gen-stronger, max_exp-fac-gen, max_exp-fac-add, max_exp-fac-01, max_exp-div-not, max_exp-div, fac-le, fac-add, est-4-big-02, est-4-big-01, est-4-big, divides-sum, countFun-shift, countFun-pot-01, countFun-pot, countFun-add, coef-switch, coef-succ, coef-sub-mult, coef-sub, coef-rec-lower, coef-rec-add-02, coef-rec-add-01, coef-product-le, coef-pred-01, coef-mult-rec-lower, coef-mult-rec, coef-le-2pot, coef-fac-divides-h, coef-fac-divides, bertrand-small-primes, bertrand-middle-primes, bertrand-holds-lower, bertrand-estimate, Binom-theorem-countFun,
• int-basic2/add-in is used by max_exp-not-div, max_exp-mult-01, max_exp-fac-rec, max_exp-fac-gen, countFun-shift, countFun-pot, coef-succ, coef-sub-mult, coef-rec-add-02, Binom-theorem-countFun,
• int-basic2/add-less is used by countFun-shift,
• int-basic2/add-zero is used by product-pot-rec, product-pot-no-dups, prime-fac-divides, middle-coef-max_exp-le, middle-coef-max_exp-equality, middle-coef-max_exp-big-primes, middle-coef-max_exp, middle-coef-largest-01, middle-coef-largest, max_exp-mult-01, max_exp-fac-smaller, max_exp-fac-rec, max_exp-fac-gen-stronger, max_exp-fac-gen, max_exp-fac-01, fac-add, est-4-big-02, est-4-big, countFun-shift, countFun-pot, coef-switch, coef-succ, coef-sub-mult, coef-rec-add-02, coef-rec-add-01, coef-mult-rec-lower, coef-fac-divides-h, Binom-theorem-countFun,
• int-basic2/eq is used by max_exp-mult-01, max_exp-fac-add, coef-le-2pot, Binom-theorem-countFun,
• int-basic2/ls is used by prime-product, middle-coef-largest-01, max_exp-fac-gen, max_exp-fac-add, fac-add,
• int-basic2/ls-01 is used by prime-product, max_exp-fac-gen, countFun-shift, bertrand-estimate,
• int-basic2/ls-02 is used by est-4-big-02, est-4-big, bertrand-estimate,
• int-basic2/lst-02 is used by countFun-shift,
• int-basic2/lst-03 is used by middle-coef-largest-01,
• int-basic2/num-between is used by middle-coef-max_exp-big-primes, est-4-big-01,
• int-basic2/pred is used by product-pot-rec, product-all-elems-le, coef-le-2pot, Binom-theorem-countFun,
• int-basic2/succ-01 is used by middle-coef-max_exp-big-primes,
• int-basic2/zero-02 is used by prime-divides-coef, max_exp-zero, max_exp-fac-01, countFun-pot-01, countFun-add, Binom-theorem-countFun,
• int-basic2/zero-04 is used by fac-le,

Used from specification nat-basic1

• nat-basic1/f is used by max_exp-primes-two, max_exp-fac-gen, bertrand-small-primes,
• nat-basic1/zero is used by middle-coef-max_exp-le, middle-coef-max_exp, max_exp-fac-gen, bertrand-small-primes,

Used from specification int-div

• int-div/div-add1-pospos is used by est-4-big, coef-rec-add-01, bertrand-estimate,
• int-div/div-lezero is used by max_exp-not-div, max_exp-mult-01,
• int-div/div-ls-modnotzero is used by middle-coef-larger-stronger, middle-coef-larger,
• int-div/div-mult is used by prime-divides-coef, middle-coef-divides-not, max_exp-divides, coef-mult-rec-lower,
• int-div/div-mult-nle-est is used by bertrand-estimate,
• int-div/div-mult-two-nls-01 is used by middle-coef-max_exp-le, middle-coef-max_exp,
• int-div/div-zero-03 is used by max_exp-fac-gen,
• int-div/div-zero-nls is used by middle-coef-largest-01, coef-nls-zero,
• int-div/mult is used by max_exp-fac-gen,
• int-div/mult-02 is used by max_exp-fac-gen,
• int-div/num-ls is used by middle-coef-max_exp-big-primes, est-4-big-02, est-4-big-01,
• int-div/div-elim is used by max_exp-fac-gen,
• int-div/div-elim-pospos is used by est-4-big-02, est-4-big, bertrand-estimate,
• int-div/div-eq-same-01 is used by middle-coef-max_exp-big-primes,
• int-div/div-ls-zero is used by est-4-big-02, est-4-big, bertrand-middle-primes,
• int-div/div-mult-01 is used by middle-coef-larger-stronger, coef-sub-mult, coef-sub, coef-rec-add-01, coef-mult-rec,
• int-div/div-mult-03 is used by primes-divide, max_exp-not-div, max_exp-mult-01, max_exp-div, est-4-big, coef-succ, coef-sub-mult, coef-sub, coef-rec-lower, coef-rec-add-01, coef-rec, coef-pred-01, coef-one,
• int-div/div-mult-nls-zero is used by bertrand-estimate,
• int-div/div-mult-num is used by middle-coef-max_exp-big-primes, middle-coef-larger-stronger, bertrand-estimate,
• int-div/div-mult-num-01 is used by middle-coef-max_exp-big-primes,
• int-div/div-same is used by coef-zero, coef-same, coef-rec-add-01,
• int-div/div-zero-03 is used by middle-coef-max_exp-big-primes,
• int-div/div-zero-05 is used by est-4-big,
• int-div/div-zero-06 is used by max_exp-not-div, max_exp-mult-01, max_exp-fac-gen-stronger,
• int-div/less-mult-div-01 is used by middle-coef-max_exp-big-primes, est-4-big-02, est-4-big-01, est-4-big, bertrand-middle-coef-smaller, bertrand-big-primes,
• int-div/lsfc-01 is used by middle-coef-max_exp-big-primes,
• int-div/mod-less-01 is used by coef-rec-add-01,
• int-div/mod-mult-02 is used by coef-rec-add-01,
• int-div/mod-mult-04 is used by est-4-big,
• int-div/mod-same is used by coef-rec-add-01,
• int-div/mod-zero is used by est-4-big-01,
• int-div/mod-zero-num is used by bertrand-estimate,
• int-div/neqf is used by coef-le-2pot,
• int-div/nls-mult-div is used by bertrand-estimate,
• int-div/nummult-le-01 is used by est-4-big-02, est-4-big, bertrand-middle-primes,
• int-div/nummult-le-02 is used by middle-coef-max_exp-big-primes, est-4-big-01, bertrand-holds-lower,
• int-div/nummult-ls is used by middle-coef-not-one-01, middle-coef-max_exp-big-primes, middle-coef-larger-strongest, est-4-big-01,
• int-div/nummult-ls-02 is used by prime-product, middle-coef-larger-strongest, est-4-big-02, bertrand-small-primes, BertrandsPostulate,
• int-div/nummult-modls is used by est-4-big-02,
• int-div/one is used by middle-coef-max_exp-big-primes, max_exp-fac-gen, max_exp-divides,
• int-div/pos is used by bertrand-estimate,
• int-div/zero is used by coef-rec-add-01,

Used from specification olist

• olist/intlista/ordered-ex-divide-lels is used by bertrand-prime-factors,
• olist/intlista/app-01 is used by bertrand-prime-factors,

Used from specification list-del

• list-del/intlista/del-e is used by product-pot-rec,
• list-del/intlista/del-length is used by product-pot-no-dups,
• list-del/intlista/del-n is used by product-pot-rec,
• list-del/intlista/del-rmdup-length-nle is used by product-pot-no-dups,
• list-del/intlista/del-y is used by product-pot-rec, product-pot-no-dups,
• list-del/intlista/in-03 is used by product-pot-rec,
• list-del/intlista/in-del-new is used by product-pot-no-dups,

Used from specification int-min

• int-min/odd-def is used by prime-product,
• int-min/odd-even-rew is used by prime-product,