Used simplifier rules/spec theorems by specification

Used from specification int-basic1

• int-basic1/l is used by gcd-rec-sub-01,
• int-basic1/ls-rec is used by prime-13, prime-43, prime-7, case-20, prime-11, prime-163, prime-23, prime-5, case-30, case-10, case-40,
• int-basic1/lsrec is used by prime-43, case-10,
• int-basic1/lst-01 is used by gcd-com, gcd-rec, gcd-abs-rew-02,
• int-basic1/two-ls is used by max_prime_divisor-ge2,
• int-basic1/forward-pos is used by gcd-div-gcd-pos, not-less-gcd, prime-13, max_prime_divisor-ge2, prime-def-mod, gcd-one-prime, prime-divides-01, gcdhex, prime-43, gcd-rec-sub, prime-7, prime-631, num-gcd-pos, case-20, prime-11, max_prime_divisor-nls-02, div-not-ls, prime-163, prime-23, gcd-mult-pos, square-neq-any-pos-02, prime-317, prime-mult-not, prime-5, gcd-mod-one, prime-83, max_prime_divisor-nls, gcd-mod-one-01, case-30, prime-three, div-mult-div, gcd-one, gcd-prime, prime-1259, prime-def-prime, gcd-rec-sub-02, case-10, gcd-primes, max_prime_divisor-nls-01, case-40,
• int-basic1/irref is used by max_prime_divisor-nls-02,
• int-basic1/ls-01 is used by gcd-div-gcd-pos, prime-def-mod, gcd-pos, gcdex-pos, gcdhex, gcdex, gcd-rec-sub-03, gcd-rec-sub, gcd-conq-one, num-gcd-pos, div-mod, gcd-mult-pos, square-neq-any-pos-02, gcd-divides-both-h, gcd-rec-sub-01, gcd-mod-one, gcd-com, gcd-rec, square-neq-any-pos, prime-def-prime, square-neq-prime, gcd-abs-rew-02, max_prime_divisor-nls-01,
• int-basic1/lst is used by gcd-rec-sub,
• int-basic1/lst-01 is used by gcdex-pos, gcd-mult-pos, gcd-rec-sub-01, gcd-one,
• int-basic1/numlslsdel is used by prime-631, prime-317, prime-1259,
• int-basic1/two-ls is used by prime-13, prime-def-mod, prime-43, prime-7, prime-631, prime-11, max_prime_divisor-nls-02, prime-odd-01, prime-163, prime-23, prime-317, prime-5, prime-83, prime-three, prime-1259, prime-def-prime,

Used from specification int-mult

