Used simplifier rules/spec theorems by specification

Used from specification int-basic1

• int-basic1/forward-pos is used by range-cong-dups, lagrange-lemma-smallest, four-square-mod-zero, four-square-divides-all, four-square-congmod, fermat-pos, fermat-for-rsa, diff-primes-neg, diff-primes, congmod-inverse-smallest, congmod-inverse-pos, congmod-inverse, Shor-algorithm, RSA-decrypt-ij-vars, Lagrange-SumOf4Squares-primes, Diffie-Hellman,
• int-basic1/ls-01 is used by range-cong-dups, mod-zero-neg, mod-zero, mod-rec-neg, mod-rec-any, mod-neg, mod-mult-add, fermat-pos, ex-modeq-half, congmod-inverse-smallest, congmod-inverse-pos, congmod-def-mod-01, Shor-algorithm, RSA-decrypt-ij-vars, Diffie-Hellman,
• int-basic1/lst-01 is used by mod-ex-div, mod-abs-neg-neg, four-square-mod-zero,
• int-basic1/numlsf is used by Shor-algorithm, RSA-decrypt-ij-vars,
• int-basic1/numlslsdel is used by fermat-1,
• int-basic1/numlslsdel-01 is used by fermat-for-rsa, RSA-decrypt-ij-vars,
• int-basic1/two-ls is used by Lagrange-SumOf4Squares-primes,

Used from specification int-mult

• int-mult/commutativity is used by fermat-for-rsa,
• int-mult/dist-lsplit is used by four-square-divides-all, Shor-algorithm,
• int-mult/dist-rmerge is used by Lagrange-SumOf4Squares-primes,
• int-mult/dist-rsplit is used by four-square-divides-all, diff-primes-neg, diff-primes-dups, diff-primes, Lagrange-SumOf4Squares-primes,
• int-mult/dist-sub-split is used by mod-mult-law, four-square-divides-all, div-mod-eq, diff-primes-neg, diff-primes, congmod-def-mod, Shor-algorithm,
• int-mult/ls-pos is used by lagrange-lemma,
• int-mult/ls-same-01 is used by lagrange-lemma,
• int-mult/minus-left is used by mod-mult-02,
• int-mult/modeqp-copied is used by mod-neg,
• int-mult/numeq-01 is used by mod-rec-neg,
• int-mult/numsucc is used by mod-rec-neg, ex-modeq-half,
• int-mult/pred-rmerge is used by cong-mult-02,
• int-mult/zero-le is used by mod-crt, RSA-decrypt-ij-vars,
• int-mult/Mult-zero is used by mod-rec-neg, mod-neg, mod-mult-add, mod-mult-03, mod-mult-01, four-square-odd-ls, fermat-for-rsa, ex-modeq-half, congmod-inverse-smallest, congmod-inverse-pos, congmod-inverse, cong-crt-01, RSA-decrypt-ij-vars,
• int-mult/abs-eqall is used by four-square-odd-ls, Shor-algorithm,
• int-mult/add-mult-two is used by mod-rec-any, lagrange-lemma, four-square-odd-ls, fermat-1, ex-modeq-half, diff-primes-neg, diff-primes-dups, diff-primes, Shor-algorithm, Lagrange-SumOf4Squares-primes,
• int-mult/associativity is used by rem-mod-pos, mod-zero-neg, mod-zero, mod-rec-neg, mod-rec, mod-neg, mod-mult-law, mod-mult-add-01, mod-mult-add, mod-mult-03, mod-mult-01, mod-mult, mod-ex-div, mod-crt, mod-add-law, mod-abs-neg-neg, mod-abs-neg-div, lagrange-lemma, four-square-odd-ls, four-square-mod-zero, four-square-divides-all, four-square-congmod, fermat-pos, fermat-for-rsa, fermat-2, fermat-1, ex-modeq-half, div-mod-eq, diff-primes-neg, diff-primes-dups, diff-primes, congmod-inverse-smallest, congmod-inverse-pos, congmod-inverse, congmod-def-mod, cong-mult-rew, cong-mult-02, cong-mult, cong-crt-01, cong-crt, cong-add, Shor-algorithm, RSA-decrypt-ij-vars, Lagrange-SumOf4Squares-primes,
• int-mult/commutativity is used by rem-mod-pos, mod-zero-neg, mod-zero, mod-rec-neg, mod-rec, mod-neg, mod-mult-law, mod-mult-add-01, mod-mult-add, mod-mult-03, mod-mult-01, mod-mult, mod-ex-div, mod-crt, mod-add-law, mod-abs-neg-neg, mod-abs-neg-div, lagrange-lemma, four-square-odd-ls, four-square-mod-zero, four-square-divides-all, four-square-congmod, fermat-pos, fermat-for-rsa, fermat-2, fermat-1, ex-modeq-half, div-mod-eq, diff-primes-neg, diff-primes-dups, diff-primes, congmod-inverse-smallest, congmod-inverse-pos, congmod-inverse, congmod-def-mod, cong-mult-rew, cong-mult-03, cong-mult-02, cong-mult, cong-crt-01, cong-crt, cong-add, Shor-algorithm, RSA-decrypt-ij-vars, Lagrange-SumOf4Squares-primes, Diffie-Hellman,
• int-mult/eq-dist is used by mod-rec-neg, mod-mult-law, mod-mult-add, mod-ex-div, mod-add-law, four-square-mod-zero, four-square-divides-all, diff-primes-neg, diff-primes, cong-mult-rew,
• int-mult/eq-nonzero is used by fermat-2, congmod-def-mod,
• int-mult/eq-one is used by congmod-inverse, RSA-decrypt-ij-vars,
• int-mult/eq-pos is used by four-square-odd-ls, four-square-mod-zero, Lagrange-SumOf4Squares-primes,
• int-mult/eq-succ is used by mod-mult-add,
• int-mult/le-pos is used by lagrange-lemma,
• int-mult/ls-add is used by mod-zero,
• int-mult/ls-dist-03 is used by mod-rec-neg,
• int-mult/ls-pos is used by lagrange-lemma, Lagrange-SumOf4Squares-primes,
• int-mult/ls-same is used by mod-zero-neg, mod-rec-neg, mod-neg, mod-ex-div,
• int-mult/ls-same-01 is used by four-square-mod-zero, Lagrange-SumOf4Squares-primes,
• int-mult/minus-left is used by mod-mult-law, mod-add-law, congmod-inverse,
• int-mult/minus-one-01 is used by congmod-inverse, RSA-decrypt-ij-vars,
• int-mult/modzero-02 is used by mod-rec-neg,
• int-mult/neq-not-zero is used by fermat-2, Lagrange-SumOf4Squares-primes,
• int-mult/neq-two is used by Lagrange-SumOf4Squares-primes,
• int-mult/numabs-01 is used by four-square-odd-ls,
• int-mult/numeq-02 is used by mod-abs-neg-neg,
• int-mult/numle-02 is used by four-square-odd-ls,
• int-mult/numle-08 is used by lagrange-lemma,
• int-mult/numle-12 is used by ex-modeq-half,
• int-mult/numls-04 is used by ex-modeq-half,
• int-mult/numsucc is used by four-square-odd-ls,
• int-mult/one is used by mod-rec-neg, mod-mult-add, mod-ex-div, mod-abs-neg-neg, lagrange-lemma, four-square-odd-ls, fermat-pos, fermat-for-rsa, fermat-2, ex-modeq-half, div-mod-eq, congmod-inverse-pos, congmod-inverse, Shor-algorithm, Lagrange-SumOf4Squares-primes,
• int-mult/one-01 is used by mod-mult-add, lagrange-lemma, congmod-inverse-smallest, congmod-inverse-pos, congmod-inverse, RSA-decrypt-ij-vars,
• int-mult/square-le is used by lagrange-lemma,
• int-mult/two-zero is used by four-square-odd-ls,
• int-mult/zero-eq is used by mod-zero-neg, mod-zero, cong-crt-01,
• int-mult/zero-ge is used by four-square-odd-ls, four-square-mod-zero, ex-modeq-half, diff-primes-neg, diff-primes, congmod-inverse-pos, congmod-inverse, RSA-decrypt-ij-vars,
• int-mult/zero-ge-01 is used by fermat-for-rsa,
• int-mult/zero-ge-02 is used by fermat-for-rsa,
• int-mult/zero-ge-add is used by mod-rec,
• int-mult/zero-gr is used by four-square-odd-ls, four-square-mod-zero, diff-primes-neg, diff-primes, RSA-decrypt-ij-vars, Lagrange-SumOf4Squares-primes,
• int-mult/zero-gr-add is used by mod-zero-neg, mod-rec-neg,
• int-mult/zero-le is used by lagrange-lemma, RSA-decrypt-ij-vars,
• int-mult/zero-le-03 is used by mod-crt,
• int-mult/zero-ls is used by mod-zero-neg, mod-rec-neg, ex-modeq-half, congmod-inverse, RSA-decrypt-ij-vars,
• int-mult/zero-ls-01 is used by mod-abs-neg-div, RSA-decrypt-ij-vars,
• int-mult/zero-ls-02 is used by RSA-decrypt-ij-vars,

