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

Used simplifier rules/spec theorems by specification

Used from specification int-basic1

int-basic1/two-ls is used by all_prime_divisors-rec-02, all_prime_divisors-div,
int-basic1/forward-pos is used by range-dups, min-del-nlz, max-le-rec, euler-phi-prime, coprimes-prime, coprimes-max, all_prime_divisors-div,
int-basic1/ls-01 is used by sum-countfun-not-ls, sum-constant-countFun, range-dups, product-negative, min-rec, min-in-nls, min-del-nlz-01, max-le-rec, max-del1, filterFun-ordered, countFun-in, count-i2j-ordered, count-i2j-min, count-i2j-max,
int-basic1/lst-01 is used by sum-constant-countFun, max-perm, count-i2j-min, all_prime_divisors-div,
int-basic1/two-ls is used by euler-phi-prime, all_prime_divisors-product, all_prime_divisors-div,

Used from specification int-gcd

int-gcd/div-eq-one is used by all_prime_divisors-div,
int-gcd/div-mult is used by all_prime_divisors-div,
int-gcd/div-mult-shift is used by all_prime_divisors-product,
int-gcd/divides is used by all_prime_divisors-rec-01, all_prime_divisors-div,
int-gcd/divides-prime is used by all_prime_divisors-product-del, all_prime_divisors-in-01, all_prime_divisors-div,
int-gcd/gcd-com is used by coprimes-prime,
int-gcd/gcd-prime is used by coprimes-prime,
int-gcd/max_prime_divisor-def is used by all_prime_divisors-div,
int-gcd/max_prime_divisor-divides-03 is used by all_prime_divisors-div,
int-gcd/prime-divides is used by product-prime-divides, all_prime_divisors-div,
int-gcd/prime-ex-max is used by all_prime_divisors-div,
int-gcd/prime-not-odd is used by primes-max-even,
int-gcd/div-mult is used by all_prime_divisors-rec-02, all_prime_divisors-div,
int-gcd/div-not-ls is used by all_prime_divisors-in, all_prime_divisors-div,
int-gcd/div-zero is used by all_prime_divisors-in-01,
int-gcd/div-zero-01 is used by all_prime_divisors-div,
int-gcd/div-zero-zero is used by all_prime_divisors-div,
int-gcd/divides-mult-01 is used by all_prime_divisors-div,
int-gcd/gcd-com is used by coprimes-prime, coprimes-one, coprimes-max,
int-gcd/gcd-one-01 is used by coprimes-prime, coprimes-one, coprimes-min, coprimes-max,
int-gcd/gcd-same-01 is used by coprimes-prime, coprimes-max,
int-gcd/gcd-zero-04 is used by coprimes-max,
int-gcd/max_prime_divisor-abs is used by all_prime_divisors-in-01,
int-gcd/max_prime_divisor-abs-01 is used by all_prime_divisors-product, all_prime_divisors-ordered, all_prime_divisors-in-01, all_prime_divisors-div,
int-gcd/max_prime_divisor-divides is used by all_prime_divisors-product, all_prime_divisors-in-01, all_prime_divisors-div,
int-gcd/max_prime_divisor-divides-01 is used by all_prime_divisors-product,
int-gcd/max_prime_divisor-divides-02 is used by all_prime_divisors-in-01,
int-gcd/max_prime_divisor-divides-03 is used by all_prime_divisors-in-01, all_prime_divisors-div,
int-gcd/max_prime_divisor-ge2 is used by all_prime_divisors-in-01, all_prime_divisors-div,
int-gcd/max_prime_divisor-nle-01 is used by all_prime_divisors-product, all_prime_divisors-ordered, all_prime_divisors-in-01, all_prime_divisors-div,
int-gcd/max_prime_divisor-nle-zero-01 is used by all_prime_divisors-product, all_prime_divisors-div,
int-gcd/max_prime_divisor-nls-02 is used by all_prime_divisors-ordered,
int-gcd/max_prime_divisor-nls-03 is used by all_prime_divisors-ordered,
int-gcd/max_prime_divisor-not-zero is used by all_prime_divisors-product, all_prime_divisors-ordered, all_prime_divisors-in-01, all_prime_divisors-div,
int-gcd/max_prime_divisor-prime is used by all_prime_divisors-in-01, all_prime_divisors-div,
int-gcd/prime-abs is used by all_prime_divisors-product-del, all_prime_divisors-in-01, all_prime_divisors-div,
int-gcd/prime-divides-one is used by product-prime-divides, all_prime_divisors-div,
int-gcd/prime-le-2 is used by primes-le-2,
int-gcd/prime-not-four is used by primes-max-even,
int-gcd/prime-not-neg is used by primes-not-neg, all_prime_divisors-rec-01,
int-gcd/prime-not-neg-01 is used by coprimes-prime, all_prime_divisors-rec-02, all_prime_divisors-rec-01, all_prime_divisors-div,
int-gcd/prime-one is used by euler-phi-prime, coprimes-prime, all_prime_divisors-rec-02, all_prime_divisors-product-del, all_prime_divisors-in-01, all_prime_divisors-div,
int-gcd/prime-small is used by all_prime_divisors-div,
int-gcd/prime-two-01 is used by primes-max-even, primes-le-2,

Used from specification int-mult

