Used simplifier rules/spec theorems by specification

Used from specification nat

• nat/le-def is used by max-def,
• nat/ls-03 is used by enc-invert,
• nat/prop-01 is used by enc-invert,
• nat/sub-add is used by enc-invert,
• nat/add-num-03 is used by max-snd-nls, max-snd-nle, max-rev, max-def, enc-invert,
• nat/add-num-04 is used by max-zero-01,
• nat/cancel-01 is used by max-rev, max-def, max-bigger,
• nat/elim-sub is used by snd-eq, max-rev, max-def, max-bigger,
• nat/eq-01 is used by snd-def, fst-def,
• nat/eq-02 is used by max-rev, max-def, enc-invert,
• nat/fle is used by max-snd-nls, max-rev, max-def-01, max-def, max-bigger,
• nat/fle-01 is used by max-zero-01, max-snd-nle, max-rev, max-le, max-def-01, max-def, max-bigger, enc-invert,
• nat/l-num-05 is used by max-zero-01,
• nat/le is used by max-snd-nle,
• nat/le-add is used by snd-ls, max-size-01,
• nat/le-ls-simp is used by max-zero-01, max-rev, max-def, enc-invert,
• nat/lels is used by snd-ls, max-snd-nls, max-size-01, max-rev, max-le, max-def-01, max-def, max-bigger, fst-ls-01, enc-invert,
• nat/lels-01 is used by snd-ls, snd-le, snd-eq, max-zero-01, max-zero, max-square, max-snd-nls, max-snd-nle, max-snd-le, max-rev, max-le, max-def, max-bigger, fst-ls, enc-invert,
• nat/lels-02 is used by max-zero-01,
• nat/lep is used by max-square, max-snd-nls, max-rev, max-def, max-bigger, enc-invert,
• nat/lep-02 is used by max-square, max-snd-nls, max-snd-nle, max-size-01, max-rev, max-def,
• nat/leprf is used by max-rev, max-def,
• nat/ler is used by max-square,
• nat/let is used by snd-nle, max-snd-nls, max-snd-nle, max-size-01, max-rev, max-def-01, max-def, fst-nle, enc-invert,
• nat/lez is used by max-rev-01, max-rev, max-def-01, max-def,
• nat/ls is used by snd-le, max-snd-nls,
• nat/ls-01 is used by max-bigger,
• nat/ls-02 is used by snd-ls, fst-ls-01,
• nat/ls-03 is used by max-rev, max-def,
• nat/ls-le-simp is used by max-nls, enc-invert,
• nat/not-zero is used by max-zero-01, max-zero,
• nat/one-02 is used by max-snd-nle,
• nat/succ-01 is used by max-rev, max-def, max-bigger,

Used from specification nat-basic2

• nat-basic2/a is used by enc-invert,
• nat-basic2/add-base is used by max-def,
• nat-basic2/c is used by snd-nle, fst-nle, enc-invert,
• nat-basic2/a is used by snd-zero, snd-one, snd-nle, snd-ls, snd-le, snd-eq, snd-def, max-zero-01, max-zero, max-square, max-snd-nls, max-snd-nle, max-size-01, max-rev-01, max-rev, max-nls, max-le, max-def-01, max-def, max-bigger, fst-nle, fst-ls-01, fst-def, encode-zero-01, encode-zero, enc-invert,
• nat-basic2/add-base is used by snd-nle, max-rev, max-def, fst-nle, encode-zero,
• nat-basic2/c is used by snd-zero, snd-one, snd-nle, snd-ls, snd-le, snd-eq, snd-def, max-zero-01, max-zero, max-square, max-snd-nls, max-snd-nle, max-size-01, max-rev-01, max-rev, max-nls, max-le, max-def-01, max-def, max-bigger, fst-nle, fst-ls-01, fst-def, encode-zero-01, encode-zero, enc-invert,
• nat-basic2/eq is used by snd-eq,
• nat-basic2/eq-01 is used by max-rev, max-def, enc-invert,
• nat-basic2/l is used by max-snd-nls, max-snd-nle, enc-invert,
• nat-basic2/l-01 is used by enc-invert,
• nat-basic2/l-02 is used by snd-le, max-square,
• nat-basic2/one is used by max-zero-01, max-snd-nls, max-rev, max-def,
• nat-basic2/oz is used by max-zero-01,
• nat-basic2/s is used by max-square, max-snd-nls, max-size-01, max-rev, max-le, max-def-01, max-def, max-bigger, enc-invert,
• nat-basic2/succ is used by max-zero-01,
• nat-basic2/z is used by max-def, max-bigger,
• nat-basic2/z-01 is used by snd-nle, snd-ls, snd-eq, max-snd-nls, max-bigger, fst-nle, encode-zero,

Used from specification nat-mult

