Used simplifier rules/spec theorems by specification

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,
• nat/fle-01 is used by rounded-help2, alignup-upper-bound, alignup-le-is-aligned, alignup-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 eq1, aligndown-le, aligndown-add-n,
• nat/le-ls-simp is used by alignup-lower-bound, alignup-le,
• nat/le-one is used by rounded-help, eq1,
• nat/lels is used by rounded-help2, rounded-help, eq1, alignup-upper-bound, alignup-le-is-aligned, alignup-le, aligndown-is-zero, aligndown-is-smaller,
• nat/lels-01 is used by rounded-help, eq1, alignup-upper-bound, alignup-lower-bound, alignup-is-bigger, aligndown-is-smaller-01,
• 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,
• nat/lep-02 is used by rounded-help, alignup-upper-bound-01, aligndown-add-n,
• nat/ler is used by alignup-le-is-aligned, alignup-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-01 is used by rounded-help, eq1, aligndown-is-zero,
• nat/ls-le-simp is used by alignup-upper-bound-01, alignup-isnot-smaller, aligndown-not-smaller, aligndown-add-n,
• nat/prop-07 is used by is-aligned-add-diff-ls,
• nat/zero is used by alignup-le, aligndown-sub-add-sub,

Used from specification nat-basic2

• nat-basic2/addex is used by rounded-help2, between-is-aligned,
• nat-basic2/a is used by rounded-help2, rounded-help, is-aligned-still-space, is-aligned-not-multiples, is-aligned-multiple-1, is-aligned-multiple, is-aligned-mod-alignment, is-aligned-minus, is-aligned-elim, 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-calc, alignup-add-mult, 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, add-n-aligndown,
• nat-basic2/add-base is used by rounded-help, is-aligned-not-multiples, is-aligned-multiple-1, is-aligned-multiple, is-aligned-mod-alignment, is-aligned-elim, eq1, alignup-upper-bound, alignup-le-is-aligned, alignup-le, alignup-add-bounded1, aligndown-is-n, aligndown-eq-add, aligndown-add-same0, aligndown-add-same, aligndown-add-not-smaller,
• nat-basic2/c is used by rounded-help2, rounded-help, is-aligned-still-space, is-aligned-not-multiples, is-aligned-multiple-1, is-aligned-multiple, is-aligned-mod-alignment, is-aligned-minus, is-aligned-elim, 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-calc, alignup-add-mult, 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, add-n-aligndown,
• nat-basic2/eq is used by alignup-le-is-aligned, alignup-add-bounded1, aligndown-remainder, aligndown-plus-remainder, aligndown-eq-add, aligndown-add-same0,
• nat-basic2/eq-01 is used by div-mult-to-diff-mod, alignup-add-mult, aligndown-sub-add-sub, aligndown-is-aligned-add, aligndown-aligndown-add, aligndown-add-same, aligndown-add-n-alignup, add-n-aligndown,
• nat-basic2/eqs is used by aligndown-remainder,
• nat-basic2/l is used by rounded-help2, between-is-aligned, alignup-lower-bound, alignup-le-is-aligned, alignup-le,
• nat-basic2/l-01 is used by between-is-aligned, alignup-le,
• nat-basic2/l-02 is used by alignup-is-even-bigger, aligndown-add-not-smaller,
• nat-basic2/one is used by aligndown-is-n,
• nat-basic2/oz is used by eq1, aligndown-is-zero,
• nat-basic2/s is used by rounded-help, is-aligned-still-space, eq1, alignup-upper-bound, alignup-le-is-aligned, alignup-le,
• nat-basic2/succ is used by rounded-help, 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-calc, alignup-add-mult, alignup-add-bounded1, aligndown-is-n, aligndown-add-n-alignup,
• nat-basic2/z-01 is used by aligndown-eq-add, aligndown-add-same0,

Used from specification nat-mult