int-mult/dist-lsplit is used by sum-all-elems-le,
int-mult/numsucc is used by sum-constant-countFun,
int-mult/zero-le is used by product-positive,
int-mult/zero-ls is used by product-negative,
int-mult/Mult-zero is used by sum-all-elems-le, countFun-mult, all_prime_divisors-rec-02, all_prime_divisors-div,
int-mult/add-mult-two is used by euler-phi-prime,
int-mult/associativity is used by sum-constant-countFun, sum-all-elems-le, product-zero, product-positive, product-perm-equal, product-one, product-negative, product-divide, product-del1-02, product-del1, product-app, euler-phi-prime, countFun-mult, all_prime_divisors-rec-02, all_prime_divisors-rec-01, all_prime_divisors-product, all_prime_divisors-div,
int-mult/commutativity is used by sum-constant-countFun, sum-all-elems-le, product-zero, product-positive, product-perm-equal, product-one, product-negative, product-last, product-divide, product-del1-02, product-del1, product-app, euler-phi-prime, countFun-mult, all_prime_divisors-rec-02, all_prime_divisors-rec-01, all_prime_divisors-product, all_prime_divisors-div,
int-mult/eq-dist is used by countFun-mult,
int-mult/eq-nonzero is used by product-del1-02, product-app,
int-mult/eq-one is used by all_prime_divisors-rec-02,
int-mult/eq-pos is used by all_prime_divisors-div,
int-mult/le-same is used by all_prime_divisors-div,
int-mult/ls-pos is used by all_prime_divisors-div,
int-mult/ls-same is used by all_prime_divisors-div,
int-mult/ls-same-01 is used by all_prime_divisors-div,
int-mult/neq-not-zero is used by product-del1-02, product-app,
int-mult/one is used by sum-constant-countFun, sum-all-elems-le, product-one, product-del1-02, product-app,
int-mult/one-01 is used by euler-phi-prime, all_prime_divisors-rec-02, all_prime_divisors-div,
int-mult/zero-eq is used by product-zero, all_prime_divisors-div,
int-mult/zero-ge is used by all_prime_divisors-div,
int-mult/zero-gr is used by all_prime_divisors-rec-02, all_prime_divisors-div,
int-mult/zero-gr-03 is used by all_prime_divisors-rec-01,
int-mult/zero-le-03 is used by product-positive,
int-mult/zero-ls-03 is used by product-negative,
int-mult/zero-neq-01 is used by all_prime_divisors-div,

Used from specification nat

nat/elim-pred-c is used by sum-constant-countFun, range-dups, map-at, countFun-at,
nat/elim-sub is used by sum-constant-countFun, countFun-at,
nat/eq is used by countFun-at,
nat/eq-02 is used by sum-constant-countFun, all_prime_divisors-rec-02,
nat/eqle-one is used by sum-constant-countFun,
nat/le-add is used by nodups-interval-size,
nat/lels is used by sum-constant-countFun, nodups-interval-size, map-at, countFun-at,
nat/lels-01 is used by sum-constant-countFun, nodups-interval-size, all_prime_divisors-rec-02,
nat/lep is used by sum-constant-countFun,
nat/ler is used by nodups-interval-size, countFun-at,
nat/lez is used by sum-constant-countFun, sum-all-indices-le, countFun-at,
nat/ls is used by sum-constant-countFun, countFun-at,
nat/ls-01 is used by nodups-interval-size, countFun-length,
nat/ls-02 is used by nodups-interval-size,
nat/not-zero is used by sum-constant-countFun, countFun-at,
nat/pred-03 is used by sum-constant-countFun, range-dups, nodups-interval-size, map-at, countFun-at, all_prime_divisors-rec-02,
nat/sub-base is used by countFun-at,
nat/sub-ls is used by countFun-length,
nat/succ-01 is used by sum-constant-countFun, map-at, countFun-length,

Used from specification int-abs