Used from specification int-gcd

• int-gcd/coprime-divides is used by cong-crt-01,
• int-gcd/coprime-divides-02 is used by Shor-algorithm,
• int-gcd/div-mod is used by diff-primes-neg, diff-primes,
• int-gcd/div-mult-01 is used by cong-crt-01,
• int-gcd/div-neg is used by cong-neg,
• int-gcd/div-not-ls is used by diff-primes-neg, diff-primes,
• int-gcd/div-one-pos is used by RSA-decrypt-ij-vars,
• int-gcd/divides is used by lagrange-lemma, four-square-mod-zero, four-square-divides-all, four-square-congmod, fermat-for-rsa, congmod-inverse-smallest, congmod-def-mod, cong-mult-rew, cong-crt-01, cong-crt, cong-add, RSA-decrypt-ij-vars, Lagrange-SumOf4Squares-primes,
• int-gcd/divides-minus is used by lagrange-lemma, cong-comm,
• int-gcd/divides-mult is used by cong-crt,
• int-gcd/divides-mult-add is used by cong-mult-rew,
• int-gcd/divides-prime is used by cong-crt,
• int-gcd/gcd-abs-rew-02 is used by congmod-inverse,
• int-gcd/gcd-com is used by fermat-pos,
• int-gcd/gcd-mod-one-01 is used by congmod-inverse-pos, congmod-inverse,
• int-gcd/gcd-one-prime is used by fermat-for-rsa,
• int-gcd/gcd-prime is used by fermat-pos,
• int-gcd/prime-divides is used by diff-primes-neg, diff-primes,
• int-gcd/prime-mult-not is used by four-square-mod-zero,
• int-gcd/div-abs is used by congmod-inverse,
• int-gcd/div-abs-02 is used by lagrange-lemma, four-square-mod-zero, four-square-divides-all, four-square-congmod, fermat-1, diff-primes-neg, diff-primes, congmod-mod-abs, congmod-inverse-smallest, congmod-inverse, congmod-def-mod, cong-same-add, cong-neg, cong-mult-rew, cong-mult-02, cong-mult, cong-crt-01, cong-comm, Shor-algorithm, RSA-decrypt-ij-vars,
• int-gcd/div-mult is used by four-square-divides-all, four-square-congmod, cong-mult, RSA-decrypt-ij-vars,
• int-gcd/div-one is used by cong-one,
• int-gcd/div-zero-01 is used by cong-same,
• int-gcd/div-zero-zero is used by congmod-inverse, cong-zero, RSA-decrypt-ij-vars,
• int-gcd/divides-abs is used by congmod-mod-abs,
• int-gcd/divides-add is used by cong-mult,
• int-gcd/divides-mone is used by cong-one-01,
• int-gcd/divides-mult-01 is used by cong-mult-02,
• int-gcd/divides-mult-add is used by four-square-divides-all, four-square-congmod, fermat-1, cong-mult,
• int-gcd/gcd-add is used by fermat-pos,
• int-gcd/gcd-com is used by fermat-pos, fermat-2-mod, fermat-2, congmod-inverse-smallest, congmod-inverse-pos, congmod-inverse, Shor-algorithm, RSA-decrypt-ij-vars,
• int-gcd/gcd-div2 is used by Shor-algorithm,
• int-gcd/gcd-less-eq-zero is used by Shor-algorithm,
• int-gcd/gcd-one-01 is used by fermat-pos, fermat-for-rsa, fermat-2-mod, congmod-inverse-smallest, congmod-inverse-pos, congmod-inverse, RSA-decrypt-ij-vars,
• int-gcd/gcd-primes is used by cong-crt-01,
• int-gcd/gcd-zero-03 is used by congmod-inverse-smallest,
• int-gcd/gcd-zero-04 is used by congmod-inverse-smallest, congmod-inverse-pos, congmod-inverse, Shor-algorithm, RSA-decrypt-ij-vars,
• int-gcd/gcd-zero-zero is used by Shor-algorithm,
• int-gcd/prime-abs is used by cong-crt,
• int-gcd/prime-divides is used by fermat-pos, cong-crt,
• int-gcd/prime-not-neg is used by fermat-pos, diff-primes-neg, diff-primes-dups, diff-primes,
• int-gcd/prime-not-neg-01 is used by mod-crt, lagrange-lemma, fermat-pos, fermat-2-mod, fermat-2, fermat-1-mod, fermat-1, diff-primes-dups, cong-crt-01, cong-crt,
• int-gcd/prime-not-odd is used by fermat-1,
• int-gcd/prime-odd-01 is used by lagrange-lemma, diff-primes-neg, diff-primes-dups, diff-primes,
• int-gcd/prime-one is used by lagrange-lemma, fermat-2-mod, cong-crt,
• int-gcd/prime-two-01 is used by Lagrange-SumOf4Squares,