• int-mult/commutativity is used by square-neq-any-pos-01, square-neq-pos, divides-prime, square-neq-any-pos-02,
• int-mult/dist-rsplit is used by gcd-conq-one, gcdex-not-unique,
• int-mult/dist-sub-split is used by gcdhex,
• int-mult/eq-nonzero is used by square-neq-pos-h, square-neq-any-pos-02,
• int-mult/eq-nonzero-01 is used by divides-abs-02,
• int-mult/le-one is used by square-neq-any-pos-02,
• int-mult/le-same-05 is used by square-neq-any-pos-02,
• int-mult/ls-same-01 is used by divides-prime, max_prime_divisor-nls-02,
• int-mult/mod-neq is used by gcd-div-rest,
• int-mult/mult-pos is used by max_prime_divisor-ge2,
• int-mult/square-le is used by prime-13, prime-43, prime-7, prime-631, prime-11, prime-163, prime-23, prime-317, prime-5, prime-83, prime-three, prime-1259,
• int-mult/Mult-zero is used by gcd-div-gcd-pos, gcd-mult, square-neq-any-pos-01, max_prime_divisor-ge2, prime-def-mod, gcdex-pos, gcd-mult-01, gcdhex, square-neq-pos, gcd-conq-one, square-neq-pos-h, max_prime_divisor-nls-02, gcd-mult-pos, square-neq-any-pos-02, exgcd-div, gcd-mod-one, gcd-mod-one-01, square-neq-any, max_prime_divisor-nls-03, square-neq-any-pos, divides-abs-02, div-zero-zero,
• int-mult/abs-eqall is used by gcd-mult, div-abs-02, gcd-mult-01, gcd-mult-pos, square-neq-any-pos-02, prime-def-prime,
• int-mult/add-mult-two is used by prime-not-odd, gcd-divides-both-h, gcd-rec-sub-01,
• int-mult/associativity is used by div-mult-01, div-mult-shift, gcd-div-gcd-pos, gcd-div-mult, gcd-mult, square-neq-any-pos-01, coprime-divides-01, divides-neg, prime-not-four, prime-13, div-abs-02, div-div, max_prime_divisor-ge2, prime-def-mod, divides-mone, div-one-one-neg, gcdex-pos, prime-not-odd, div-one-one, prime-divides-01, gcd-mult-01, gcdhex, square-neq-pos, divides-mult-01, max_prime_divisor-divides-02, prime-43, gcdex, prime-7, divides-prime, divides-mult-add, gcd-conq-one, divides-mult-02, prime-631, divides-add, square-neq-pos-h, prime-11, max_prime_divisor-nls-02, prime-odd-01, coprime-divides, div-not-ls, prime-163, prime-ex-max, prime-23, gcd-mult-pos, gcdex-not-unique, square-neq-any-pos-02, divides-mult, gcd-divides, div-same, div-abs, prime-odd, div-mod-01, divides-abs-01, prime-317, prime-mult-not, div-mod-zero, prime-5, max_prime_divisor-divides-03, exgcd-div, div-zero, gcd-div-eq, gcd-one-eq, gcd-max-prop, gcd-mod-one, div-abs-04, prime-83, gcd-mod-one-01, prime-three, square-neq-any, div-mult-div, div-abs-01, max_prime_divisor-nls-03, gcd-rec, gcd-mult-pos-01, square-neq-any-pos, prime-1259, prime-two, prime-def-prime, div-div-01, div-mod-zero-01, prime-divides, divides-abs-02, div-zero-zero, square-neq-prime, div-eq, div-neg, div-one, div-eq-one, gcd-conq-one-01,
• int-mult/commutativity is used by div-mult-01, div-mult-shift, gcd-div-gcd-pos, gcd-div-mult, gcd-mult, square-neq-any-pos-01, coprime-divides-01, divides-neg, prime-not-four, prime-13, div-abs-02, div-div, max_prime_divisor-ge2, prime-def-mod, divides-mone, div-one-one-neg, gcdex-pos, prime-not-odd, div-one-one, prime-divides-01, gcd-mult-01, gcdhex, square-neq-pos, divides-mult-01, max_prime_divisor-divides-02, prime-43, gcdex, prime-7, divides-prime, divides-mult-add, gcd-conq-one, divides-mult-02, prime-631, divides-add, square-neq-pos-h, prime-11, max_prime_divisor-nls-02, prime-odd-01, coprime-divides, div-not-ls, prime-163, prime-ex-max, prime-23, gcd-mult-pos, gcdex-not-unique, square-neq-any-pos-02, divides-mult, gcd-divides, div-same, div-abs, divides-mod, prime-odd, div-mod-01, divides-abs-01, prime-317, prime-mult-not, div-mod-zero, prime-5, max_prime_divisor-divides-03, exgcd-div, div-zero, coprime-divides-03, gcd-div-eq, gcd-one-eq, gcd-max-prop, gcd-mod-one, div-abs-04, prime-83, gcd-mod-one-01, prime-three, square-neq-any, gcd-div-rest, div-mult-div, div-abs-01, max_prime_divisor-nls-03, gcd-rec, gcd-mult-pos-01, square-neq-any-pos, prime-1259, prime-two, prime-def-prime, div-div-01, div-mod-zero-01, prime-divides, divides-abs-02, div-zero-zero, square-neq-prime, div-eq, div-neg, div-one, div-eq-one, gcd-conq-one-01,
• int-mult/dist-rmerge is used by coprime-divides-01, divides-add, div-mod-01,
• int-mult/eq-dist is used by divides-add, gcdex-not-unique, gcd-rec,
• int-mult/eq-nonzero is used by square-neq-pos-h, square-neq-any-pos-02, divides-mult, div-abs, divides-abs-01, gcd-rec, divides-abs-02,
• int-mult/eq-one is used by gcd-div-gcd-pos, div-div, div-one-one, gcd-conq-one, square-neq-pos-h, square-neq-any-pos-02, div-mult-div, div-div-01,
• int-mult/eq-one-neg is used by div-one-one-neg, gcd-mod-one,
• int-mult/eq-pos is used by gcd-mult-pos, div-mod-01, gcd-mult-pos-01,
• int-mult/eq-same is used by div-div, prime-not-odd, divides-prime, prime-odd, div-div-01,
• int-mult/eq-same-01 is used by div-div, div-div-01,
• int-mult/eq-same-02 is used by gcd-div-gcd-pos, div-mult-div,
• int-mult/le-neg is used by square-neq-any-pos-02,
• int-mult/le-one is used by max_prime_divisor-nls-02,
• int-mult/le-pos is used by prime-def-mod, gcd-mult-pos, div-mod-01, prime-def-prime,
• int-mult/le-same is used by gcd-div-gcd-pos, prime-def-mod, divides-prime, prime-ex-max, square-neq-any-pos-02, max_prime_divisor-nls-03, prime-def-prime,
• int-mult/le-same-02 is used by gcdex-pos, gcd-conq-one, square-neq-any-pos-02,
• int-mult/ls-forward is used by square-neq-any-pos-02,
• int-mult/ls-pos is used by square-neq-any-pos-02,
• int-mult/ls-same is used by div-not-ls, prime-def-prime,
• int-mult/ls-same-01 is used by prime-def-mod, max_prime_divisor-nls-02, square-neq-any-pos-02, prime-mult-not, prime-def-prime,
• int-mult/ls-same-03 is used by divides-prime,
• int-mult/minus-left is used by divides-neg, div-abs-02, gcdex-pos, gcdex, gcd-conq-one, div-abs, divides-abs-01, div-abs-04, div-abs-01, square-neq-any-pos, divides-abs-02, square-neq-prime, div-neg, gcd-conq-one-01,
• int-mult/minus-one-01 is used by divides-mone,
• int-mult/minus-one-02 is used by div-abs-04,
• int-mult/neq-not-zero is used by div-abs, divides-abs-01, gcd-rec, divides-abs-02,
• int-mult/one is used by square-neq-any-pos-01, max_prime_divisor-ge2, gcdhex, square-neq-pos, square-neq-pos-h, square-neq-any-pos-02, div-same, gcd-one-eq, div-one,
• int-mult/one-01 is used by gcd-div-gcd-pos, coprime-divides-01, prime-13, prime-43, prime-7, prime-631, prime-11, max_prime_divisor-nls-02, prime-odd-01, prime-163, prime-ex-max, prime-23, square-neq-any-pos-02, prime-317, prime-5, prime-83, prime-three, prime-1259, prime-def-prime, div-eq-one,
• int-mult/pred-rmerge is used by gcd-conq-one,
• int-mult/square-eq is used by square-neq-pos-h, square-neq-any-pos-02,
• int-mult/square-le is used by square-neq-any-pos-02,
• int-mult/square-lez is used by square-neq-any-pos-02, square-neq-any,
• int-mult/square-lez-01 is used by square-neq-any-pos-02, square-neq-any,
• int-mult/square-zero is used by square-neq-any-pos-02, square-neq-any, square-neq-any-pos,
• int-mult/succ-rmerge is used by gcdex-pos, divides-prime,
• int-mult/zero-eq is used by divides-prime, gcd-mult-pos, square-neq-any-pos-02, div-mod-zero, square-neq-any, square-neq-prime,
• int-mult/zero-ge is used by gcd-div-gcd-pos, prime-def-mod, divides-prime, max_prime_divisor-nls-02, gcd-mult-pos, div-mod-01, prime-mult-not, div-div-01,
• int-mult/zero-ge-01 is used by gcdex-pos, divides-prime, max_prime_divisor-nls-02,
• int-mult/zero-ge-add is used by div-mod-01,
• int-mult/zero-gr is used by prime-def-mod, divides-prime, max_prime_divisor-nls-02, div-not-ls, square-neq-any-pos-02, prime-mult-not, max_prime_divisor-nls-03, prime-def-prime,
• int-mult/zero-gr-01 is used by divides-prime, square-neq-any,
• int-mult/zero-gr-03 is used by divides-prime, max_prime_divisor-nls-02, square-neq-any-pos-02,
• int-mult/zero-le is used by gcd-mod-one,
• int-mult/zero-le-01 is used by div-div,
• int-mult/zero-left is used by div-zero,
• int-mult/zero-ls is used by gcd-mod-one, gcd-mod-one-01,
• int-mult/zero-neq-01 is used by gcd-div-gcd-pos, gcd-mult-pos, square-neq-any-pos-02, square-neq-any-pos,