int-abs/Abs-pos is used by euler-phi-prime, countFun-at, count-i2j-length,
int-abs/sub-le-01 is used by countFun-at,
int-abs/Sub-def is used by sum-constant-countFun, euler-phi-prime, countFun-at, count-rec, count-i2j-min, count-i2j-max,
int-abs/abs-03 is used by countFun-at, count-i2j-no-dups, count-i2j-length, count-i2j-in,
int-abs/abs-08 is used by euler-phi-prime,
int-abs/abs-09 is used by countFun-at,
int-abs/abs-16 is used by sum-constant-countFun, countFun-at, all_prime_divisors-rec-02, all_prime_divisors-product, all_prime_divisors-ordered, all_prime_divisors-in-01, all_prime_divisors-div,
int-abs/abs-le-succ is used by sum-countFun-sub,
int-abs/absle is used by sum-constant-countFun, range-dups, countFun-length, countFun-last-01, countFun-at, count-rec, count-i2j-no-dups, count-i2j-in,
int-abs/absls-06 is used by count-i2j-no-dups, count-i2j-in,
int-abs/abssub is used by countFun-last-01, countFun-at, count-rec, count-i2j-length,
int-abs/abssub-01 is used by count-i2j-min, count-i2j-max,
int-abs/abssub-02 is used by count-i2j-min, count-i2j-max,
int-abs/anti is used by sum-countfun-not-ls, sum-countFun-sub, sum-constant-countFun, range-dups, nodups-interval-size, max-rec, countFun-mult, countFun-length, countFun-last, countFun-in, countFun-dist, countFun-at, count-i2j-min, count-i2j-max, count-i2j-length, count-i2j-in, coprimes-max,
int-abs/bet is used by sum-constant-countFun, coprimes-prime, all_prime_divisors-div,
int-abs/bet-01 is used by countFun-at, count-rec, count-i2j-ordered,
int-abs/elim-sub is used by sum-countFun-sub, countFun-mult, countFun-last-01, countFun-last, countFun-in, countFun-dist, count-rec, count-i2j-ordered, count-i2j-no-dups, count-i2j-in,
int-abs/forward-le is used by coprimes-max, all_prime_divisors-product-del, all_prime_divisors-ordered, all_prime_divisors-in-01, all_prime_divisors-in, all_prime_divisors-div,
int-abs/forward-le-01 is used by sum-not-ls-zero, sum-in-not-ls, sum-countfun-not-ls, sum-countFun-sub, sum-constant-countFun, range-dups, product-min-not-ls-zero, max-app-ls-01, max-app-ls, countFun-mult, countFun-length, countFun-last-01, countFun-last, countFun-in, countFun-dist, countFun-at, count-rec, count-i2j-ordered, count-i2j-no-dups, count-i2j-in, all_prime_divisors-product-del, all_prime_divisors-product, all_prime_divisors-ordered, all_prime_divisors-in-01, all_prime_divisors-in, all_prime_divisors-div,
int-abs/forward-le-02 is used by sum-positive, sum-not-ls-zero, sum-in-not-ls, sum-countfun-not-ls, sum-countFun-sub, sum-all-indices-le, product-negative, product-min-not-ls-zero, product-min-nlz, primes-product-not-neg, primes-not-neg, min-del-nlz-01, min-del-nlz, filterFun-max, countFun-mult, countFun-last, countFun-in, count-i2j-ordered, count-i2j-no-dups, count-i2j-in,
int-abs/forward-le-04 is used by product-positive, min-del-nlz-01, countFun-at, coprimes-min, coprimes-empty, all_prime_divisors-div,
int-abs/forward-le-05 is used by sum-countfun-not-ls, sum-constant-countFun, range-dups, product-positive, product-negative, product-min-nlz, min-del-nlz-01, min-del-nlz, max-le-rec, euler-phi-prime, countFun-in, countFun-at, count-i2j-ordered, coprimes-prime, coprimes-min, coprimes-max, all_prime_divisors-rec-02, all_prime_divisors-rec-01, all_prime_divisors-product, all_prime_divisors-div,
int-abs/forward-lele is used by sum-countfun-not-ls, sum-countFun-sub, sum-constant-countFun, range-dups, min-rec, max-rec, max-le-rec, countFun-last-01, countFun-in-01, countFun-in, count-i2j-ordered, count-i2j-no-dups, count-i2j-length, count-i2j-in, coprimes-min, coprimes-max, all_prime_divisors-div,
int-abs/forward-lels is used by sum-countfun-not-ls, sum-constant-countFun, sum-all-elems-le, product-positive, nodups-interval-size, min-rec, min-del-nlz-01, max-perm, max-le-rec, max-del1, filterFun-min, filterFun-max, divide-list-at-value, countFun-last-01, count-i2j-min, count-i2j-max, coprimes-min, all_prime_divisors-in, all_prime_divisors-div,
int-abs/forward-lsle is used by sum-not-ls-zero, sum-in-not-ls, sum-countfun-not-ls, sum-countFun-sub, product-min-not-ls-zero, nodups-interval-size, min-rec, min-in-nle, max-le-rec, max-del1, filterFun-ordered, filterFun-min, filterFun-max, countFun-in, countFun-at, count-i2j-ordered, count-i2j-max, coprimes-max, all_prime_divisors-ordered, all_prime_divisors-div,
int-abs/int-simp-07 is used by sum-all-indices-le,
int-abs/le-add is used by countFun-last-01, countFun-last, countFun-dist, countFun-at, count-rec, count-i2j-in,
int-abs/le-add-03 is used by countFun-last-01, count-i2j-in,
int-abs/lels is used by sum-not-ls-zero, sum-in-not-ls, sum-countfun-not-ls, sum-countFun-sub, sum-constant-countFun, sum-all-elems-le, range-dups, product-positive, product-negative, nodups-interval-size, min-rec, min-del-nlz-01, max-perm, max-le-rec, max-del1, max-app-ls-01, max-app-ls, filterFun-ordered, filterFun-min, filterFun-max, euler-phi-prime, divide-list-at-value, countFun-mult, countFun-length, countFun-last-01, countFun-last, countFun-in, countFun-dist, countFun-at, count-rec, count-i2j-ordered, count-i2j-no-dups, count-i2j-min, count-i2j-max, count-i2j-length, count-i2j-in, count-i2j-empty-02, coprimes-prime, coprimes-min, coprimes-max, all_prime_divisors-rec-02, all_prime_divisors-rec-01, all_prime_divisors-product, all_prime_divisors-ordered, all_prime_divisors-in-01, all_prime_divisors-div,
int-abs/lels-01 is used by sum-positive, sum-not-ls-zero, sum-in-not-ls, sum-countfun-not-ls, sum-countFun-sub, sum-constant-countFun, sum-all-indices-le, sum-all-elems-le, range-dups, product-negative, product-min-not-ls-zero, product-min-nlz, primes-product-not-neg, nodups-interval-size, max-rec, max-le-rec, filterFun-min, filterFun-max, divide-list-at-value, countFun-one, countFun-mult, countFun-length, countFun-last, countFun-in, countFun-dist, countFun-base-02, countFun-base-01, countFun-at, count-rec, count-one, count-i2j-ordered, count-i2j-no-dups, count-i2j-min, count-i2j-max, count-i2j-in, count-i2j-empty-01, count-empty, coprimes-empty, all_prime_divisors-rec-02, all_prime_divisors-product, all_prime_divisors-ordered, all_prime_divisors-last, all_prime_divisors-in-01, all_prime_divisors-in, all_prime_divisors-div,
int-abs/lels-02 is used by sum-countfun-not-ls, sum-constant-countFun, range-dups, product-negative, nodups-interval-size, min-rec, max-rec, countFun-at, count-i2j-ordered, count-i2j-min, count-i2j-max, count-i2j-in, coprimes-min, all_prime_divisors-rec-01, all_prime_divisors-div,
int-abs/lels-03 is used by sum-positive, sum-not-ls-zero, sum-in-not-ls, sum-countfun-not-ls, sum-all-indices-le, sum-all-elems-le, range-dups, product-negative, nodups-interval-size, min-rec, min-in-not-ls, min-in-nle, max-is-max, divide-list-at-value, countFun-mult, countFun-in, count-i2j-ordered, count-i2j-no-dups, count-i2j-in, coprimes-min, coprimes-max, all_prime_divisors-rec-02, all_prime_divisors-div,
int-abs/lenls is used by sum-in-not-ls, sum-constant-countFun, sum-all-elems-le, product-positive, max-rec, max-perm, max-le-rec, max-last-not-max, max-app-ls-01, max-app-ls, filterFun-min, filterFun-max, divide-list-at-value, countFun-mult, countFun-length, countFun-last-01, countFun-last, countFun-in, countFun-dist, countFun-at, count-rec, count-i2j-in, coprimes-min, coprimes-empty,
int-abs/leone is used by sum-constant-countFun, range-dups, euler-phi-prime, countFun-dist, countFun-at, coprimes-prime, coprimes-min, coprimes-max,
int-abs/lep is used by countFun-mult, countFun-last-01, countFun-last, countFun-in, countFun-dist, count-rec, count-i2j-ordered, count-i2j-no-dups, count-i2j-length, count-i2j-in,
int-abs/lep-01 is used by countFun-last-01, countFun-at, count-rec, count-i2j-no-dups, count-i2j-min, count-i2j-length, count-i2j-in,
int-abs/ler is used by sum-countfun-not-ls, sum-constant-countFun, range-dups, nodups-interval-size, countFun-in, countFun-at, count-i2j-ordered, count-i2j-in, coprimes-max,
int-abs/les is used by range-dups, countFun-last-01,
int-abs/lsone is used by count-i2j-ordered, coprimes-min, coprimes-empty, all_prime_divisors-div,
int-abs/minus-add is used by count-i2j-no-dups, count-i2j-in,
int-abs/minus-sub is used by euler-phi-prime,
int-abs/mone-06 is used by sum-countFun-sub, range-dups,
int-abs/mone-08 is used by sum-countFun-sub, countFun-last, count-i2j-no-dups, count-i2j-in,
int-abs/numadd-01 is used by range-dups,
int-abs/numle-02 is used by sum-countFun-sub, countFun-length, countFun-last-01, countFun-last, countFun-dist, count-i2j-no-dups, count-i2j-in,
int-abs/numleledel is used by countFun-at,
int-abs/numleledel-01 is used by sum-countFun-sub, countFun-length, countFun-last-01, countFun-last, countFun-dist, all_prime_divisors-in-01, all_prime_divisors-div,
int-abs/numls-02 is used by range-dups,
int-abs/numlsledel is used by all_prime_divisors-div,
int-abs/numlsledel-01 is used by all_prime_divisors-div,
int-abs/numsub is used by sum-countFun-sub, countFun-last-01, count-rec,
int-abs/one-03 is used by countFun-last-01,
int-abs/sub-add is used by sum-constant-countFun, countFun-length, countFun-at,
int-abs/sub-add-01 is used by sum-countFun-sub, sum-constant-countFun, nodups-interval-size, euler-phi-prime, count-i2j-length,
int-abs/sub-add-05 is used by countFun-mult, countFun-last, countFun-in, countFun-dist, count-i2j-ordered, count-i2j-length,
int-abs/sub-add-06 is used by countFun-length, countFun-last-01,
int-abs/sub-eq is used by sum-countFun-sub, euler-phi-prime, count-rec,
int-abs/sub-eq-01 is used by countFun-length, count-i2j-length,
int-abs/sub-le-01 is used by sum-countfun-not-ls, sum-constant-countFun, range-dups, nodups-interval-size, countFun-at, count-i2j-length, coprimes-prime,
int-abs/sub-ls is used by range-dups, nodups-interval-size, euler-phi-prime, countFun-last-01, countFun-base-02, countFun-at, count-rec, count-i2j-min, count-i2j-max, count-i2j-length, count-empty,
int-abs/sub-ls-01 is used by range-dups, euler-phi-prime, countFun-length, count-i2j-length,
int-abs/sub-sub is used by nodups-interval-size, euler-phi-prime, countFun-length, count-i2j-length,
int-abs/succ-01 is used by sum-countfun-not-ls, sum-constant-countFun, range-dups, nodups-interval-size, countFun-length, countFun-in, countFun-at, count-i2j-ordered, count-i2j-no-dups, count-i2j-min, count-i2j-max, count-i2j-length, count-i2j-in, coprimes-prime,
int-abs/succ-02 is used by range-dups, nodups-interval-size, countFun-length, countFun-base-02, countFun-base-01, countFun-at, count-rec, count-i2j-ordered, count-i2j-min, count-i2j-max, count-i2j-length, count-i2j-in, count-i2j-empty-01, count-empty,
int-abs/zero-gels-01 is used by sum-not-ls-zero, sum-in-not-ls, sum-countfun-not-ls, product-negative, product-min-not-ls-zero, max-perm, max-del1-01, max-app-ls-01, max-app-ls, count-i2j-ordered, count-i2j-no-dups, count-i2j-in,
int-abs/zero-gels-04 is used by sum-countfun-not-ls, sum-countFun-sub, sum-constant-countFun, range-dups, product-positive, countFun-mult, countFun-last, countFun-in, countFun-dist, countFun-at, count-rec, all_prime_divisors-div,
int-abs/zero-gs is used by countFun-last,