Used from specification intlist

• intlist/all_prime_divisors-product is used by Lagrange-SumOf4Squares,
• intlist/countFun-at is used by diff-primes-neg, diff-primes,
• intlist/countFun-in is used by lagrange-lemma, fermat-pos, diff-primes-dups,
• intlist/countFun-last is used by fermat-pos,
• intlist/countFun-length is used by diff-primes-neg, diff-primes-dups, diff-primes,
• intlist/countFun-rec is used by fermat-pos,
• intlist/map-in is used by range-cong-dups,
• intlist/range-dups is used by range-cong-dups, diff-primes-dups,
• intlist/all_prime_divisors-in-01 is used by Lagrange-SumOf4Squares,
• intlist/countFun-one is used by diff-primes-neg, diff-primes,
• intlist/map-at is used by range-cong-dups,
• intlist/map-length is used by range-cong-dups,
• intlist/prod-empty is used by lagrange-primedivisors,
• intlist/prod-rec is used by lagrange-primedivisors,
• intlist/sum-app is used by fermat-pos,
• intlist/sum-one is used by fermat-pos,
• intlist/sum-rec is used by fermat-pos,

Used from specification int-square

• int-square/Square-def is used by lagrange-lemma, four-square-odd-ls, four-square-mod-zero, four-square-divides-all, four-square-congmod, diff-primes-neg, diff-primes, Lagrange-SumOf4Squares-primes,
• int-square/euler-four-square-identity2 is used by lagrange-primedivisors, Lagrange-SumOf4Squares-primes,
• int-square/le is used by lagrange-lemma, four-square-odd-ls,
• int-square/two-even-01 is used by Lagrange-SumOf4Squares-primes,
• int-square/two-ls is used by four-square-odd-ls,
• int-square/two-mult is used by four-square-congmod, Lagrange-SumOf4Squares-primes,
• int-square/two-plus is used by four-square-congmod,
• int-square/four-square-le-zero is used by Lagrange-SumOf4Squares-primes,
• int-square/neq is used by four-square-odd-ls, Lagrange-SumOf4Squares-primes,
• int-square/one is used by lagrange-primedivisors, lagrange-lemma-smallest, Lagrange-SumOf4Squares,
• int-square/two-not-neg is used by lagrange-lemma,
• int-square/zero-i is used by lagrange-primedivisors, lagrange-lemma-smallest, lagrange-lemma, diff-primes-neg, diff-primes, Lagrange-SumOf4Squares,

Used from specification nat

• nat/lels is used by diff-primes-neg, diff-primes,

Used from specification int-pot

• int-pot/Pot-pos is used by mod-pot-pot, fermat-2, RSA-decrypt-ij-vars,
• int-pot/minus-odd is used by fermat-1,
• int-pot/pot-dist-pos is used by Shor-algorithm,
• int-pot/pot-pot is used by Diffie-Hellman,
• int-pot/pot-pot-01 is used by RSA-decrypt-ij-vars,
• int-pot/pot-pot-02 is used by fermat-for-rsa,
• int-pot/succ is used by mod-pot-pot,
• int-pot/zero-01 is used by fermat-1,
• int-pot/Pot-zero is used by mod-pot-pot, fermat-pos, fermat-for-rsa, fermat-2-mod, Shor-algorithm, RSA-decrypt-ij-vars,
• int-pot/even-square is used by even-sum,
• int-pot/minus-square-01 is used by fermat-1,
• int-pot/notneg-02 is used by Shor-algorithm, RSA-decrypt-ij-vars,
• int-pot/odd-square is used by even-sum,
• int-pot/one is used by RSA-decrypt-ij-vars,
• int-pot/one-01 is used by fermat-pos,
• int-pot/pot-lez is used by Shor-algorithm,
• int-pot/pot-zero-01 is used by Shor-algorithm,
• int-pot/zero-01 is used by RSA-decrypt-ij-vars,

Used from specification int-abs