Used from specification int-abs

• int-abs/Abs-neg is used by div-one-one-neg, gcd-rec-sub-01, gcd-one,
• int-abs/Abs-pos is used by div-abs-02, div-one-one, divides-prime, gcd-mult-pos, gcd-divides-both-h, div-abs-03, div-abs-04, div-abs-01, gcd-divides-both,
• int-abs/abs-12 is used by gcd-mult-pos,
• int-abs/absa is used by gcd-rec-sub-03,
• int-abs/forward-le is used by div-gcd-is-neg-01,
• int-abs/ge-def is used by gcd-rec-sub-03,
• int-abs/le-def is used by gcd-conq-one,
• int-abs/lels is used by gcd-rec-sub-01,
• int-abs/neg-10 is used by gcd-zero-05,
• int-abs/rew-eqzero is used by gcd-zero-05, gcd-divides-both,
• int-abs/sub-same is used by gcd-rec-sub-03,
• int-abs/Abs-pos is used by div-one-one-neg, gcdex, gcd-rec-sub-03, gcd-rec-sub-01, gcd-one,
• int-abs/Sub-def is used by gcdhex, div-mod, div-mod-01, divides-mult-sub,
• int-abs/abs is used by prime-13, gcd-one-prime, prime-43, divides-prime, prime-631, prime-11, prime-163, prime-23, prime-317, gcd-mod-one, prime-83, gcd-mod-one-01, prime-three, div-mult-div, prime-1259, prime-def-prime, gcd-primes,
• int-abs/abs-01 is used by gcd-mult-01, gcd-div-gcd, gcd-abs-rew, square-neq-any-pos-02, gcd-abs-rew-01, gcd-rec, gcd-neg, gcd-same-02,
• int-abs/abs-03 is used by gcd-mult, gcdex, gcd-mult-pos, gcd-rec, gcd-divides-both,
• int-abs/abs-06 is used by gcd-mult, abs-gcd-not-less, gcd-nls, gcd-div-gcd, gcd-mult-pos, gcd-rec, div-gcd-neg-not-zero, gcd-divides-both,
• int-abs/abs-07 is used by mod-gcd-01, gcd-mult-01, gcd-zero-zero, gcd-div-gcd, gcd-rec-sub-01, gcd-one-eq, gcd-rec, gcd-same, gcd-zero-04, gcd-abs-rew-02, gcd-same-02,
• int-abs/abs-08 is used by div-abs-02, gcdex-pos, div-one-one, gcdex, gcd-rec-sub-03, divides-prime, gcd-divides-both-h, gcd-rec-sub-01, div-abs, div-abs-03, divides-abs-01, div-abs-04, div-abs-01, div-gcd-neg-not-zero, divides-abs-02, gcd-divides-both,
• int-abs/abs-16 is used by gcd-div-gcd-pos, square-neq-any-pos-01, gcdhex, square-neq-pos, gcdex-smallest-pos, gcd-rec-sub-03, prime-7, divides-prime, gcd-mult-pos, square-neq-any-pos-02, gcd-divides-both-h, gcd-rec-sub-01, prime-5, gcd-same-01, max_prime_divisor-abs, gcd-rec-pos, gcd-mult-pos-01,
• int-abs/abs-18 is used by prime-abs, gcd-rec-sub-03, gcd-abs, gcd-rec-sub-01, div-abs, divides-abs-01, divides-abs-02, max_prime_divisor-abs-01,
• int-abs/abs-neg is used by div-one-one-neg, gcd-rec-sub-01, gcd-neg,
• int-abs/abseq is used by gcd-rec-sub-03, gcd-rec-sub-01,
• int-abs/absle is used by gcd-div-gcd-pos, div-div, gcdhex, square-neq-pos, gcdex-smallest-pos, gcd-rec-sub-03, gcd-conq-one, square-neq-pos-h, gcd-mult-pos, gcd-rec-pos, div-div-01,
• int-abs/absls is used by gcd-divides-both,
• int-abs/abssub-02 is used by prime-ex-max,
• int-abs/anti is used by gcd-rec-sub-03, prime-ex-max, gcd-divides-both-h, gcd-mod-one, gcd-mod-one-01, square-neq-any-pos, prime-def-prime, gcd-divides-both,
• int-abs/bet is used by gcd-div-gcd-pos, prime-def-mod, divides-prime, prime-ex-max, square-neq-any-pos-02, gcd-one, prime-two, prime-def-prime,
• int-abs/elim-sub is used by gcdex-pos, gcd-rec-sub-03, gcd-rec-sub, divides-add, prime-odd-01, gcdex-not-unique, gcd-divides-both-h, gcd-rec-sub-01, divides-minus, gcd-rec-sub-02,
• int-abs/forward-le is used by prime-13, max_prime_divisor-ge2, prime-def-mod, max_prime_divisor-divides-02, prime-43, prime-7, divides-prime, prime-631, prime-11, max_prime_divisor-nls-02, prime-163, prime-ex-max, prime-23, gcd-mult-pos, gcd-divides-both-h, prime-317, max_prime_divisor-nle-zero, prime-mult-not, prime-5, max_prime_divisor-divides-03, prime-one, max_prime_divisor-not-zero, max_prime_divisor-abs, prime-83, max_prime_divisor-nls, prime-not-neg-01, prime-three, max_prime_divisor-prime, max_prime_divisor-nls-03, max_prime_divisor-divides-01, prime-1259, max_prime_divisor-nle-zero-01, prime-def-prime, max_prime_divisor-nls-zero, max_prime_divisor-divides, max_prime_divisor-nls-01, max_prime_divisor-nle-01, max_prime_divisor-nle,
• int-abs/forward-le-01 is used by gcd-div-gcd-pos, prime-13, div-abs-02, div-div, max_prime_divisor-ge2, prime-def-mod, div-one-one-neg, gcdhex, square-neq-pos, max_prime_divisor-divides-02, prime-43, gcdex-smallest-pos, gcd-rec-sub-03, gcd-rec-sub, prime-7, divides-prime, gcd-conq-one, prime-631, square-neq-pos-h, prime-11, max_prime_divisor-nls-02, prime-odd-01, prime-163, prime-ex-max, div-gcd-is-neg-01-01, prime-23, gcd-mult-pos, square-neq-any-pos-02, gcd-divides-both-h, div-mod-01, prime-317, max_prime_divisor-nle-zero, prime-mult-not, prime-5, max_prime_divisor-divides-03, prime-one, gcd-one-eq, max_prime_divisor-not-zero, gcd-mod-one, max_prime_divisor-abs, prime-83, max_prime_divisor-nls, prime-not-neg-01, prime-three, max_prime_divisor-prime, gcd-negone-eq, max_prime_divisor-nls-03, gcd-rec, gcd-one, gcd-prime, square-neq-any-pos, max_prime_divisor-divides-01, prime-1259, max_prime_divisor-nle-zero-01, prime-def-prime, div-div-01, max_prime_divisor-nls-zero, max_prime_divisor-divides, div-gcd-not-neg, max_prime_divisor-nls-01, max_prime_divisor-nle-01, max_prime_divisor-nle,
• int-abs/forward-le-02 is used by div-abs-02, div-div, gcd-zero-02, gcd-pos, div-one-one-neg, gcdex-pos, gcd-rec-sub-03, prime-not-neg, divides-prime, gcd-conq-one, div-gcd-is-neg-01-01, div-gcd-is-neg, gcd-divides-both-h, gcd-rec-sub-01, div-abs, divides-abs-01, gcd-nls-zero, gcd-one-eq, gcd-mod-one, div-abs-04, square-neq-any, div-abs-01, gcd-one, div-gcd-neg-not-zero, square-neq-any-pos, divides-abs-02, max_prime_divisor-nls-zero, div-gcd-is-neg-01, square-neq-prime, gcd-divides-both,
• int-abs/forward-le-04 is used by div-div, max_prime_divisor-ge2, gcd-rec-sub-03, square-neq-any-pos-02, gcd-rec-sub-01, max_prime_divisor-nle-zero, gcd-nls-zero, gcd-mod-one-01, prime-not-neg-01, square-neq-any, square-neq-any-pos, max_prime_divisor-nle-zero-01, square-neq-prime, div-gcd-not-neg,
• int-abs/forward-le-05 is used by gcd-div-gcd-pos, not-less-gcd, gcd-zero-05, square-neq-any-pos-01, prime-13, prime-def-mod, gcd-one-prime, gcdex-pos, prime-divides-01, gcdhex, square-neq-pos, prime-43, gcdex-smallest-pos, gcd-rec-sub-03, gcd-rec-sub, prime-7, divides-prime, gcd-conq-one, div-one-neg-pos, prime-631, num-gcd-pos, square-neq-pos-h, case-20, prime-11, max_prime_divisor-nls-02, prime-odd-01, div-not-ls, prime-163, prime-23, gcd-mult-pos, square-neq-any-pos-02, div-gcd-is-neg, gcd-divides-both-h, gcd-rec-sub-01, prime-odd, div-mod-01, prime-317, prime-mult-not, div-one-pos, prime-5, gcd-nls-zero, gcd-one-eq, gcd-mod-one, prime-83, max_prime_divisor-nls, gcd-mod-one-01, case-30, prime-three, div-mult-div, gcd-rec, gcd-one, gcd-prime, square-neq-any-pos, gcd-less-eq-zero, prime-1259, prime-two, prime-def-prime, div-div-01, gcd-rec-sub-02, case-10, div-gcd-is-neg-01, gcd-primes, square-neq-prime, div-gcd-not-neg, gcd-add, max_prime_divisor-nls-01, case-40, max_prime_divisor-nle-01,
• int-abs/forward-lele is used by prime-13, max_prime_divisor-ge2, prime-def-mod, prime-43, prime-7, divides-prime, prime-631, prime-11, prime-163, prime-ex-max, prime-23, gcd-mult-pos, prime-317, max_prime_divisor-nle-zero, prime-5, prime-one, prime-83, prime-not-neg-01, prime-three, max_prime_divisor-nls-03, gcd-prime, prime-1259, max_prime_divisor-nle-zero-01, prime-def-prime, div-gcd-not-neg, max_prime_divisor-nle-01, max_prime_divisor-nle,
• int-abs/forward-lels is used by gcd-rec-sub-03, square-neq-any-pos-02, max_prime_divisor-nle-zero, gcd-nls-zero, max_prime_divisor-nls, gcd-mod-one-01, square-neq-any-pos, max_prime_divisor-nle-zero-01, prime-def-prime, div-gcd-not-neg, max_prime_divisor-nls-01,
• int-abs/forward-lsle is used by div-div, max_prime_divisor-ge2, gcdhex, gcd-rec-sub-03, gcd-conq-one, max_prime_divisor-nls-02, div-gcd-is-neg-01-01, gcd-mult-pos, gcd-divides-both-h, gcd-one-eq, gcd-mod-one, max_prime_divisor-nls-03, gcd-prime, prime-def-prime, max_prime_divisor-nls-zero, max_prime_divisor-nle-01, max_prime_divisor-nle,
• int-abs/ge-def is used by gcd-rec-sub-03, gcd-one-eq,
• int-abs/gr-def is used by gcd-div-gcd-pos, gcd-one-prime, gcd-one, gcd-prime, gcd-one-01, gcd-primes,
• int-abs/le-add is used by gcd-conq-one, gcd-mult-pos, div-mod-01,
• int-abs/le-def is used by gcd-div-gcd-pos, prime-abs, prime-13, max_prime_divisor-ge2, prime-def-mod, gcd-pos, gcdex-pos, gcdhex, square-neq-pos, prime-43, gcdex, gcd-rec-sub-03, gcd-abs, gcd-rec-sub, prime-7, gcd-conq-one, prime-631, num-gcd-pos, prime-11, max_prime_divisor-nls-02, prime-odd-01, prime-163, div-mod, prime-23, gcd-mult-pos, square-neq-any-pos-02, div-gcd-is-neg, gcd-divides-both-h, div-gcd-zero, gcd-rec-sub-01, gcd-less, div-abs, divides-abs-01, prime-317, prime-5, gcd-mod-one, prime-83, prime-three, gcd-less-eq-zero, prime-1259, prime-def-prime, divides-abs-02, square-neq-prime, max_prime_divisor-abs-01, max_prime_divisor-nls-01,
• int-abs/lels is used by gcd-div-gcd-pos, square-neq-any-pos-01, div-abs-02, max_prime_divisor-ge2, prime-def-mod, div-one-one-neg, gcdhex, square-neq-pos, gcdex-smallest-pos, gcdex, gcd-rec-sub-03, divides-prime, gcd-conq-one, max_prime_divisor-nls-02, prime-ex-max, gcd-mult-pos, square-neq-any-pos-02, gcd-divides-both-h, gcd-rec-sub-01, prime-odd, gcd-nls-zero, gcd-one-eq, gcd-mod-one, max_prime_divisor-nls, gcd-mod-one-01, square-neq-any, max_prime_divisor-nls-03, gcd-one, gcd-prime, gcd-ge-one, square-neq-any-pos, prime-two, max_prime_divisor-nle-zero-01, prime-def-prime, gcd-divides-both, max_prime_divisor-nle-01,
• int-abs/lels-02 is used by gcd-div-gcd-pos, gcd-zero-05, div-div, max_prime_divisor-ge2, gcdhex, square-neq-pos, gcd-rec-sub-03, divides-prime, gcd-conq-one, case-20, max_prime_divisor-nls-02, prime-odd-01, div-gcd-is-neg-01-01, gcd-mult-pos, square-neq-any-pos-02, div-gcd-is-neg, gcd-rec-sub-01, gcd-one-eq, case-30, square-neq-any, gcd-com, gcd-rec, gcd-same, square-neq-any-pos, gcd-less-eq-zero, prime-le-2, div-div-01, gcd-zero-04, case-10, square-neq-prime, div-gcd-not-neg, gcd-abs-rew-02, case-40,
• int-abs/lels-03 is used by gcd-div-gcd-pos, gcd-zero-02, gcdex-smallest-pos, gcd-rec-sub-03, gcd-conq-one, max_prime_divisor-nls-02, div-not-ls, prime-ex-max, gcd-divides-both-h, gcd-rec-sub-01, gcd-less, gcd-mod-one, gcd-com, gcd-rec, prime-def-prime, gcd-abs-rew-02, max_prime_divisor-nle,
• int-abs/lenls is used by prime-7, prime-small, prime-5, square-neq-prime,
• int-abs/leone is used by prime-def-mod, gcd-pos, gcdex-pos, gcd-conq-one, square-neq-any-pos-02, gcd-ge-one, prime-two,
• int-abs/lep is used by gcd-rec-sub, div-mod-01,
• int-abs/lep-01 is used by gcd-rec-sub-03, gcd-divides-both-h, gcd-rec-sub-01,
• int-abs/ler is used by gcdhex, gcd-divides-both-h, gcd-divides-both,
• int-abs/lsone is used by divides-prime, div-not-ls, gcd-one, prime-def-prime,
• int-abs/minus-add is used by div-one-one-neg,
• int-abs/minus-sub is used by div-mod,
• int-abs/mone-05 is used by gcdex-pos, gcd-mod-one,
• int-abs/mone-08 is used by divides-prime,
• int-abs/neg is used by gcd-zero-05, gcd-rec-sub-03, gcd-rec-sub-01, square-neq-any-pos, square-neq-prime,
• int-abs/neg-01 is used by gcd-rec-sub-03,
• int-abs/neg-02 is used by gcd-negone-eq, square-neq-any-pos, square-neq-prime,
• int-abs/neg-03 is used by divides-neg, divides-mone, gcd-rec-sub-03, gcd-conq-one, div-abs, divides-abs-01, div-abs-04, divides-abs-02, div-neg, gcd-conq-one-01,
• int-abs/neg-05 is used by gcd-divides-both,
• int-abs/neg-06 is used by div-one-one-neg, gcd-conq-one, gcd-rec-sub-01, gcd-one, gcd-conq-one-01,
• int-abs/neg-07 is used by gcd-rec-sub-03, divides-prime, gcd-rec-sub-01,
• int-abs/neg-11 is used by gcdex, gcd-rec-sub-03,
• int-abs/neg-12 is used by gcd-rec-sub-03, gcd-rec-sub-01,
• int-abs/neg-13 is used by gcd-rec-sub-03, divides-prime, gcd-rec-sub-01, div-gcd-neg-not-zero,
• int-abs/neg-15 is used by gcdex-pos, gcdex, gcd-conq-one, gcd-rec-sub-01, divides-abs-02, divides-mult-sub, gcd-conq-one-01,
• int-abs/negeq is used by gcd-zero-05, divides-neg, div-abs-02, divides-mone, div-one-one-neg, div-one-one, gcdex, gcd-rec-sub-03, divides-prime, gcd-rec-sub-01, div-abs, divides-abs-01, gcd-mod-one, div-abs-04, gcd-negone-eq, div-abs-01, gcd-one, divides-abs-02, gcd-divides-both, div-neg,
• int-abs/negle-07 is used by square-neq-prime,
• int-abs/negle-13 is used by gcd-divides-both-h, gcd-rec-sub-01,
• int-abs/num-subadd is used by gcd-conq-one, gcd-conq-one-01,
• int-abs/numadd-01 is used by div-one-one-neg, div-one-one, prime-43, divides-prime, prime-odd-01, gcd-mod-one, gcd-negone-eq, gcd-one, case-10,
• int-abs/numle-03 is used by gcdex-pos, gcd-mod-one,
• int-abs/numleledel is used by divides-prime,
• int-abs/numleledel-01 is used by max_prime_divisor-nls-02, max_prime_divisor-nle-01, max_prime_divisor-nle,
• int-abs/numlelsdel is used by max_prime_divisor-nls-02, prime-163,
• int-abs/numlelsdel-01 is used by prime-def-prime,
• int-abs/numls-03 is used by prime-43, divides-prime, case-10,
• int-abs/numlsledel is used by max_prime_divisor-ge2, max_prime_divisor-nls-02,
• int-abs/numlsledel-01 is used by prime-def-mod, prime-7, max_prime_divisor-nls-02, prime-5, gcd-prime, prime-def-prime,
• int-abs/sub-add is used by gcd-rec-sub-03, gcd-rec-sub, gcd-rec-sub-01, gcd-add,
• int-abs/sub-add-01 is used by gcdhex, prime-ex-max,
• int-abs/sub-add-06 is used by gcd-conq-one,
• int-abs/sub-add-09 is used by gcd-rec-sub-03, gcd-rec-sub-01, divides-minus,
• int-abs/sub-eq is used by div-one-one-neg, gcdhex, gcdex, gcd-conq-one, div-mod, div-mod-01, gcd-mod-one, gcd-rec, divides-mult-sub, gcd-conq-one-01,
• int-abs/sub-eq-01 is used by divides-abs-02,
• int-abs/sub-le-01 is used by gcdex-pos,
• int-abs/sub-ls is used by prime-ex-max,
• int-abs/sub-ls-01 is used by prime-ex-max,
• int-abs/sub-minus is used by gcd-rec-sub-03,
• int-abs/sub-sub is used by gcd-conq-one, gcd-conq-one-01,
• int-abs/sub-sub-03 is used by gcd-rec-sub-01,
• int-abs/subneg is used by gcdex-pos, gcd-rec-sub-03, gcd-rec-sub-01,
• int-abs/subsub is used by gcd-rec-sub-03, gcd-rec-sub-01,
• int-abs/zero-gels-01 is used by div-div, max_prime_divisor-ge2, gcd-rec-sub-03, divides-prime, gcd-conq-one, div-gcd-is-neg-01-01, gcd-rec-sub-01, div-abs, gcd-one-eq, gcd-mod-one, max_prime_divisor-nls-zero,
• int-abs/zero-gels-02 is used by prime-not-neg, max_prime_divisor-nls-zero,
• int-abs/zero-gels-03 is used by gcd-rec-sub-03, max_prime_divisor-nls-02,
• int-abs/zero-gels-04 is used by max_prime_divisor-ge2, prime-def-mod, gcdhex, square-neq-pos, gcdex-smallest-pos, gcd-rec-sub, gcd-conq-one, max_prime_divisor-nls-02, prime-ex-max, div-mod, gcd-divides-both-h, div-mod-01, max_prime_divisor-nle-zero,