Used from specification list-last

list-last/intlista/l is used by all_prime_divisors-ordered,
list-last/intlista/last-def is used by all_prime_divisors-last,
list-last/intlista/lin-01 is used by all_prime_divisors-ordered,

Used from specification list-data

list-data/intlista/le-one is used by nodups-interval-size,
list-data/intlista/elim-list-c is used by sum-rec-01, sum-equal, sum-all-indices-le, filterFun-ordered, count-i2j-ordered,
list-data/intlista/l is used by sum-equal, sum-all-indices-le, range-dups, nodups-interval-size, map-at, countFun-length, countFun-at, count-i2j-length,
list-data/intlista/size-01 is used by sum-equal, sum-all-indices-le, sum-all-elems-le, map-length, countFun-length, countFun-at,

Used from specification int-min

int-min/Max-left is used by max-perm, max-le-rec, max-del1-01, max-del1, filterFun-max, divide-list-at-value, count-i2j-max,
int-min/Min-left is used by filterFun-min,
int-min/Min-right is used by min-rec, min-del-nlz-01, min-del-nlz, filterFun-min, divide-list-at-value, count-i2j-min,
int-min/odd-even-rew is used by primes-max-even,
int-min/Max-right is used by max-rec, max-perm, max-le-rec, max-last-max, max-del1-01, max-del1, filterFun-max, divide-list-at-value, count-i2j-max,
int-min/Min-left is used by min-rec, min-del-nlz-01, min-del-nlz, filterFun-min, divide-list-at-value, count-i2j-min,
int-min/Min-right is used by filterFun-min,
int-min/even-2 is used by primes-max-even,
int-min/max is used by max-rec, max-last-not-max, max-del1,
int-min/max-01 is used by max-del1-01, max-app-ls-01, max-app-ls, filterFun-max,
int-min/max-a is used by max-rec, max-perm, max-le-rec, max-last-not-max, max-last-max, max-del1-01, max-del1, max-app-ls-01, max-app-ls, max-app, filterFun-max, divide-list-at-value, count-i2j-max,
int-min/max-c is used by max-rec, max-perm, max-le-rec, max-last-not-max, max-last-max, max-del1-01, max-del1, max-app-ls-01, max-app-ls, max-app, filterFun-max, divide-list-at-value, count-i2j-max,
int-min/min-03 is used by min-in-nls, min-in-nle, min-del-nlz-01, filterFun-min,
int-min/min-a is used by min-rec, min-in-nls, min-in-nle, min-del-nlz-01, min-del-nlz, filterFun-min, divide-list-at-value, count-i2j-min,
int-min/min-c is used by min-rec, min-in-nls, min-in-nle, min-del-nlz-01, min-del-nlz, filterFun-min, divide-list-at-value, count-i2j-min,