• int-abs/Abs-neg is used by mod-rec-any, ex-modeq-half,
• int-abs/Abs-pos is used by mod-abs-pos, ex-modeq-half, diff-primes-dups, congmod-def-mod-02, Shor-algorithm,
• int-abs/abs-08 is used by ex-modeq-half,
• int-abs/add-rew is used by mod-mult-law, mod-add-law, congmod-def-mod,
• int-abs/estimate-add1-le-left is used by lagrange-lemma,
• int-abs/estimate-add1-le-right is used by diff-primes-neg, diff-primes,
• int-abs/forward-lele is used by lagrange-lemma,
• int-abs/le-rec is used by congmod-inverse-pos, Shor-algorithm,
• int-abs/notle-pos is used by diff-primes-neg, diff-primes,
• int-abs/ple is used by four-square-odd-ls,
• int-abs/sub-same-01 is used by congmod-inverse, cong-crt-01,
• int-abs/succ-01 is used by lagrange-lemma,
• int-abs/Abs-pos is used by mod-rec-any, ex-modeq-half,
• int-abs/Sub-def is used by mod-rec-any, mod-mult-law, ex-modeq-half, div-mod-eq, congmod-def-mod, cong-neg, cong-mult-rew, Shor-algorithm,
• int-abs/abs is used by lagrange-lemma-smallest, congmod-inverse-pos, Shor-algorithm,
• int-abs/abs-01 is used by congmod-inverse, congmod-def-mod-01,
• int-abs/abs-06 is used by mod-rec-any, ex-modeq-half, congmod-inverse, congmod-def-mod-02, congmod-def-mod-01,
• int-abs/abs-07 is used by congmod-inverse, congmod-def-mod-01, cong-zero,
• int-abs/abs-08 is used by mod-zero-neg, mod-rec-neg, mod-neg, mod-ex-div, mod-abs-pos, mod-abs-neg-neg, mod-abs-neg-div, ex-modeq-half, congmod-inverse, congmod-def-mod-02,
• int-abs/abs-09 is used by lagrange-lemma, cong-crt, RSA-decrypt-ij-vars,
• int-abs/abs-16 is used by mod-abs-neg, lagrange-lemma-smallest, lagrange-lemma, four-square-odd-ls, four-square-congmod, congmod-inverse-smallest, cong-crt, RSA-decrypt-ij-vars, Lagrange-SumOf4Squares-primes,
• int-abs/abs-neg is used by four-square-mod-zero, congmod-inverse,
• int-abs/abs-one-01 is used by congmod-inverse,
• int-abs/absle is used by mod-pot-pot, lagrange-lemma, ex-modeq-half, congmod-inverse-smallest, congmod-inverse-pos, congmod-inverse,
• int-abs/anti is used by mod-zero-neg, mod-rec-any, mod-pot-pot, mod-mult-add, lagrange-lemma, fermat-pos, fermat-for-rsa, ex-modeq-half, diff-primes-neg, diff-primes-dups, diff-primes, congmod-inverse-pos,
• int-abs/bet is used by mod-mult-add, lagrange-lemma, fermat-pos, fermat-for-rsa, fermat-2-mod, congmod-inverse-smallest, congmod-inverse-pos, RSA-decrypt-ij-vars,
• int-abs/bet-01 is used by congmod-inverse-smallest,
• int-abs/elim-sub is used by mod-rec, mod-pot-pot, mod-mult-law, mod-mult-add, mod-ex-div, fermat-pos, fermat-1, congmod-mod-abs, congmod-inverse-smallest, cong-mult,
• int-abs/forward-le is used by mod-rec-any, lagrange-lemma, four-square-odd-ls, ex-modeq-half, diff-primes-neg, diff-primes, congmod-inverse-smallest,
• int-abs/forward-le-01 is used by rem-mod-pos, range-cong-dups, mod-zero, mod-rec-any, mod-rec, mod-pot-pot, mod-pos-rev, mod-pos, mod-le-same, mod-i2n, mod-ex-div, mod-crt, mod-abs-pos, lagrange-lemma, four-square-mod-zero, fermat-pos, fermat-for-rsa, ex-modeq-half, diff-primes-neg, diff-primes-dups, diff-primes, congmod-inverse-smallest, congmod-inverse-pos, congmod-inverse, congmod-def-mod-02, congmod-def-mod-01, cong-crt-01, cong-crt, Shor-algorithm, RSA-decrypt-ij-vars, Lagrange-SumOf4Squares-primes, Lagrange-SumOf4Squares, Diffie-Hellman,
• int-abs/forward-le-02 is used by mod-zero-neg, mod-zero-04, mod-zero-02, mod-rec-neg, mod-rec-any, mod-pos, mod-neg, mod-mult-add, mod-ex-div, mod-abs-pos, mod-abs-neg-neg, mod-abs-neg-div, lagrange-lemma, fermat-1, ex-modeq-half, div-mod-eq, diff-primes-dups, congmod-inverse-pos, congmod-inverse, congmod-def-mod-02, congmod-def-mod-01, RSA-decrypt-ij-vars,
• int-abs/forward-le-03 is used by diff-primes-neg, diff-primes-dups, diff-primes, Shor-algorithm,
• int-abs/forward-le-04 is used by mod-rec-neg, mod-neg, mod-mult-add, mod-ex-div, mod-crt, lagrange-lemma, fermat-1, ex-modeq-half, diff-primes-neg, diff-primes-dups, diff-primes, congmod-inverse, cong-mult, Shor-algorithm, RSA-decrypt-ij-vars,
• int-abs/forward-le-05 is used by rem-mod-pos, range-cong-dups, mod-zero-neg, mod-zero, mod-rec-neg, mod-rec-any, mod-rec, mod-pot-pot, mod-pos, mod-plus, mod-neg, mod-mult-law, mod-mult-add, mod-mult-01, mod-mod, mod-le-same, mod-i2n, mod-ex-div, mod-crt, mod-add-law, mod-abs-neg-div, lagrange-lemma-smallest, lagrange-lemma, four-square-odd-ls, four-square-mod-zero, four-square-divides-all, four-square-congmod, fermat-pos, fermat-for-rsa, fermat-2-mod, fermat-1, ex-modeq-half-all, ex-modeq-half, diff-primes-neg, diff-primes, congmod-inverse-smallest, congmod-inverse-pos, congmod-inverse, congmod-def-mod-01, congmod-def-mod, cong-mult, cong-crt-01, cong-crt, Shor-algorithm, RSA-decrypt-ij-vars, Lagrange-SumOf4Squares-primes, Lagrange-SumOf4Squares, Diffie-Hellman,
• int-abs/forward-lele is used by mod-ex-div, mod-crt, lagrange-lemma, four-square-odd-ls, diff-primes-neg, diff-primes-dups, diff-primes, RSA-decrypt-ij-vars,
• int-abs/forward-lels is used by range-cong-dups, mod-rec-neg, mod-neg, mod-mult-add, mod-ex-div, mod-crt, lagrange-lemma, four-square-odd-ls, diff-primes-neg, diff-primes-dups, diff-primes, congmod-inverse-pos, congmod-inverse, Shor-algorithm, RSA-decrypt-ij-vars, Lagrange-SumOf4Squares-primes,
• int-abs/forward-lsle is used by mod-rec-any, mod-rec, mod-pos, mod-le-same, mod-ex-div, mod-abs-pos, lagrange-lemma, four-square-odd-ls, ex-modeq-half, diff-primes-neg, diff-primes-dups, diff-primes, congmod-inverse-smallest, congmod-inverse-pos, congmod-def-mod-02, congmod-def-mod-01,
• int-abs/gr-def is used by Lagrange-SumOf4Squares-primes,
• int-abs/int-simp-09 is used by lagrange-lemma,
• int-abs/le-add is used by lagrange-lemma,
• int-abs/le-add-03 is used by fermat-pos,
• int-abs/lels is used by range-cong-dups, mod-zero-neg, mod-rec-neg, mod-rec-any, mod-pot-pot, mod-pos, mod-neg, mod-mult-add, mod-mod, mod-le-same, mod-ex-div, mod-crt, mod-abs-neg-neg, lagrange-lemma-smallest, lagrange-lemma, four-square-odd-ls, fermat-pos, fermat-for-rsa, fermat-2-mod, fermat-2, fermat-1-mod, fermat-1, ex-modeq-half, diff-primes-neg, diff-primes-dups, diff-primes, congmod-inverse-smallest, congmod-inverse-pos, congmod-inverse, congmod-def-mod-02, congmod-def-mod-01, cong-mult, Shor-algorithm, RSA-decrypt-ij-vars, Lagrange-SumOf4Squares-primes,
• int-abs/lels-01 is used by range-cong-dups, mod-rec-any, mod-rec, mod-neg, mod-mod, mod-ex-div, mod-abs-pos, lagrange-lemma, four-square-odd-ls, fermat-pos, fermat-for-rsa, ex-modeq-half, div-mod-eq, diff-primes-neg, diff-primes-dups, diff-primes, congmod-inverse-smallest, congmod-inverse-pos, congmod-inverse, congmod-def-mod-02, congmod-def-mod-01, Shor-algorithm, RSA-decrypt-ij-vars, Diffie-Hellman,
• int-abs/lels-02 is used by mod-zero-neg, mod-zero, mod-mult-add, four-square-odd-ls, fermat-1, ex-modeq-half, diff-primes-neg, diff-primes, congmod-inverse-smallest, Shor-algorithm, RSA-decrypt-ij-vars, Lagrange-SumOf4Squares,
• int-abs/lels-03 is used by mod-rec-neg, mod-pos, mod-mult-add, mod-le-same, lagrange-lemma-smallest, four-square-mod-zero, fermat-pos, ex-modeq-half, diff-primes-neg, diff-primes, RSA-decrypt-ij-vars,
• int-abs/lenls is used by mod-rec-neg, mod-rec, mod-neg, lagrange-lemma, four-square-odd-ls, ex-modeq-half, diff-primes-neg, diff-primes, congmod-inverse-pos, congmod-inverse, congmod-def-mod-02, RSA-decrypt-ij-vars, Lagrange-SumOf4Squares-primes,
• int-abs/leone is used by lagrange-lemma, fermat-pos, fermat-for-rsa, congmod-inverse-smallest,
• int-abs/lep is used by mod-rec, mod-le-same, ex-modeq-half,
• int-abs/lep-01 is used by mod-rec-any, lagrange-lemma, ex-modeq-half, diff-primes-neg, diff-primes,
• int-abs/ler is used by mod-mult-add, diff-primes-dups,
• int-abs/les is used by mod-mult-add,
• int-abs/lsone is used by mod-zero-neg, mod-rec-neg, mod-neg, mod-ex-div, four-square-mod-zero, Shor-algorithm, RSA-decrypt-ij-vars,
• int-abs/minus-02 is used by RSA-decrypt-ij-vars,
• int-abs/minus-add is used by diff-primes-neg, congmod-inverse,
• int-abs/minus-neg is used by lagrange-lemma, Shor-algorithm,
• int-abs/minus-sub is used by mod-rec-any, mod-neg, ex-modeq-half, cong-neg,
• int-abs/mone-05 is used by mod-rec-neg, mod-mult-add, lagrange-lemma,
• int-abs/mone-06 is used by mod-pot-pot, mod-mult-add, four-square-odd-ls, fermat-pos, ex-modeq-half, diff-primes-neg, diff-primes, congmod-inverse, cong-crt, RSA-decrypt-ij-vars, Lagrange-SumOf4Squares-primes,
• int-abs/mone-08 is used by ex-modeq-half,
• int-abs/neg is used by fermat-1, ex-modeq-half,
• int-abs/neg-02 is used by congmod-inverse,
• int-abs/neg-03 is used by mod-rec-any, mod-abs-neg-neg,
• int-abs/neg-05 is used by mod-neg,
• int-abs/neg-06 is used by mod-rec-any, four-square-mod-zero, ex-modeq-half,
• int-abs/neg-07 is used by mod-rec-neg,
• int-abs/neg-10 is used by mod-zero-04,
• int-abs/neg-12 is used by mod-neg,
• int-abs/neg-13 is used by mod-zero-neg, mod-rec-neg, mod-neg, mod-ex-div,
• int-abs/neg-15 is used by mod-neg, mod-mult-law, mod-add-law, mod-abs-pos, congmod-def-mod-02, RSA-decrypt-ij-vars,
• int-abs/negeq is used by congmod-inverse,
• int-abs/negle-07 is used by mod-neg,
• int-abs/numadd-01 is used by four-square-odd-ls, diff-primes-neg, diff-primes, congmod-inverse,
• int-abs/numle-02 is used by mod-pot-pot, fermat-pos, diff-primes-neg, diff-primes, RSA-decrypt-ij-vars,
• int-abs/numle-03 is used by mod-rec-neg, mod-mult-add, lagrange-lemma, diff-primes-neg, diff-primes-dups, diff-primes, Shor-algorithm,
• int-abs/numleledel-01 is used by mod-pot-pot, fermat-pos, Shor-algorithm, Lagrange-SumOf4Squares-primes,
• int-abs/numlelsdel-01 is used by congmod-inverse-pos, congmod-inverse, Shor-algorithm, RSA-decrypt-ij-vars,
• int-abs/numls-02 is used by mod-pot-pot, mod-mult-add, four-square-odd-ls, fermat-pos, ex-modeq-half, cong-crt, RSA-decrypt-ij-vars,
• int-abs/numls-03 is used by mod-rec-neg, ex-modeq-half, diff-primes-dups, Shor-algorithm, RSA-decrypt-ij-vars,
• int-abs/numlsledel-01 is used by diff-primes-dups, Shor-algorithm,
• int-abs/numsub is used by diff-primes-neg, diff-primes-dups, diff-primes, cong-crt,
• int-abs/sub-add is used by mod-plus, mod-mult-add, ex-modeq-half, congmod-mod-abs,
• int-abs/sub-add-01 is used by mod-neg, mod-add-law, lagrange-primedivisors, four-square-divides-all, diff-primes-neg, diff-primes-dups, diff-primes, congmod-def-mod, cong-mult-rew, Shor-algorithm, Lagrange-SumOf4Squares-primes,
• int-abs/sub-add-06 is used by four-square-divides-all, cong-same-add,
• int-abs/sub-eq is used by mod-rec-any, mod-neg, mod-mult-law, mod-mult-add, mod-add-law, mod-abs-pos, mod-abs-neg-neg, four-square-divides-all, four-square-congmod, ex-modeq-half, diff-primes-neg, diff-primes, congmod-inverse, congmod-def-mod-02, congmod-def-mod, cong-zero, cong-neg, cong-mult-rew, cong-crt-01, cong-crt, Shor-algorithm, RSA-decrypt-ij-vars,
• int-abs/sub-eq-01 is used by lagrange-lemma, fermat-for-rsa, fermat-2-mod, Shor-algorithm, RSA-decrypt-ij-vars,
• int-abs/sub-le is used by fermat-for-rsa, ex-modeq-half, RSA-decrypt-ij-vars,
• int-abs/sub-le-01 is used by mod-rec-neg, mod-rec-any, lagrange-lemma, fermat-pos, fermat-for-rsa, ex-modeq-half, diff-primes-neg, diff-primes-dups, diff-primes, RSA-decrypt-ij-vars,
• int-abs/sub-ls is used by mod-rec-neg, mod-rec-any, ex-modeq-half, Shor-algorithm,
• int-abs/sub-ls-01 is used by mod-rec-any, mod-mult-add, lagrange-lemma, fermat-pos, RSA-decrypt-ij-vars,
• int-abs/sub-minus is used by cong-neg,
• int-abs/sub-pred is used by mod-pot-pot, fermat-2,
• int-abs/sub-sub is used by mod-add-law, lagrange-primedivisors, lagrange-lemma, diff-primes-neg, Shor-algorithm, Lagrange-SumOf4Squares-primes,
• int-abs/sub-sub-03 is used by cong-same,
• int-abs/sub-sub-04 is used by diff-primes-neg,
• int-abs/sub-zero-01 is used by four-square-congmod, ex-modeq-half, diff-primes-neg, diff-primes, Shor-algorithm, Lagrange-SumOf4Squares-primes,
• int-abs/subneg is used by fermat-1,
• int-abs/subsub is used by mod-add-law, congmod-inverse,
• int-abs/succ-01 is used by mod-rec-neg, lagrange-lemma, fermat-pos,
• int-abs/succ-02 is used by mod-rec-neg, mod-mult-add, fermat-pos, ex-modeq-half, diff-primes-neg, diff-primes-dups, diff-primes,
• int-abs/zero-gels-01 is used by mod-zero-neg, mod-rec-neg, mod-rec-any, mod-pos, mod-neg, mod-mult-add, mod-ex-div, mod-abs-pos, mod-abs-neg-neg, lagrange-lemma, fermat-1, ex-modeq-half, diff-primes-dups, congmod-inverse-pos, congmod-inverse, congmod-def-mod-02, congmod-def-mod-01, RSA-decrypt-ij-vars,
• int-abs/zero-gels-03 is used by mod-zero-neg, mod-rec-neg, mod-neg, mod-ex-div, ex-modeq-half,
• int-abs/zero-gels-04 is used by rem-mod-pos, mod-zero, mod-rec-neg, mod-rec, mod-pot-pot, mod-neg, mod-i2n, mod-ex-div, mod-crt, lagrange-lemma, ex-modeq-half, diff-primes-neg, diff-primes-dups, diff-primes, congmod-inverse-smallest, congmod-inverse-pos, congmod-inverse, RSA-decrypt-ij-vars, Diffie-Hellman,

