Used simplifier rules/spec theorems by specification

Used from specification nat-basic

• nat-basic/addex is used by rounded-help2, between-is-aligned,
• nat-basic/a is used by rounded-help2, rounded-help, is-aligned-still-space, is-aligned-pad, is-aligned-of-mod, is-aligned-not-multiples, is-aligned-multiple-1, is-aligned-multiple, is-aligned-mod-alignment, is-aligned-minus, is-aligned-is-aligned-mod, is-aligned-elim, is-aligned-align-up-multiple, is-aligned-add-diff-ls, is-aligned-add, eq1, div-mult-to-diff-mod, between-is-aligned, alignup-upper-bound-01, alignup-upper-bound, alignup-lower-bound, alignup-le-is-aligned, alignup-le, alignup-isnot-smaller, alignup-is-even-bigger, alignup-is-bigger, alignup-is-aligned, alignup-div-mult, alignup-calc, alignup-add-mult, alignup-add-le, alignup-add-bounded1, aligndown-sub-add-sub, aligndown-same-equiv, aligndown-remainder, aligndown-plus-remainder, aligndown-le, aligndown-is-zero, aligndown-is-n, aligndown-is-aligned-add, aligndown-eq-add, aligndown-aligndown-add, aligndown-add-same0, aligndown-add-same, aligndown-add-not-smaller, aligndown-add-n-alignup, aligndown-add-n, align-down-add-to-align-up, align-down-add-ls, align-down-add-eq-add-ls, align-down-add-eq, add-n-aligndown,
• nat-basic/add-base is used by rounded-help, is-aligned-of-mod, is-aligned-not-multiples, is-aligned-multiple-1, is-aligned-multiple, is-aligned-mod-alignment, is-aligned-is-aligned-mod, is-aligned-elim, is-aligned-align-up-multiple, eq1, alignup-upper-bound, alignup-le-is-aligned, alignup-le, alignup-add-le, alignup-add-bounded1, aligndown-is-n, aligndown-eq-add, aligndown-add-same0, aligndown-add-same, aligndown-add-not-smaller, align-down-add-ls, align-down-add-eq,
• nat-basic/c is used by rounded-help2, rounded-help, is-aligned-still-space, is-aligned-pad, is-aligned-of-mod, is-aligned-not-multiples, is-aligned-multiple-1, is-aligned-multiple, is-aligned-mod-alignment, is-aligned-minus, is-aligned-is-aligned-mod, is-aligned-elim, is-aligned-align-up-multiple, is-aligned-add-diff-ls, is-aligned-add-diff-le, is-aligned-add, eq1, div-mult-to-diff-mod, between-is-aligned, alignup-upper-bound-01, alignup-upper-bound, alignup-lower-bound, alignup-le-is-aligned, alignup-le, alignup-isnot-smaller, alignup-is-even-bigger, alignup-is-bigger, alignup-is-aligned, alignup-div-mult, alignup-calc, alignup-add-mult, alignup-add-le, alignup-add-bounded1, aligndown-sub-add-sub, aligndown-same-equiv, aligndown-remainder, aligndown-plus-remainder, aligndown-le, aligndown-is-zero, aligndown-is-n, aligndown-is-aligned-add, aligndown-eq-add, aligndown-aligndown-add, aligndown-add-same0, aligndown-add-same, aligndown-add-not-smaller, aligndown-add-n-alignup, aligndown-add-n, align-down-add-to-align-up, align-down-add-ls, align-down-add-eq-add-ls, align-down-add-eq, add-n-aligndown,
• nat-basic/eq-01 is used by div-mult-to-diff-mod, alignup-div-mult, alignup-add-mult, aligndown-sub-add-sub, aligndown-is-aligned-add, aligndown-aligndown-add, aligndown-add-same, aligndown-add-n-alignup, align-down-add-to-align-up, align-down-add-eq-add-ls, align-down-add-eq, add-n-aligndown,
• nat-basic/eq-02 is used by alignup-le-is-aligned, alignup-add-bounded1, aligndown-remainder, aligndown-plus-remainder, aligndown-eq-add, aligndown-add-same0, align-down-add-eq,
• nat-basic/eqs is used by aligndown-remainder,
• nat-basic/f is used by rounded-help2, rounded-help, is-aligned-still-space, is-aligned-pad, is-aligned-of-mod, is-aligned-mod-alignment, is-aligned-ls-eq-zero, is-aligned-is-aligned-mod, is-aligned-elim, is-aligned-add-diff-ls, eq1, between-is-aligned, alignup-upper-bound-01, alignup-upper-bound, alignup-lower-bound, alignup-le-is-aligned, alignup-le, alignup-is-even-bigger, alignup-is-bigger, alignup-add-le, alignup-add-bounded1, aligndown-not-smaller, aligndown-le, aligndown-is-smaller-01, aligndown-is-smaller, aligndown-is-n, aligndown-eq-add, aligndown-add-same0, aligndown-add-same, aligndown-add-not-smaller, aligndown-add-n, align-down-ls-zero, align-down-add-ls, align-down-add-eq-add-ls, align-down-add-eq,
• nat-basic/l is used by rounded-help2, between-is-aligned, alignup-lower-bound, alignup-le-is-aligned, alignup-le, align-down-add-ls,
• nat-basic/l-01 is used by between-is-aligned, alignup-le, aligndown-add-same, align-down-add-ls,
• nat-basic/l-02 is used by alignup-is-even-bigger, alignup-add-le, aligndown-add-not-smaller, align-down-add-ls,
• nat-basic/l-05 is used by align-down-add-eq-add-ls,
• nat-basic/lf is used by between-is-aligned, aligndown-is-n, align-down-add-ls,
• nat-basic/lf-01 is used by eq1, aligndown-is-n, aligndown-add-same, align-down-add-ls, align-down-add-eq-add-ls,
• nat-basic/lf-02 is used by alignup-upper-bound, alignup-le-is-aligned, alignup-le, aligndown-is-n, aligndown-add-same0, aligndown-add-same, align-down-add-eq-add-ls,
• nat-basic/ls-02 is used by alignup-lower-bound, alignup-le-is-aligned, alignup-le, alignup-is-bigger, align-down-add-eq-add-ls,
• nat-basic/one is used by between-is-aligned, aligndown-is-n,
• nat-basic/one-03 is used by aligndown-is-n,
• nat-basic/oz is used by eq1,
• nat-basic/ref is used by eq1, alignup-upper-bound, alignup-le-is-aligned, alignup-is-bigger, aligndown-is-smaller-01, aligndown-is-smaller,
• nat-basic/s-04 is used by rounded-help, is-aligned-still-space, eq1, alignup-upper-bound, alignup-le-is-aligned, alignup-le,
• nat-basic/succ is used by rounded-help, is-aligned-align-up-multiple, eq1, between-is-aligned, alignup-upper-bound-01, alignup-upper-bound, alignup-lower-bound, alignup-le-is-aligned, alignup-le, alignup-isnot-smaller, alignup-is-even-bigger, alignup-is-bigger, alignup-is-aligned, alignup-div-mult, alignup-calc, alignup-add-mult, alignup-add-le, alignup-add-bounded1, aligndown-is-n, aligndown-add-n-alignup, align-down-add-to-align-up, align-down-add-ls,
• nat-basic/trans is used by between-is-aligned, align-down-add-ls,
• nat-basic/twols-02 is used by aligndown-is-n,
• nat-basic/z-01 is used by is-aligned-is-aligned-mod, aligndown-is-zero, aligndown-eq-add, aligndown-add-same0, align-down-add-ls,
• nat-basic/zero is used by rounded-help, is-aligned-of-mod, is-aligned-ls-eq-zero, is-aligned-is-aligned-mod, is-aligned-elim, is-aligned-aligndown-zero, eq1, alignup-upper-bound, aligndown-add-not-smaller, align-down-add-ls, align-down-add-eq,
• nat-basic/zero-01 is used by is-aligned-is-aligned-mod, alignup-upper-bound-01, alignup-le-is-aligned, aligndown-add-same0, aligndown-add-same, align-down-add-ls,