Used from specification list

list/intlista/app-03 is used by all_prime_divisors-div,
list/intlista/in-17 is used by min-one, max-one,
list/intlista/in-rec is used by min-rec, max-rec,
list/intlista/some-element is used by coprimes-min,
list/intlista/Last is used by count-rec, count-one, count-i2j-no-dups, count-i2j-in, count-i2j-empty-02, coprimes-prime,
list/intlista/Nil is used by sum-app, product-app, max-app-ls-01, max-app-ls, max-app, filterFun-append, divide-list-at-value, countFun-last-01, countFun-last, count-rec, count-one, coprimes-prime, all_prime_divisors-ordered, all_prime_divisors-div,
list/intlista/a is used by sum-rec-01, sum-one, sum-not-ls-zero, sum-in-not-ls, sum-equal, sum-countfun-not-ls, sum-countFun-sub, sum-constant-countFun, sum-app, sum-all-indices-le, sum-all-elems-le, product-zero, product-prime-divides, product-positive, product-perm-equal, product-one, product-negative, product-mult, product-min-nlz, product-last, product-divide, product-del1-02, product-app, primes-rec, primes-perm-02, primes-perm-01, primes-le-2, min-rec, min-in-nls, min-in-nle, min-del-nlz-01, max-rec, max-perm-ls, max-perm, max-le-rec, max-del1-01, max-del1, max-app-ls-01, max-app-ls, max-app, map-length, map-in, map-at, filterFun-ordered, filterFun-one, filterFun-not-in, filterFun-no-dups, filterFun-min, filterFun-max, filterFun-in, filterFun-append, filterFun-all, divide-list-at-value, countFun-one, countFun-mult, countFun-length, countFun-last-01, countFun-last, countFun-in, countFun-dist, countFun-at, count-rec, count-one, count-i2j-ordered, count-i2j-min, count-i2j-max, count-i2j-length, count-i2j-in, count-i2j-empty-02, coprimes-prime, all_prime_divisors-product, all_prime_divisors-ordered, all_prime_divisors-last, all_prime_divisors-in-01, all_prime_divisors-div,
list/intlista/app is used by sum-one, product-one, min-in-nls, min-in-nle, min-del-nlz-01, max-perm, max-le-rec, max-del1-01, max-del1, max-app-ls-01, max-app-ls, max-app, filterFun-ordered, filterFun-one, filterFun-min, filterFun-max, divide-list-at-value, countFun-one, count-i2j-ordered, count-i2j-min, count-i2j-max, coprimes-prime, all_prime_divisors-div,
list/intlista/app-01 is used by filterFun-append, filterFun-all, countFun-last-01, countFun-last,
list/intlista/app-02-ant is used by product-divide, max-app, filterFun-ordered, count-i2j-empty-02,
list/intlista/app-03 is used by count-rec,
list/intlista/app-04 is used by count-rec, all_prime_divisors-div,
list/intlista/c is used by sum-rec-01, sum-not-ls-zero, sum-in-not-ls, sum-equal, sum-app, sum-all-indices-le, sum-all-elems-le, product-zero, product-prime-divides, product-positive, product-perm-equal, product-negative, product-divide, product-del1-02, product-app, primes-rec, primes-le-2, min-rec, min-del-nlz-01, max-perm, max-del1-01, max-del1, max-app, map-length, map-in, map-at, filterFun-ordered, filterFun-not-in, filterFun-no-dups, filterFun-min, filterFun-max, filterFun-in, filterFun-append, filterFun-all, divide-list-at-value, count-i2j-ordered,
list/intlista/c-03 is used by primes-le-2, max-del1-01,
list/intlista/c-04 is used by countFun-one, countFun-last-01, countFun-last, count-one, coprimes-one, all_prime_divisors-div,
list/intlista/c-06 is used by filterFun-ordered,
list/intlista/c-07 is used by filterFun-ordered, count-i2j-ordered,
list/intlista/c-08 is used by filterFun-ordered, count-i2j-ordered,
list/intlista/e is used by nodups-interval-size, min-one, max-perm, max-one, max-last-not-max, max-last-max, max-del1-01, max-del1, filterFun-ordered, count-i2j-empty-02, coprimes-prime, all_prime_divisors-ordered, all_prime_divisors-div,
list/intlista/e-01 is used by sum-rec-01, sum-equal, sum-all-indices-le, primes-le-2, min-rec, max-rec, max-del1-01, max-app, map-at, filterFun-ordered, filterFun-min, filterFun-max, divide-list-at-value, count-i2j-ordered,
list/intlista/e-02 is used by countFun-last-01, all_prime_divisors-last,
list/intlista/in-01 is used by product-zero, filterFun-not-in,
list/intlista/in-06 is used by primes-le-2, filterFun-not-in,
list/intlista/in-08 is used by range-dups,
list/intlista/in-11 is used by primes-perm-01,
list/intlista/in-12 is used by primes-perm-02,
list/intlista/in-14 is used by filterFun-ordered, count-i2j-ordered,
list/intlista/in-17 is used by sum-not-ls-zero, sum-in-not-ls, sum-all-elems-le, product-prime-divides, product-positive, product-negative, product-del1-02, primes-rec, primes-one, min-rec, max-rec, max-perm, map-in, filterFun-ordered, filterFun-in, filterFun-all, countFun-in, count-i2j-in, all_prime_divisors-in-01,
list/intlista/in-append is used by sum-not-ls-zero, sum-in-not-ls, sum-all-elems-le, product-prime-divides, product-positive, product-negative, product-divide, product-del1-02, primes-rec, min-rec, max-rec, map-in, filterFun-ordered, filterFun-in, filterFun-all, countFun-in, count-i2j-in, all_prime_divisors-in-01,
list/intlista/in-empty is used by sum-in-not-ls, product-zero, product-prime-divides, product-del1-02, primes-rec, min-in-not-ls, min-in, max-perm, max-in-not-ls, max-in-01, map-in, filterFun-not-in, filterFun-in, countFun-in, count-i2j-in, coprimes-min, all_prime_divisors-in-01,
list/intlista/len is used by sum-equal, sum-all-indices-le, sum-all-elems-le, map-length, map-at, countFun-length, count-i2j-length,
list/intlista/len-02 is used by sum-equal, sum-all-indices-le, sum-all-elems-le, nodups-interval-size, map-length, map-at, countFun-length, count-i2j-length,
list/intlista/one-01 is used by max-del1-01,