Used from specification int-fac

• int-fac/Binom-theorem is used by fermat-pos,
• int-fac/binomlist-def2 is used by fermat-pos,
• int-fac/coef-gcd is used by fermat-pos,
• int-fac/divides-sum is used by fermat-pos,
• int-fac/prime-divides-pot-01 is used by fermat-for-rsa,
• int-fac/coef-same is used by fermat-pos,
• int-fac/coef-zero is used by fermat-pos,
• int-fac/prime-divides-pot-01 is used by fermat-pos,

Used from specification list-data

• list-data/intlista/l is used by range-cong-dups, diff-primes-neg, diff-primes,

Used from specification int-min

• int-min/even-add is used by even-sum,
• int-min/even-def is used by Lagrange-SumOf4Squares-primes,
• int-min/even-def-mod is used by Shor-algorithm,
• int-min/even-odd-rew is used by Lagrange-SumOf4Squares-primes,
• int-min/odd-add is used by even-sum,
• int-min/odd-def is used by four-square-odd-ls, ex-modeq-half,
• int-min/odd-even-rew is used by Lagrange-SumOf4Squares-primes,
• int-min/even-mult is used by Lagrange-SumOf4Squares-primes,
• int-min/not-even-mod2 is used by Lagrange-SumOf4Squares-primes,
• int-min/odd-two is used by fermat-1,
• int-min/odd-zero is used by ex-modeq-half,