Used from specification nat

• nat/anti is used by alignup-add-bounded1,
• nat/le-addex is used by aligndown-is-zero,
• nat/anti is used by alignup-upper-bound, alignup-le-is-aligned, alignup-le, alignup-add-bounded1,
• nat/cancel-01 is used by aligndown-sub-add-sub,
• nat/elim-sub is used by is-aligned-multiple, is-aligned-minus, is-aligned-add-diff-le, div-mult-to-diff-mod, alignup-le-is-aligned, alignup-le, aligndown-sub-add-sub, aligndown-remainder, aligndown-is-n,
• nat/eq-01 is used by eq1, aligndown-is-zero,
• nat/eq-02 is used by rounded-help, eq1, div-mult-to-diff-mod, aligndown-sub-add-sub, aligndown-remainder, aligndown-plus-remainder,
• nat/eqle-one is used by eq1,
• nat/fle is used by alignup-lower-bound, alignup-le, alignup-is-even-bigger, aligndown-not-smaller, aligndown-add-same, align-down-add-ls,
• nat/fle-01 is used by rounded-help2, alignup-upper-bound, alignup-le-is-aligned, alignup-le, alignup-add-le, aligndown-is-smaller, aligndown-is-n,
• nat/ge is used by alignup-upper-bound, alignup-lower-bound,
• nat/gr-def is used by eq1,
• nat/le-add is used by alignup-add-le, aligndown-le, aligndown-add-n, align-down-add-ls,
• nat/le-def is used by rounded-help, is-aligned-le-eq-zero, eq1, alignup-upper-bound, alignup-lower-bound, alignup-is-bigger, aligndown-is-smaller-01,
• nat/le-ls-simp is used by alignup-le, aligndown-add-same,
• nat/le-one is used by rounded-help, eq1,
• nat/lels is used by rounded-help2, rounded-help, is-aligned-still-space, eq1, alignup-upper-bound, alignup-le-is-aligned, alignup-le, aligndown-is-zero, aligndown-is-smaller, aligndown-add-same, align-down-add-ls,
• nat/lels-02 is used by rounded-help, alignup-add-bounded1, aligndown-is-n,
• nat/lep is used by eq1, aligndown-sub-add-sub, aligndown-is-zero, align-down-add-ls,
• nat/lep-02 is used by rounded-help, alignup-upper-bound-01, alignup-add-le, aligndown-add-n,
• nat/ler is used by alignup-le-is-aligned, alignup-le, alignup-add-le, aligndown-le,
• nat/les is used by eq1,
• nat/let is used by alignup-le-is-aligned, alignup-le, alignup-is-even-bigger,
• nat/lez is used by alignup-upper-bound-01, align-down-add-ls,
• nat/lez-01 is used by rounded-help, is-aligned-le-eq-zero, is-aligned-aligndown-zero-ls, eq1, aligndown-is-zero, align-down-add-ls,
• nat/ls-le-simp is used by is-aligned-still-space, alignup-upper-bound-01, alignup-lower-bound, alignup-le-is-aligned, alignup-le, alignup-isnot-smaller, aligndown-not-smaller, aligndown-add-n,
• nat/prop-07 is used by is-aligned-add-diff-ls,
• nat/succ-01 is used by eq1,
• nat/zero is used by alignup-le, aligndown-sub-add-sub,

