Used simplifier rules/spec theorems by specification

Used from specification int-mult

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

Used from specification int-basic1

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

Used from specification int-square

• int-square/isSquare-def is used by pot-isSquare, isSquare-mult-aux, isSquare-mult,
• int-square/isSquare-one is used by pot-isSquare, isSquare-mult-aux,
• int-square/isSquare-square is used by pot-isSquare, isSquare-mult-aux, isSquare-mult,
• int-square/isSquare-zero is used by isSquare-mult,

Used from specification int-pot

• int-pot/Pot-pos is used by pot-isSquare, divides-pot-prime, coprime-pot,
• int-pot/pot-dist-pos is used by pot-isSquare,
• int-pot/Pot-zero is used by pot-isSquare, divides-pot-prime, coprime-pot,
• int-pot/pot-square-02 is used by pot-isSquare,

Used from specification int-abs

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

Used from specification int-min

• int-min/even-def is used by pot-isSquare,
• int-min/not-odd-ex is used by prime-not-odd,
• int-min/even-2 is used by pot-isSquare,
• int-min/even-not is used by pot-isSquare,

Used from specification nat-basic2

• nat-basic2/a is used by divides-pot-prime, coprime-pot,
• nat-basic2/c is used by divides-pot-prime, coprime-pot,
• nat-basic2/s is used by divides-pot-prime, coprime-pot,

Used from specification intnat

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

Used from specification int-basic2

• int-basic2/add-c is used by gcd-conq-one,
• int-basic2/add-a is used by square-neq-prime, square-neq-any-pos, prime-two, prime-odd-01, prime-not-odd, prime-ex-max, prime-43, pot-isSquare, max_prime_divisor-nls-02, max_prime_divisor-nls, isSquare-mult-aux, isSquare-mult, gcdhex, gcdex-pos, gcdex-not-unique, gcdex, gcd-zero-05, gcd-rec-sub-03, gcd-rec-sub-02, gcd-rec-sub-01, gcd-rec-sub, gcd-rec, gcd-one, gcd-nls-zero, gcd-negone-eq, gcd-mult-pos, gcd-mod-one, gcd-divides-both-h, gcd-divides-both, gcd-div-rest, gcd-conq-one-01, gcd-conq-one, gcd-add, divides-prime, divides-pot-prime, divides-neg, divides-mult-sub, divides-mult-add, divides-mone, divides-minus, divides-add, divides-abs-02, divides-abs-01, div-one-one-neg, div-one-one, div-neg, div-mod-01, div-mod, div-abs-04, div-abs-02, div-abs-01, div-abs, coprime-pot, coprime-divides-01, case-10,
• int-basic2/add-c is used by square-neq-prime, square-neq-any-pos, prime-two, prime-odd-01, prime-not-odd, prime-ex-max, prime-43, pot-isSquare, max_prime_divisor-nls-02, max_prime_divisor-nls, isSquare-mult-aux, isSquare-mult, gcdhex, gcdex-pos, gcdex-not-unique, gcdex, gcd-zero-05, gcd-rec-sub-03, gcd-rec-sub-02, gcd-rec-sub-01, gcd-rec-sub, gcd-rec, gcd-one, gcd-nls-zero, gcd-negone-eq, gcd-mult-pos, gcd-mod-one, gcd-divides-both-h, gcd-divides-both, gcd-div-rest, gcd-conq-one-01, gcd-conq-one, gcd-add, divides-prime, divides-pot-prime, divides-neg, divides-mult-sub, divides-mult-add, divides-mone, divides-minus, divides-add, divides-abs-02, divides-abs-01, div-one-one-neg, div-one-one, div-neg, div-mod-01, div-mod, div-abs-04, div-abs-02, div-abs-01, div-abs, coprime-pot, coprime-divides-01, case-10,
• 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 isSquare-mult, gcdex-pos, gcd-rec-sub-03, gcd-rec-sub-01,
• int-basic2/add-zero-rev is used by square-neq-prime, isSquare-mult-aux, gcdhex, gcd-divides-both-h, gcd-div-rest, gcd-conq-one,
• int-basic2/ls is used by isSquare-mult-aux, gcd-rec-sub-03, gcd-nls-zero, gcd-divides-both-h,
• int-basic2/ls-02 is used by isSquare-mult, gcd-rec-sub-03, gcd-rec-sub-02, gcd-rec-sub, gcd-divides-both-h, gcd-divides-both, div-abs-02, div-abs-01,
• int-basic2/ls-add-both is used by prime-ex-max,
• int-basic2/lst-03 is used by max_prime_divisor-nls-02, max_prime_divisor-nls,
• int-basic2/num-between is used by prime-two-01, case-40, case-30, case-20, case-10,
• int-basic2/succ-01 is used by square-neq-prime, square-neq-any-pos, square-neq-any, prime-ex-max, prime-def-prime, prime-43, max_prime_divisor-nls-zero, max_prime_divisor-nls-02, max_prime_divisor-nls, isSquare-mult-aux, gcd-nls-zero, gcd-mod-one, gcd-divides-both-h, gcd-conq-one, div-gcd-is-neg-01, div-gcd-is-neg, div-abs-02, div-abs-01, 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-03, max_prime_divisor-divides-02, 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-odd-01, prime-odd, prime-def-mod, mod-square-10, divides-mod, 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 square-neq-any-pos-02, max_prime_divisor-abs, gcd-div-gcd,
• 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 prime-odd-01, gcd-rec, gcd-div-gcd-pos, div-mod-01,
• 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-ls-same is used by div-gcd-is-neg,
• int-div/div-mult-03 is used by prime-divides-01, max_prime_divisor-nls-03, max_prime_divisor-nls-02, gcd-div-mult, div-mult-shift, div-eq-one, div-eq,
• int-div/div-same is used by square-neq-pos, square-neq-any-pos-01, gcd-one-eq-02, gcd-one-eq-01, gcd-div-gcd, div-gcd-neg-not-zero, div-eq-one,
• int-div/div-zero-05 is used by square-neq-any-pos-02, square-neq-any-pos-01,
• int-div/div-zero-06 is used by max_prime_divisor-nle-zero-01,
• int-div/div-zero-ngr is used by max_prime_divisor-nls, div-gcd-is-neg,
• int-div/lsfc-01 is used by square-neq-any-pos-02,
• 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 div-mod-01,
• int-div/mod-mult-pos-02 is used by prime-odd-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-04 is used by mod-gcd-01, gcd-mod-one-01, gcd-mod-one,
• int-div/mod-zero-ls is used by gcd-mult-pos,
• int-div/mod-zero-num is used by mod-square-10,
• 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-pos, square-neq-any-pos-02, square-neq-any-pos-01,
• int-div/nummult-eq-01 is used by mod-square-10,
• 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-three, prime-83, prime-7, prime-631, prime-5, prime-43, prime-317, prime-23, prime-163, prime-13, prime-1259, prime-11,
• int-div/zero is used by square-neq-pos, square-neq-any-pos-01, gcd-one-eq, gcd-div-gcd,
• int-div/zero-07 is used by max_prime_divisor-nle-zero-01,