Used from specification list

• list/intlista/a is used by lagrange-primedivisors, fermat-pos, diff-primes-dups,
• list/intlista/c is used by lagrange-primedivisors,
• list/intlista/e is used by diff-primes-neg, diff-primes,
• list/intlista/in-17 is used by lagrange-primedivisors,
• list/intlista/in-append is used by lagrange-primedivisors, diff-primes-dups,
• list/intlista/in-empty is used by lagrange-primedivisors,
• list/intlista/len is used by diff-primes-dups,

Used from specification nat-basic2

• nat-basic2/a is used by mod-pot-pot, diff-primes-neg, diff-primes-dups, diff-primes,
• nat-basic2/c is used by mod-pot-pot, diff-primes-neg, diff-primes-dups, diff-primes,
• nat-basic2/s is used by mod-pot-pot, diff-primes-neg, diff-primes,
• nat-basic2/succ is used by diff-primes-neg, diff-primes,

Used from specification list-dup

• list-dup/intlista/a is used by diff-primes-dups,

Used from specification intnat

• intnat/i2n-mod is used by mod-i2n,
• intnat/num-i2n-ls-02 is used by diff-primes-neg, diff-primes,
• intnat/abs-02 is used by diff-primes-neg, diff-primes,
• intnat/abs-pred is used by mod-mult-add, fermat-pos,
• intnat/abs-succ-01 is used by mod-mult-add,
• intnat/abs-succ-03 is used by diff-primes-neg, diff-primes,
• intnat/abs-zero is used by diff-primes-neg, diff-primes,
• intnat/ini2-abs is used by diff-primes-dups,
• intnat/inj is used by diff-primes-neg, diff-primes,
• intnat/labs is used by mod-pot-pot, lagrange-lemma-smallest,
• intnat/n2i-add is used by diff-primes-dups,
• intnat/nat2int is used by diff-primes-neg, diff-primes,
• intnat/nat2int-04 is used by diff-primes-neg, diff-primes,
• intnat/nat2int-08 is used by diff-primes-neg, diff-primes,
• intnat/nat2int-10 is used by diff-primes-neg, diff-primes,
• intnat/num-n2i-ls-02 is used by range-cong-dups, diff-primes-neg, diff-primes,
• intnat/rax-04 is used by mod-pot-pot,