• nat-mult/dist is used by max-snd-nls, max-rev, max-def, enc-invert,
• nat-mult/mult-c is used by snd-nle, fst-nle,
• nat-mult/numeral-32 is used by snd-nle, fst-nle,
• nat-mult/coef-06 is used by max-snd-nls,
• nat-mult/coef-07 is used by enc-invert,
• nat-mult/coef-20 is used by max-snd-nle,
• nat-mult/le is used by max-snd-nls,
• nat-mult/le-04 is used by snd-nle, fst-nle,
• nat-mult/le-num is used by enc-invert,
• nat-mult/ls-01 is used by max-rev, max-le, max-def, max-bigger,
• nat-mult/mult-a is used by snd-zero, snd-one, snd-nle, snd-ls, snd-le, snd-eq, snd-def, max-zero-01, max-zero, max-square, max-snd-nls, max-snd-nle, max-size-01, max-rev-01, max-rev, max-nls, max-le, max-def-01, max-def, max-bigger, fst-nle, fst-def, encode-zero-01, encode-zero, enc-invert,
• nat-mult/mult-c is used by snd-zero, snd-one, snd-nle, snd-ls, snd-le, snd-eq, snd-def, max-zero-01, max-zero, max-square, max-snd-nls, max-snd-nle, max-size-01, max-rev-01, max-rev, max-nls, max-le, max-def-01, max-def, max-bigger, fst-nle, fst-def, encode-zero-01, encode-zero, enc-invert,
• nat-mult/numeral-21 is used by max-snd-nls,
• nat-mult/numeral-26 is used by max-snd-nle,
• nat-mult/one is used by max-snd-nls, max-snd-nle,
• nat-mult/rsucc-02 is used by snd-ls, snd-le, snd-eq, snd-def, max-square, max-snd-nls, max-snd-nle, max-size-01, max-rev, max-nls, max-le, max-def-01, max-def, max-bigger, fst-def, encode-zero, enc-invert,
• nat-mult/square-one is used by snd-ls, snd-eq, max-nls, max-def, encode-zero,
• nat-mult/sqzero is used by snd-ls, snd-eq,
• nat-mult/succ is used by max-rev, max-def, enc-invert,
• nat-mult/two-02 is used by max-snd-nls, max-snd-nle,
• nat-mult/zero is used by snd-nle, fst-nle,
• nat-mult/zero-01 is used by max-snd-nls,
• nat-mult/zero-06 is used by snd-nle, fst-nle,

Used from specification nat-basic1

• nat-basic1/f is used by snd-le, max-zero-01, max-snd-nls, max-snd-nle, max-rev, max-nls, max-le, max-def-01, max-def, max-bigger, fst-ls-01, fst-ls, enc-invert,
• nat-basic1/lf is used by max-rev, max-def,
• nat-basic1/lf-02 is used by enc-invert,
• nat-basic1/ls-02 is used by max-def, max-bigger, fst-ls,
• nat-basic1/one is used by max-zero-01,
• nat-basic1/one-01 is used by max-zero-01, max-zero, max-bigger,
• nat-basic1/ref-1 is used by max-def-01, max-def, max-bigger,
• nat-basic1/trans is used by max-def, max-bigger,
• nat-basic1/trans-1 is used by max-rev, max-def, max-bigger,
• nat-basic1/twols-02 is used by max-zero-01,

Used from specification nat-div

• nat-div/div-add is used by max-rev, max-def,
• nat-div/exmult is used by enc-invert,
• nat-div/mult-div is used by max-snd-nls,
• nat-div/square-inject is used by injectivity,
• nat-div/square-interval is used by max-def,
• nat-div/square-ls-02 is used by max-def,
• nat-div/square-ls-03 is used by max-square,
• nat-div/two-le-02 is used by max-snd-nls,
• nat-div/two-le-03 is used by max-size-01,
• nat-div/two-ls-05 is used by max-snd-nls,
• nat-div/two-mdiv2-02 is used by enc-invert,
• nat-div/le-div-to-mult is used by max-snd-nle, max-size-01, max-rev, max-le, max-def, enc-invert,
• nat-div/ls-02 is used by max-def,
• nat-div/mod-mult is used by max-rev, max-def,
• nat-div/square-even-02 is used by max-snd-nls, max-size-01, enc-invert,
• nat-div/square-even-03 is used by max-snd-nls,
• nat-div/two-loup-12 is used by max-rev, max-le, max-def, max-bigger,
• nat-div/two-mdiv2-02 is used by max-rev, max-def, enc-invert,
• nat-div/two-rec is used by max-square, max-snd-nls, max-size-01, max-rev, max-le, max-def-01, max-def, max-bigger, enc-invert,
• nat-div/two-zero-01-01 is used by snd-ls, snd-eq, max-snd-nls, max-nls, max-def, encode-zero,