Used from specification nat-basic2

nat-basic2/a is used by sum-equal, sum-constant-countFun, sum-all-indices-le, sum-all-elems-le, range-dups, nodups-interval-size, map-length, map-at, euler-phi-prime, countFun-length, countFun-at, count-i2j-length, all_prime_divisors-rec-02,
nat-basic2/add-base is used by countFun-at,
nat-basic2/c is used by sum-equal, sum-constant-countFun, sum-all-indices-le, sum-all-elems-le, range-dups, nodups-interval-size, map-length, map-at, euler-phi-prime, countFun-length, countFun-at, count-i2j-length, all_prime_divisors-rec-02,
nat-basic2/eq-01 is used by sum-equal, sum-all-indices-le, map-length, countFun-length, count-i2j-length,
nat-basic2/l is used by sum-constant-countFun,
nat-basic2/one is used by range-dups, all_prime_divisors-rec-02,
nat-basic2/oz is used by sum-equal, sum-constant-countFun, sum-all-indices-le, map-at,
nat-basic2/s is used by sum-equal, sum-all-indices-le, range-dups, nodups-interval-size, map-at, countFun-length,
nat-basic2/z-01 is used by countFun-at,

Used from specification list-dup

list-dup/intlista/l-03 is used by count-i2j-no-dups,
list-dup/intlista/dups-cons is used by primes-le-2, filterFun-no-dups,
list-dup/intlista/e-01 is used by filterFun-no-dups, count-i2j-no-dups,
list-dup/intlista/rec is used by filterFun-no-dups,