Used from specification oelem

• oelem/intlista/irreflexivity is used by mod-pot-pot,
• oelem/intlista/lel is used by mod-zero-neg, mod-zero-04, mod-rec-neg, mod-rec-any, mod-pot-pot, mod-neg, lagrange-lemma, four-square-divides-all, fermat-for-rsa, ex-modeq-half, diff-primes-neg, diff-primes, congmod-inverse-smallest, congmod-inverse-pos, congmod-inverse, Shor-algorithm, RSA-decrypt-ij-vars, Lagrange-SumOf4Squares-primes,
• oelem/intlista/transitivity is used by range-cong-dups, mod-zero-neg, mod-rec-neg, mod-rec-any, mod-pos, mod-neg, mod-ex-div, mod-abs-neg-div, lagrange-lemma-smallest, lagrange-lemma, four-square-mod-zero, four-square-divides-all, fermat-1, ex-modeq-half, congmod-inverse-pos, congmod-inverse, Shor-algorithm, RSA-decrypt-ij-vars, Lagrange-SumOf4Squares-primes, Diffie-Hellman,

Used from specification int-basic2

• int-basic2/pls-01 is used by lagrange-lemma,
• int-basic2/add-a is used by rem-mod-pos, mod-zero-neg, mod-zero, mod-rec-plus, mod-rec-neg, mod-rec-any, mod-rec, mod-pot-pot, mod-pos, mod-plus, mod-neg, mod-mult-law, mod-mult-add-01, mod-mult-add, mod-mult-04, mod-mult, mod-le-same, mod-ex-div, mod-add-law, mod-abs-pos, mod-abs-neg-neg, lagrange-primedivisors, lagrange-lemma-smallest, lagrange-lemma, four-square-odd-ls, four-square-mod-zero, four-square-divides-all, four-square-congmod, fermat-pos, fermat-for-rsa, fermat-1, ex-modeq-half, even-sum, div-mod-eq, diff-primes-neg, diff-primes-dups, diff-primes, congmod-mod-abs, congmod-inverse-smallest, congmod-inverse, congmod-def-mod-02, congmod-def-mod, cong-zero, cong-same-add, cong-neg, cong-mult-rew, cong-mult, cong-crt-01, cong-crt, cong-add, Shor-algorithm, RSA-decrypt-ij-vars, Lagrange-SumOf4Squares-primes, Lagrange-SumOf4Squares,
• int-basic2/add-c is used by rem-mod-pos, mod-zero-neg, mod-zero, mod-rec-plus, mod-rec-neg, mod-rec-any, mod-rec, mod-pot-pot, mod-pos, mod-plus, mod-neg, mod-mult-law, mod-mult-add-01, mod-mult-add, mod-mult-04, mod-mult, mod-le-same, mod-ex-div, mod-add-law, mod-abs-pos, mod-abs-neg-neg, lagrange-primedivisors, lagrange-lemma-smallest, lagrange-lemma, four-square-odd-ls, four-square-mod-zero, four-square-divides-all, four-square-congmod, fermat-pos, fermat-for-rsa, fermat-1, ex-modeq-half, even-sum, div-mod-eq, diff-primes-neg, diff-primes-dups, diff-primes, congmod-mod-abs, congmod-inverse-smallest, congmod-inverse, congmod-def-mod-02, congmod-def-mod, cong-zero, cong-same-add, cong-neg, cong-mult-rew, cong-mult, cong-crt-01, cong-crt, cong-add, Shor-algorithm, RSA-decrypt-ij-vars, Lagrange-SumOf4Squares-primes, Lagrange-SumOf4Squares,
• int-basic2/add-in is used by mod-zero-neg, mod-rec-neg, mod-mult-law, mod-mult-add, mod-ex-div, mod-add-law, four-square-divides-all, ex-modeq-half, diff-primes-neg, diff-primes, congmod-def-mod-02, congmod-def-mod, cong-mult, cong-crt-01, Lagrange-SumOf4Squares-primes,
• int-basic2/add-less is used by mod-zero-neg, mod-rec-neg, mod-neg, mod-ex-div,
• int-basic2/add-zero is used by mod-zero-neg, mod-rec-neg, mod-rec-any, mod-neg, mod-mult-add, mod-mult-04, mod-mult, mod-abs-neg-neg, four-square-odd-ls, ex-modeq-half, diff-primes-neg, diff-primes, congmod-def-mod-02, cong-zero, cong-crt-01, cong-crt, RSA-decrypt-ij-vars,
• int-basic2/eq is used by mod-zero-neg, mod-zero, mod-neg, mod-ex-div,
• int-basic2/ls is used by mod-rec-neg, mod-rec-any, mod-neg, ex-modeq-half, diff-primes-neg, diff-primes,
• int-basic2/ls-01 is used by mod-rec-neg, mod-neg, mod-ex-div, diff-primes-neg, diff-primes,
• int-basic2/ls-02 is used by mod-zero-neg, ex-modeq-half,
• int-basic2/lst-04 is used by mod-rec-neg,
• int-basic2/num-between is used by Lagrange-SumOf4Squares-primes,
• int-basic2/pred is used by RSA-decrypt-ij-vars,
• int-basic2/zero is used by congmod-def-mod-02,
• int-basic2/zero-02 is used by fermat-pos,
• int-basic2/zero-04 is used by congmod-inverse,