• nat-mult/dist is used by rounded-help2, is-aligned-still-space, aligndown-is-aligned-add, aligndown-aligndown-add,
• nat-mult/coef-04 is used by alignup-add-mult, aligndown-aligndown-add,
• 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 rounded-help2, is-aligned-elim, alignup-multiplier, aligndown-multiplier, aligndown-add-same,
• nat-mult/eq-same is used by is-aligned-not-multiples, aligndown-is-n,
• nat-mult/leone is used by rounded-help,
• nat-mult/ls is used by is-aligned-still-space, alignup-le, aligndown-is-n, aligndown-add-not-smaller,
• nat-mult/ls-01 is used by rounded-help2,
• nat-mult/ls-04 is used by aligndown-is-n,
• nat-mult/ls-08 is used by aligndown-is-n,
• nat-mult/modeq is used by aligndown-add-same0, aligndown-add-same,
• nat-mult/modeq-01 is used by aligndown-same-equiv,
• nat-mult/mult-a is used by rounded-help2, rounded-help, is-aligned-still-space, is-aligned-not-multiples, is-aligned-multiplier, is-aligned-multiple-1, is-aligned-multiple, is-aligned-mod-alignment, is-aligned-elim, 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-calc, alignup-add-mult, 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, add-n-aligndown,
• nat-mult/mult-base is used by rounded-help, alignup-add-bounded1, aligndown-is-zero,
• nat-mult/mult-c is used by rounded-help2, rounded-help, is-aligned-still-space, is-aligned-not-multiples, is-aligned-multiplier, is-aligned-multiple-1, is-aligned-multiple, is-aligned-mod-alignment, is-aligned-elim, 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-calc, alignup-add-mult, 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, 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, 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-calc, alignup-add-mult, alignup-add-bounded1, aligndown-is-n, aligndown-add-n-alignup,
• nat-mult/two-02 is used by rounded-help2, rounded-help,
• nat-mult/two-zero-01 is used by aligndown-is-n,
• nat-mult/zero-01 is used by is-aligned-still-space, is-aligned-not-multiples, is-aligned-multiple-1, is-aligned-mod-alignment, eq1, alignup-add-bounded1, aligndown-not-smaller, aligndown-is-zero, aligndown-is-smaller-01, aligndown-is-smaller, aligndown-add-not-smaller,

Used from specification nat-basic1

• nat-basic1/f is used by rounded-help2, rounded-help, is-aligned-still-space, is-aligned-mod-alignment, 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, aligndown-not-smaller, aligndown-is-smaller-01, aligndown-is-smaller, aligndown-is-n, aligndown-add-same0, aligndown-add-same, aligndown-add-not-smaller,
• nat-basic1/lf is used by between-is-aligned, aligndown-is-n,
• nat-basic1/lf-01 is used by eq1, aligndown-is-n,
• nat-basic1/lf-02 is used by alignup-upper-bound, alignup-le-is-aligned, alignup-le, aligndown-is-n, aligndown-add-same0,
• nat-basic1/ls-02 is used by alignup-lower-bound, alignup-le-is-aligned, alignup-le, alignup-is-bigger,
• nat-basic1/one is used by between-is-aligned, aligndown-is-n,
• nat-basic1/ref-1 is used by eq1, alignup-upper-bound, alignup-le-is-aligned, alignup-is-bigger, aligndown-is-smaller-01, aligndown-is-smaller,
• nat-basic1/trans-1 is used by between-is-aligned,
• nat-basic1/twols-01 is used by aligndown-is-n,
• nat-basic1/zero is used by rounded-help, is-aligned-elim, is-aligned-aligndown-zero, eq1, alignup-upper-bound, 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,
• nat-div/div-elim is used by is-aligned-still-space, is-aligned-not-multiples, is-aligned-multiple-1, is-aligned-mod-alignment, is-aligned-elim, alignup-upper-bound-01, alignup-upper-bound, alignup-lower-bound, alignup-calc, aligndown-same-equiv, aligndown-le, aligndown-eq-add, aligndown-add-same0, aligndown-add-same, aligndown-add-not-smaller, aligndown-add-n,
• nat-div/div-mult is used by alignup-upper-bound,
• 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,
• nat-div/mod-eq is used by is-aligned-mod-alignment, is-aligned-aligndown-zero, between-is-aligned, alignup-add-bounded1, aligndown-is-zero,
• 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-mod-alignment, alignup-is-aligned, alignup-add-mult, aligndown-aligndown-add, aligndown-add-not-smaller,
• nat-div/mod-mult-01 is used by is-aligned-multiplier, is-aligned-multiple-1, is-aligned-mod-alignment, alignup-upper-bound, alignup-multiplier, aligndown-multiplier, aligndown-is-aligned,
• 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-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-add-mult, aligndown-aligndown-add,
• nat-div/mult-02 is used by aligndown-is-aligned-add, aligndown-aligndown-add,
• nat-div/one is used by eq1, 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,