Used from specification intnat

intnat/Int2nat-pos is used by countFun-length, count-i2j-length,
intnat/abs-succ-02 is used by sum-constant-countFun, countFun-at,
intnat/n2i-sub is used by nodups-interval-size,
intnat/abs-pred is used by sum-countfun-not-ls, range-dups, countFun-mult, countFun-last, countFun-in, countFun-dist, count-i2j-ordered,
intnat/abs-zero is used by sum-constant-countFun, countFun-at,
intnat/ini2-abs is used by euler-phi-prime, countFun-at,
intnat/inni-ls is used by countFun-at,
intnat/labs is used by sum-countFun-sub, sum-constant-countFun, range-dups, countFun-length, countFun-last-01, count-rec, count-i2j-no-dups, count-i2j-min, count-i2j-max, count-i2j-length, count-i2j-in, all_prime_divisors-product, all_prime_divisors-ordered, all_prime_divisors-in-01, all_prime_divisors-div,
intnat/labs-01 is used by sum-constant-countFun, countFun-at,
intnat/le is used by countFun-at,
intnat/n2i-add is used by sum-all-elems-le, range-dups, euler-phi-prime,
intnat/n2n is used by countFun-at,
intnat/nat2int is used by range-dups,
intnat/nat2int-02 is used by countFun-at,
intnat/nat2int-04 is used by nodups-interval-size,
intnat/nat2int-10 is used by countFun-at,
intnat/num-i2n-le is used by sum-constant-countFun,
intnat/num-n2i-ls-02 is used by range-dups, nodups-interval-size, countFun-at,
intnat/rax-04 is used by range-dups, countFun-length,

Used from specification list-perm

list-perm/intlista/del-01 is used by product-perm-equal, product-divide, max-perm,
list-perm/intlista/del1 is used by all_prime_divisors-rec-02,
list-perm/intlista/in is used by primes-perm-02, primes-perm-01,
list-perm/intlista/nodups is used by product-equal-01,
list-perm/intlista/a is used by divide-list-at-value,
list-perm/intlista/c is used by divide-list-at-value,
list-perm/intlista/empty is used by max-perm,
list-perm/intlista/empty-01 is used by product-perm-equal, product-divide, max-perm, divide-list-at-value,
list-perm/intlista/in is used by primes-perm,
list-perm/intlista/in-05 is used by all_prime_divisors-rec-02,
list-perm/intlista/notin is used by all_prime_divisors-rec-02,
list-perm/intlista/oc-zero is used by all_prime_divisors-rec-02,
list-perm/intlista/one is used by all_prime_divisors-rec-02,

Used from specification int-basic2

int-basic2/add-a is used by sum-rec-01, sum-one, sum-not-ls-zero, sum-in-not-ls, sum-equal, sum-countfun-not-ls, sum-countFun-sub, sum-constant-countFun, sum-app, sum-all-indices-le, sum-all-elems-le, range-dups, nodups-interval-size, euler-phi-prime, countFun-one, countFun-mult, countFun-length, countFun-last-01, countFun-last, countFun-in, countFun-dist, countFun-base-02, countFun-base-01, countFun-at, count-rec, count-i2j-ordered, count-i2j-no-dups, count-i2j-min, count-i2j-max, count-i2j-length, count-i2j-in, count-i2j-empty-01, count-empty, coprimes-prime,
int-basic2/add-c is used by sum-rec-01, sum-one, sum-not-ls-zero, sum-in-not-ls, sum-equal, sum-countfun-not-ls, sum-countFun-sub, sum-constant-countFun, sum-app, sum-all-indices-le, sum-all-elems-le, range-dups, nodups-interval-size, euler-phi-prime, countFun-one, countFun-mult, countFun-length, countFun-last-01, countFun-last, countFun-in, countFun-dist, countFun-base-02, countFun-base-01, countFun-at, count-rec, count-i2j-ordered, count-i2j-no-dups, count-i2j-min, count-i2j-max, count-i2j-length, count-i2j-in, count-i2j-empty-01, count-empty, coprimes-prime,
int-basic2/add-in is used by sum-rec-01, sum-equal, sum-countFun-sub, sum-app, countFun-last-01, countFun-dist, count-rec, count-i2j-no-dups, count-i2j-in,
int-basic2/add-less is used by count-i2j-ordered,
int-basic2/add-zero is used by sum-one, sum-countFun-sub, sum-constant-countFun, sum-app, countFun-mult, countFun-length, countFun-last-01, countFun-last, countFun-in, countFun-dist, countFun-at, count-rec, count-i2j-ordered, count-i2j-length, count-i2j-in,
int-basic2/eq is used by countFun-at,
int-basic2/ls is used by sum-not-ls-zero, sum-in-not-ls, sum-countfun-not-ls, countFun-mult, countFun-last-01, countFun-last, countFun-in, countFun-dist, count-rec, count-i2j-ordered, count-i2j-no-dups, count-i2j-in,
int-basic2/ls-01 is used by sum-countfun-not-ls, sum-all-elems-le, range-dups, nodups-interval-size, count-rec, count-i2j-ordered,
int-basic2/ls-02 is used by nodups-interval-size, countFun-in, countFun-at,
int-basic2/lst-03 is used by range-dups,

Used from specification oelem