Used from specification nat-mult

• nat-mult/dist is used by rounded-help2, is-aligned-still-space, aligndown-is-aligned-add, aligndown-aligndown-add, align-down-add-ls,
• nat-mult/coef-04 is used by alignup-add-mult, aligndown-aligndown-add,
• nat-mult/coef-10 is used by rounded-help,
• nat-mult/coef-17 is used by add-n-aligndown,
• nat-mult/coef-18 is used by eq1,
• nat-mult/coef-21 is used by is-aligned-still-space, alignup-upper-bound, alignup-le-is-aligned, alignup-le,
• nat-mult/eq is used by is-aligned-elim, alignup-multiplier, aligndown-multiplier,
• nat-mult/ls-01 is used by rounded-help2,
• nat-mult/ls-02 is used by is-aligned-still-space, alignup-le, aligndown-is-n, aligndown-add-not-smaller, align-down-add-ls,
• nat-mult/ls-04 is used by aligndown-is-n,
• nat-mult/ls-08 is used by aligndown-is-n, align-down-add-ls,
• nat-mult/modeq is used by aligndown-add-same0, aligndown-add-same,
• nat-mult/modeq-01 is used by is-aligned-is-aligned-mod, aligndown-same-equiv, align-down-add-ls,
• nat-mult/mult-a is used by rounded-help2, rounded-help, is-aligned-still-space, is-aligned-pad, is-aligned-of-mod, is-aligned-not-multiples, is-aligned-multiplier, is-aligned-multiple-1, is-aligned-multiple, is-aligned-mod-alignment, is-aligned-is-aligned-mod, is-aligned-elim, is-aligned-align-up-multiple, is-aligned-align-down, eq1, div-mult-to-diff-mod, alignup-upper-bound-01, alignup-upper-bound, alignup-multiplier, alignup-lower-bound, alignup-le-is-aligned, alignup-le, alignup-isnot-smaller, alignup-is-even-bigger, alignup-is-bigger, alignup-is-aligned, alignup-div-mult, alignup-calc, alignup-add-mult, alignup-add-le, alignup-add-bounded1, aligndown-sub-add-sub, aligndown-same-equiv, aligndown-remainder, aligndown-plus-remainder, aligndown-not-smaller, aligndown-multiplier, aligndown-is-zero, aligndown-is-smaller-01, aligndown-is-smaller, aligndown-is-n, aligndown-is-aligned-add, aligndown-is-aligned, aligndown-aligndown-add, aligndown-add-same0, aligndown-add-same, aligndown-add-not-smaller, aligndown-add-n-alignup, align-down-ls-zero, align-down-add-to-align-up, align-down-add-ls, align-down-add-eq, add-n-aligndown,
• nat-mult/mult-c is used by rounded-help2, rounded-help, is-aligned-still-space, is-aligned-pad, is-aligned-of-mod, is-aligned-not-multiples, is-aligned-multiplier, is-aligned-multiple-1, is-aligned-multiple, is-aligned-mod-alignment, is-aligned-is-aligned-mod, is-aligned-elim, is-aligned-align-up-multiple, is-aligned-align-down, eq1, div-mult-to-diff-mod, alignup-upper-bound-01, alignup-upper-bound, alignup-multiplier, alignup-lower-bound, alignup-le-is-aligned, alignup-le, alignup-isnot-smaller, alignup-is-even-bigger, alignup-is-bigger, alignup-is-aligned, alignup-div-mult, alignup-calc, alignup-add-mult, alignup-add-le, alignup-add-bounded1, aligndown-sub-add-sub, aligndown-same-equiv, aligndown-remainder, aligndown-plus-remainder, aligndown-not-smaller, aligndown-multiplier, aligndown-is-zero, aligndown-is-smaller-01, aligndown-is-smaller, aligndown-is-n, aligndown-is-aligned-add, aligndown-is-aligned, aligndown-aligndown-add, aligndown-add-same0, aligndown-add-same, aligndown-add-not-smaller, aligndown-add-n-alignup, align-down-ls-zero, align-down-add-to-align-up, align-down-add-ls, align-down-add-eq, add-n-aligndown,
• nat-mult/numeral-20 is used by rounded-help2,
• nat-mult/numeral-36 is used by aligndown-is-n,
• nat-mult/one is used by rounded-help2, is-aligned-not-multiples, eq1, aligndown-is-n,
• nat-mult/one-01 is used by is-aligned-not-multiples,
• nat-mult/rsucc-02 is used by rounded-help, is-aligned-align-up-multiple, eq1, alignup-upper-bound-01, alignup-upper-bound, alignup-lower-bound, alignup-le-is-aligned, alignup-le, alignup-isnot-smaller, alignup-is-even-bigger, alignup-is-bigger, alignup-is-aligned, alignup-div-mult, alignup-calc, alignup-add-mult, alignup-add-le, alignup-add-bounded1, aligndown-is-n, aligndown-add-n-alignup, align-down-add-to-align-up,
• nat-mult/two-02 is used by rounded-help2, rounded-help,
• nat-mult/zero is used by rounded-help, is-aligned-is-aligned-mod, alignup-upper-bound-01, alignup-le-is-aligned, alignup-add-bounded1, aligndown-is-zero, aligndown-add-same0, aligndown-add-same, align-down-ls-zero, align-down-add-ls,
• nat-mult/zero-01 is used by is-aligned-of-mod, align-down-add-ls,
• nat-mult/zero-02 is used by rounded-help2,
• nat-mult/zero-03 is used by is-aligned-not-multiples, aligndown-is-n,
• nat-mult/zero-06 is used by is-aligned-still-space, is-aligned-of-mod, is-aligned-not-multiples, is-aligned-multiple-1, is-aligned-mod-alignment, is-aligned-align-up-multiple, eq1, alignup-add-bounded1, aligndown-is-zero, aligndown-is-n, aligndown-add-not-smaller,