Used from specification intnat

• intnat/labs is used by gcdhex, gcdex-smallest-pos, prime-ex-max, gcd-mult-pos, square-neq-any-pos-02, gcd-divides-both-h, prime-def-prime,

Used from specification int-basic2

• int-basic2/add-c is used by gcd-conq-one,
• int-basic2/add-a is used by gcd-zero-05, coprime-divides-01, divides-neg, divides-mone, div-one-one-neg, gcdex-pos, prime-not-odd, div-one-one, gcdhex, prime-43, gcdex, gcd-rec-sub-03, gcd-rec-sub, divides-prime, divides-mult-add, gcd-conq-one, divides-add, prime-odd-01, prime-ex-max, div-mod, gcd-mult-pos, gcdex-not-unique, gcd-divides-both-h, gcd-rec-sub-01, div-abs, div-mod-01, divides-abs-01, gcd-nls-zero, gcd-mod-one, div-abs-04, gcd-div-rest, gcd-negone-eq, gcd-rec, gcd-one, divides-minus, prime-two, gcd-rec-sub-02, case-10, divides-abs-02, square-neq-prime, divides-mult-sub, gcd-add, div-neg, gcd-conq-one-01,
• int-basic2/add-c is used by gcd-zero-05, coprime-divides-01, divides-neg, div-abs-02, divides-mone, div-one-one-neg, gcdex-pos, prime-not-odd, div-one-one, gcdhex, prime-43, gcdex, gcd-rec-sub-03, gcd-rec-sub, divides-prime, divides-mult-add, gcd-conq-one, divides-add, prime-odd-01, prime-ex-max, div-mod, gcd-mult-pos, gcdex-not-unique, gcd-divides-both-h, gcd-rec-sub-01, div-abs, div-mod-01, divides-abs-01, gcd-nls-zero, gcd-mod-one, div-abs-04, gcd-div-rest, gcd-negone-eq, div-abs-01, gcd-rec, gcd-one, divides-minus, prime-two, gcd-rec-sub-02, case-10, divides-abs-02, square-neq-prime, divides-mult-sub, gcd-add, div-neg, gcd-conq-one-01,
• int-basic2/add-in is used by gcdhex, gcdex-not-unique, gcd-rec-sub-01, div-mod-01,
• int-basic2/add-less is used by gcd-rec-sub-03, gcd-add,
• int-basic2/add-zero is used by gcdex-pos, gcdhex, gcd-rec-sub-03, gcd-conq-one, gcd-divides-both-h, gcd-rec-sub-01, gcd-div-rest, square-neq-prime,
• int-basic2/ls is used by gcd-rec-sub-03, gcd-divides-both-h, gcd-nls-zero,
• int-basic2/ls-01 is used by prime-ex-max,
• int-basic2/ls-02 is used by gcd-rec-sub-03, gcd-rec-sub, gcd-divides-both-h, gcd-rec-sub-02,
• int-basic2/num-between is used by prime-two-01, case-20, case-30, case-10, case-40,
• int-basic2/succ-01 is used by prime-43, case-10,
• int-basic2/zero-01 is used by gcd-rec-sub-01,
• int-basic2/zero-02 is used by gcd-rec-sub, gcd-divides-both-h,