oelem/intlista/irreflexivity is used by sum-countfun-not-ls, sum-constant-countFun, range-dups, min-del-nlz-01, max-del1-01, max-del1, max-app-ls-01, max-app-ls, filterFun-min, filterFun-max, countFun-one, countFun-base-02, countFun-base-01, count-rec, count-one, count-i2j-ordered, count-i2j-min, count-i2j-max, count-i2j-empty-01, count-empty, all_prime_divisors-div,
oelem/intlista/lel is used by sum-countFun-sub, sum-constant-countFun, range-dups, min-rec, max-perm-ls, filterFun-ordered, euler-phi-prime, countFun-last-01, countFun-last, countFun-at, count-i2j-no-dups, count-i2j-min, count-i2j-in, coprimes-prime, coprimes-max, all_prime_divisors-div,
oelem/intlista/ls-le is used by product-negative,
oelem/intlista/transitivity is used by sum-countfun-not-ls, range-dups, product-negative, product-min-nlz, nodups-interval-size, min-rec, min-in-nls, min-del-nlz-01, min-del-nlz, max-rec, max-le-rec, max-del1, filterFun-min, count-i2j-max, all_prime_divisors-div,

Used from specification nat-basic1

nat-basic1/f is used by sum-equal, sum-constant-countFun, sum-all-indices-le, nodups-interval-size, map-at, countFun-at,
nat-basic1/lf-01 is used by sum-equal, sum-all-indices-le,
nat-basic1/neq-01 is used by countFun-at,
nat-basic1/one is used by range-dups, nodups-interval-size,
nat-basic1/one-01 is used by nodups-interval-size, all_prime_divisors-rec-02,
nat-basic1/ref-1 is used by nodups-interval-size,
nat-basic1/zero is used by range-dups, nodups-interval-size, countFun-at,
nat-basic1/zero-01 is used by sum-equal, sum-all-indices-le,

Used from specification int-div

int-div/div-lezero is used by all_prime_divisors-div,
int-div/div-mult is used by all_prime_divisors-div,
int-div/div-mult-03 is used by product-del1-01,
int-div/divmult is used by all_prime_divisors-product,
int-div/abs is used by all_prime_divisors-product, all_prime_divisors-ordered, all_prime_divisors-in-01, all_prime_divisors-div,
int-div/div-mult-03 is used by all_prime_divisors-rec-02, all_prime_divisors-rec-01, all_prime_divisors-product, all_prime_divisors-div,
int-div/div-same is used by all_prime_divisors-div,
int-div/div-zero-05 is used by all_prime_divisors-div,
int-div/one is used by all_prime_divisors-div,
int-div/zero-07 is used by all_prime_divisors-div,

Used from specification olist

olist/intlista/ole-last-01 is used by all_prime_divisors-ordered,
olist/intlista/ole-rec is used by filterFun-ordered, count-i2j-ordered,
olist/intlista/app-01 is used by filterFun-ordered,
olist/intlista/le-e is used by filterFun-ordered, count-i2j-ordered, all_prime_divisors-ordered,
olist/intlista/le-o is used by filterFun-ordered, count-i2j-ordered, all_prime_divisors-ordered,
olist/intlista/orderedle-ls is used by filterFun-ordered,

Used from specification list-del

list-del/intlista/app is used by all_prime_divisors-div,
list-del/intlista/app-01 is used by product-divide, all_prime_divisors-div,
list-del/intlista/del-n is used by min-del-nlz-01,
list-del/intlista/del-one-simp is used by min-del-nlz-01,
list-del/intlista/del1-empty is used by max-perm,
list-del/intlista/del1-in is used by nodups-interval-size,
list-del/intlista/del1-n is used by max-del1-01, max-del1,
list-del/intlista/get-butlast is used by countFun-at,
list-del/intlista/get-last is used by countFun-at,
list-del/intlista/get-numrec is used by map-at,
list-del/intlista/l is used by nodups-interval-size,
list-del/intlista/one-01-01 is used by all_prime_divisors-div,
list-del/intlista/app is used by product-divide, all_prime_divisors-div,
list-del/intlista/app-01 is used by all_prime_divisors-div,
list-del/intlista/del-e is used by min-del-nlz-01, min-del-nlz,
list-del/intlista/del-y is used by min-del-nlz-01,
list-del/intlista/del1-e is used by product-del1-02, max-perm, max-del1-01, max-del1, all_prime_divisors-div,
list-del/intlista/del1-empty is used by nodups-interval-size, max-del1-01, max-del1,
list-del/intlista/del1-in is used by range-dups,
list-del/intlista/del1-n is used by product-del1-02,
list-del/intlista/del1-y is used by product-del1-02, max-del1-01, max-del1,
list-del/intlista/dups is used by range-dups, nodups-interval-size,
list-del/intlista/dups-01 is used by range-dups, nodups-interval-size,
list-del/intlista/get-append-grt is used by countFun-at,
list-del/intlista/get-succ is used by sum-equal, sum-all-indices-le, map-at,
list-del/intlista/get-zero-01 is used by sum-equal, sum-all-indices-le, map-at,
list-del/intlista/in-01-01 is used by range-dups, nodups-interval-size,
list-del/intlista/in-02-01 is used by nodups-interval-size, all_prime_divisors-rec-02, all_prime_divisors-div,
list-del/intlista/in-del-new is used by all_prime_divisors-product-del,
list-del/intlista/l is used by range-dups,
list-del/intlista/one is used by min-del-nlz-01,
list-del/intlista/one-01 is used by max-perm, max-del1-01, all_prime_divisors-div,