Used from specification nat-basic1

• nat-basic1/f is used by range-cong-dups, diff-primes-neg, diff-primes,
• nat-basic1/lf is used by diff-primes-neg, diff-primes,
• nat-basic1/lf-02 is used by diff-primes-neg, diff-primes,
• nat-basic1/one is used by range-cong-dups, diff-primes-neg, diff-primes,
• nat-basic1/trans-1 is used by diff-primes-neg, diff-primes,
• nat-basic1/zero is used by range-cong-dups, diff-primes-neg, diff-primes,

Used from specification int-div

• int-div/div-add1-pospos is used by four-square-odd-ls,
• int-div/div2zero is used by Shor-algorithm,
• int-div/divmult is used by lagrange-lemma, diff-primes-neg, diff-primes-dups, diff-primes,
• int-div/mod-abs is used by congmod-def-mod-02, congmod-def-mod-01,
• int-div/mod-mult-neg-03 is used by mod-rec-neg,
• int-div/mod-neq-02 is used by ex-modeq-half,
• int-div/mod-ngez is used by ex-modeq-half,
• int-div/mod-zero-05 is used by mod-rec-neg, ex-modeq-half, diff-primes-neg, diff-primes, congmod-inverse-smallest,
• int-div/modex is used by mod-rec-neg, mod-abs-neg-div, ex-modeq-half,
• int-div/num-ls is used by lagrange-lemma,
• int-div/abs is used by lagrange-lemma,
• int-div/div-elim-negneg is used by mod-ex-div,
• int-div/div-elim-negpos is used by mod-zero-neg, mod-rec-neg, mod-neg, mod-ex-div, congmod-inverse,
• int-div/div-elim-pospos is used by rem-mod-pos, mod-zero, mod-rec, congmod-inverse,
• int-div/div-lezero is used by Lagrange-SumOf4Squares-primes,
• int-div/div-ls-mone is used by diff-primes-neg, diff-primes-dups, diff-primes,
• int-div/div-ls-zero is used by Shor-algorithm,
• int-div/div-mult-num is used by four-square-odd-ls, Lagrange-SumOf4Squares-primes,
• int-div/div-two is used by ex-modeq-half,
• int-div/div-two-zero-01 is used by lagrange-lemma, diff-primes-neg, diff-primes-dups, diff-primes, Shor-algorithm, Lagrange-SumOf4Squares-primes,
• int-div/div2-neg is used by ex-modeq-half,
• int-div/div2-nle is used by Lagrange-SumOf4Squares-primes,
• int-div/divmod-rew is used by mod-ex-div, div-mod-eq,
• int-div/divmult is used by Shor-algorithm,
• int-div/mod-add is used by mod-rec,
• int-div/mod-grz is used by mod-neg,
• int-div/mod-grz-02 is used by mod-abs-neg-neg,
• int-div/mod-les is used by mod-le-same,
• int-div/mod-less-01 is used by mod-zero-neg, mod-rec-neg, mod-neg, mod-ex-div, ex-modeq-half, diff-primes-neg, diff-primes,
• int-div/mod-ls-same-01 is used by congmod-def-mod-01, Shor-algorithm,
• int-div/mod-lsz is used by mod-pos, ex-modeq-half,
• int-div/mod-mult-04 is used by mod-mult, mod-abs-neg-div,
• int-div/mod-mult-pos is used by mod-rec,
• int-div/mod-neg is used by mod-abs-pos, mod-abs-neg-neg, mod-abs-neg-div,
• int-div/mod-neg-01 is used by mod-neg, mod-mult-04, congmod-inverse,
• int-div/mod-neq is used by ex-modeq-half, congmod-def-mod-02,
• int-div/mod-neq-01 is used by mod-neg,
• int-div/mod-ngez is used by mod-zero-neg, mod-rec-neg, mod-neg,
• int-div/mod-ngez-01 is used by mod-abs-neg-neg, congmod-def-mod-02,
• int-div/mod-one is used by mod-one,
• int-div/mod-same is used by mod-mult-04,
• int-div/mod-two-02 is used by four-square-odd-ls,
• int-div/mod-two-06 is used by Shor-algorithm,
• int-div/mod-zero is used by mod-zero, mod-rec, mod-i2n, congmod-inverse-smallest,
• int-div/mod-zero-04 is used by mod-zero-01,
• int-div/mod-zero-06 is used by mod-ex-div, mod-abs-pos, congmod-def-mod-01,
• int-div/mod-zero-09 is used by congmod-def-mod-01,
• int-div/modmod is used by ex-modeq-half,
• int-div/nummult-ls-02 is used by Lagrange-SumOf4Squares-primes,
• int-div/one-01 is used by congmod-inverse-smallest, congmod-def-mod-01,

Used from specification list-del

• list-del/intlista/dups-def is used by range-cong-dups, diff-primes-neg, diff-primes,
• list-del/intlista/get-nodups is used by range-cong-dups,

Used from specification list-set

• list-set/intlista/dups-app is used by lagrange-lemma,
• list-set/intlista/filter-empty-def is used by lagrange-lemma,