Used from specification int-div

• int-div/div-eq-zero-01 is used by div-gcd-zero,
• int-div/div-le-same is used by max_prime_divisor-nle-01,
• int-div/div-lezero is used by square-neq-any-pos-02, max_prime_divisor-nle-zero-01,
• int-div/div-ls-same is used by max_prime_divisor-nls,
• int-div/div-ls-zero is used by gcd-nls-zero,
• int-div/div-mult is used by max_prime_divisor-ge2, max_prime_divisor-divides-02, max_prime_divisor-divides-03, exgcd-div,
• int-div/mod-ngr is used by gcd-mod-one-01,
• int-div/mod-nls-01 is used by gcdhex,
• int-div/mod-rec is used by gcd-rec-sub,
• int-div/mod-rew is used by gcdhex,
• int-div/mod-two-06 is used by prime-odd,
• int-div/modex is used by prime-def-mod, prime-odd-01, divides-mod, prime-odd, div-mod-zero-01,
• int-div/num-neg is used by gcd-negone-eq,
• int-div/nummult-eq is used by mod-gcd-01, mod-gcd,
• int-div/abs is used by gcd-div-gcd, square-neq-any-pos-02, max_prime_divisor-abs,
• int-div/abs-01 is used by gcd-div-gcd,
• int-div/div-abs is used by div-gcd-zero,
• int-div/div-elim-negpos is used by gcd-one-eq,
• int-div/div-elim-pospos is used by gcd-div-gcd-pos, prime-odd-01, div-mod-01, gcd-rec,
• int-div/div-eq-same is used by gcd-div-eq, div-eq,
• int-div/div-lezero is used by div-gcd-not-neg,
• int-div/div-mult-03 is used by div-mult-shift, gcd-div-mult, prime-divides-01, max_prime_divisor-nls-02, max_prime_divisor-nls-03, div-eq, div-eq-one,
• int-div/div-same is used by square-neq-any-pos-01, square-neq-pos, gcd-div-gcd, square-neq-any-pos-02, gcd-one-eq-01, div-gcd-neg-not-zero, gcd-one-eq-02, div-eq-one,
• int-div/div-zero-ngr is used by div-gcd-is-neg, max_prime_divisor-nls,
• int-div/mod-les is used by gcd-mult-pos,
• int-div/mod-less-01 is used by div-mod-01,
• int-div/mod-mult-02 is used by gcd-mult-pos,
• int-div/mod-mult-04 is used by prime-def-mod, gcd-mult-01, div-mod-zero, div-eq,
• int-div/mod-mult-pos is used by gcd-mod-one,
• int-div/mod-mult-pos-01 is used by prime-odd-01, div-mod-01,
• int-div/mod-nle is used by gcd-mult-pos,
• int-div/mod-one is used by prime-def-mod,
• int-div/mod-same is used by gcdhex,
• int-div/mod-zero is used by gcdhex, gcd-mult-pos, div-mod-01,
• int-div/mod-zero-01 is used by gcd-mult-pos,
• int-div/mod-zero-04 is used by mod-gcd-01, gcd-mod-one, gcd-mod-one-01,
• int-div/modeven-neg is used by prime-odd-01,
• int-div/modeven-neg-01 is used by prime-odd-01,
• int-div/neg is used by div-gcd-neg-not-zero,
• int-div/neg-01 is used by gcd-negone-eq,
• int-div/neqf is used by square-neq-any-pos-01, square-neq-pos, square-neq-any-pos-02,
• int-div/nummult-le-02 is used by prime-two,
• int-div/nummult-ls-02 is used by prime-two,
• int-div/one is used by div-gcd-one,
• int-div/one-01 is used by prime-13, prime-43, prime-7, prime-631, prime-11, prime-163, prime-23, prime-317, prime-5, prime-83, prime-three, prime-1259,
• int-div/zero is used by square-neq-any-pos-01, square-neq-pos, gcd-div-gcd, square-neq-any-pos-02, gcd-one-eq,
• int-div/zero-07 is used by max_prime_divisor-nle-zero-01,

Used from specification int-min

• int-min/not-odd-ex is used by prime-not-odd,