Used from specification nat-div

• nat-div/Divdef is used by alignup-le-is-aligned, alignup-le, alignup-is-bigger,
• nat-div/div-add is used by add-n-aligndown,
• nat-div/div-succ is used by rounded-help, eq1,
• nat-div/div-succ-01 is used by eq1,
• nat-div/mod-eq is used by is-aligned-still-space,
• nat-div/mod-rew is used by is-aligned-multiple, div-mult-to-diff-mod, alignup-le-is-aligned, alignup-le, aligndown-remainder, aligndown-plus-remainder, aligndown-is-n,
• nat-div/modex is used by is-aligned-still-space,
• nat-div/rax is used by rounded-help, eq1,
• nat-div/rec is used by eq1, aligndown-is-zero, aligndown-is-n,
• nat-div/cond is used by rounded-help, is-aligned-multiple, eq1, div-mult-to-diff-mod, alignup-le-is-aligned, alignup-le, alignup-is-bigger, aligndown-sub-add-sub, aligndown-remainder, aligndown-plus-remainder, aligndown-is-n,
• nat-div/cond-01 is used by aligndown-not-smaller, aligndown-is-smaller-01, aligndown-is-smaller,
• nat-div/div-add is used by aligndown-is-aligned-add, aligndown-aligndown-add, aligndown-add-not-smaller, align-down-add-eq,
• nat-div/div-elim is used by is-aligned-still-space, is-aligned-pad, is-aligned-of-mod, is-aligned-not-multiples, is-aligned-multiple-1, is-aligned-mod-alignment, is-aligned-is-aligned-mod, is-aligned-elim, is-aligned-align-up-multiple, alignup-upper-bound-01, alignup-upper-bound, alignup-lower-bound, alignup-calc, alignup-add-le, aligndown-same-equiv, aligndown-le, aligndown-eq-add, aligndown-add-same0, aligndown-add-same, aligndown-add-not-smaller, aligndown-add-n, align-down-add-ls, align-down-add-eq-add-ls, align-down-add-eq,
• nat-div/div-succ-01 is used by rounded-help,
• nat-div/le-div-to-mult is used by alignup-upper-bound, alignup-le-is-aligned, alignup-le,
• nat-div/ls-02 is used by alignup-le, aligndown-add-not-smaller,
• nat-div/mod-add is used by is-aligned-minus, is-aligned-add, between-is-aligned, aligndown-is-aligned-add, aligndown-aligndown-add, aligndown-add-not-smaller, align-down-add-eq,
• nat-div/mod-eq is used by is-aligned-of-mod, is-aligned-mod-alignment, is-aligned-ls-eq-zero, is-aligned-le-eq-zero, between-is-aligned, alignup-add-bounded1, aligndown-is-zero, align-down-ls-zero, align-down-add-ls, align-down-add-eq,
• nat-div/mod-le is used by div-mult-to-diff-mod, aligndown-sub-add-sub,
• nat-div/mod-ls is used by is-aligned-still-space,
• nat-div/mod-mult is used by is-aligned-still-space, is-aligned-pad, is-aligned-of-mod, is-aligned-mod-alignment, is-aligned-is-aligned-mod, alignup-is-aligned, alignup-add-mult, aligndown-aligndown-add, aligndown-add-not-smaller, align-down-add-ls,
• nat-div/mod-mult-01 is used by is-aligned-of-mod, is-aligned-multiplier, is-aligned-multiple-1, is-aligned-mod-alignment, is-aligned-align-up-multiple, is-aligned-align-down, alignup-upper-bound, alignup-multiplier, aligndown-multiplier, aligndown-is-aligned, align-down-add-eq,
• nat-div/mod-once is used by eq1, aligndown-is-zero, add-n-aligndown,
• nat-div/mod-zero is used by is-aligned-same, is-aligned-pad, is-aligned-not-multiples, is-aligned-add-diff-ls, is-aligned-add-diff-le, alignup-is-aligned, alignup-add-bounded1, add-n-aligndown,
• nat-div/mod-zero-01 is used by is-aligned-zero, alignup-add-bounded1, aligndown-is-zero,
• nat-div/mult is used by alignup-div-mult, alignup-add-mult, aligndown-aligndown-add, align-down-add-ls,
• nat-div/mult-div is used by alignup-div-mult, aligndown-is-aligned-add, aligndown-aligndown-add, align-down-add-eq,
• nat-div/mult-ls is used by aligndown-is-n,
• nat-div/one is used by eq1, alignup-div-mult, alignup-add-bounded1, add-n-aligndown,
• nat-div/zero is used by rounded-help, alignup-add-bounded1,
• nat-div/zero-01 is used by alignup-add-bounded1, aligndown-is-zero, align-down-ls-zero, align-down-add-ls, align-down-add-eq,