Used simplifier rules/spec theorems by specification

Used from specification nat

• nat/add-01 is used by copy-rec, copy-append, copy-coalesce, at-copy,
• nat/cancel-01 is used by copy-rec, copy-append,
• nat/elim-sub is used by copy-rec, copy-coalesce, at-copy,
• nat/eq-01 is used by copy-rec, at-copy,
• nat/fle is used by idexcept-n-widden, copy-coalesce, idexcept-n-copy-other, idexcept-n-fill-other, idexcept-n-trans-successive, idexcept-n-shorter, copy-other-weak,
• nat/fle-01 is used by idexcept-n-widden, copy-rec, copy-append, copy-coalesce, idexcept-n-copy-other, idexcept-eq-above, idexcept-n-fill-other, at-fill-other, idexcept-n-trans-successive, idexcept-n-shorter, idexcept-eq-below, at-copy, at-fill-h, copy-other-weak,
• nat/ge is used by at-fill-other,
• nat/le-def is used by idexcept-n-widden, copy-append, copy-coalesce, idexcept-n-copy-other, idexcept-n-trans-successive, idexcept-n-shorter, copy-other-weak,
• nat/le-ls-simp is used by idexcept-n-widden, copy-rec, copy-append, idexcept-n-copy-other, idexcept-n-fill-other, at-fill-h0, at-fill-other, idexcept-n-trans-successive, idexcept-n-shorter, at-fill-h,
• nat/lels is used by idexcept-n-widden, copy-rec, copy-append, copy-coalesce, idexcept-n-copy-other, at-fill-h0, cmp-fill, idexcept-n-trans-successive, cmp-write-same, idexcept-n-shorter, idexcept-eq-below, at-copy, at-fill-h, copy-other-weak,
• nat/lels-02 is used by copy-rec, at-copy, at-fill-h,
• nat/lels-03 is used by idexcept-n-copy-other, idexcept-eq-above, idexcept-n-trans-successive, copy-other-weak,
• nat/lep is used by copy-rec, copy-coalesce, at-copy, at-fill-h,
• nat/lep-02 is used by copy-rec, copy-coalesce, cmp-fill, at-copy, copy-other-weak,
• nat/ler is used by copy-other,
• nat/let is used by idexcept-n-widden, copy-coalesce, idexcept-n-copy-other, idexcept-n-fill-other, cmp-fill, idexcept-eq-below, at-copy, at-fill-h, copy-other-weak,
• nat/lez is used by at-fill-h0, cmp-fill, at-fill-other,
• nat/ls-le-simp is used by idexcept-n-widden, copy-coalesce, idexcept-n-copy-other, copy-exact, idexcept-n-fill-other, cmp-fill, cmp-write-same, at-copy, copy-other-weak,
• nat/sub-base is used by copy-coalesce, copy-exact, copy-self, copy-other-weak,
• nat/succ-01 is used by copy-rec, at-copy, copy-other-weak,

Used from specification fsarray

• fsarray/Extension is used by copy-rec, copy-append, copy-coalesce, idexcept-same, idexcept-extract-right, copy-exact, idexcept-extract-left, copy-self, cmp-cmp-eq, copy-other-weak,
• fsarray/Put-other is used by copy-rec, idexcept-extract-right, idexcept-extract-left, cmp-write-value, at-copy, at-fill-h,
• fsarray/Put-other is used by idexcept-extract-right, idexcept-extract-left, idexcept-write-at0-right, idexcept-write-at0, idexcept-write-at, idexcept-write-at-right,
• fsarray/Put-same is used by copy-rec, idexcept-extract-right, idexcept-extract-left, cmp-write-value, cmp-full-write, at-fill-h,
• fsarray/Size-array is used by idexcept-n-widden, copy-rec, idexcept-n-copy-other, idexcept-eq-above, idexcpt-n-copy-hole, idexcept-n-trans, idexcept-n-fill-other, idexcept-n-trans-successive, cmp-write-same, idexcept-n-shorter, idexcept-eq-below, at-copy, idexcept-n-trans-rev,
• fsarray/cgetput is used by copy-rec, at-copy,
• fsarray/cngetput is used by cmp-write-below,
• fsarray/eq-write-left is used by cmp-write-same,
• fsarray/ngp-06 is used by copy-other-weak,
• fsarray/ngp-07 is used by copy-rec,
• fsarray/ngp-08 is used by copy-rec,
• fsarray/put-same-content is used by cmp-full-write,

Used from specification nat-basic

• nat-basic/a is used by idexcept-n-widden, copy-rec, copy-append, cmp-cmp, copy-coalesce, cmp-at-0, copy-exact, copy-self, idexcept-n-fill-other, at-fill-h0, cmp-fill, at-fill-other, cmp-move-1, cmp-write-above, cmp-at, idexcept-n-trans-successive, idexcept-n-shorter, idexcept-eq-below, cmp-write-below, at-copy, at-fill-h, copy-other-weak,
• nat-basic/add-base is used by copy-rec, cmp-cmp, copy-coalesce, cmp-at-0, copy-exact, copy-self, cmp-fill, at-fill-other, cmp-at, at-copy, at-fill-h, copy-other-weak,
• nat-basic/c is used by idexcept-n-widden, copy-rec, copy-append, cmp-cmp, copy-coalesce, cmp-at-0, copy-exact, copy-self, idexcept-n-fill-other, at-fill-h0, cmp-fill, at-fill-other, cmp-move-1, cmp-write-above, cmp-at, idexcept-n-trans-successive, idexcept-n-shorter, idexcept-eq-below, cmp-write-below, at-copy, at-fill-h, copy-other-weak,
• nat-basic/eq-01 is used by copy-rec, at-copy,
• nat-basic/eq-02 is used by copy-rec,
• nat-basic/f is used by idexcept-n-widden, copy-rec, copy-append, cmp-cmp, copy-coalesce, idexcept-n-copy-other, idexcept-same, idexcept-extract-right, cmp-full-at, idexcept-eq-above, idexcept-extract-left, idexcept-n-trans, idexcept-write-at0-right, idexcept-n-fill-other, cmp-cmp-eq, at-fill-h0, cmp-fill, at-fill-other, cmp-move-1, cmp-write-value, idexcept-write-at0, cmp-at, cmp-full-write, idexcept-n-trans-successive, idexcept-n-shorter, idexcept-eq-below, idexcept-comm-simp, cmp-write-below, at-copy, at-fill-h, idexcept-n-trans-rev, copy-other-weak, idexcept-trans,
• nat-basic/l is used by copy-rec, copy-append, copy-coalesce, idexcept-n-trans-successive, idexcept-n-shorter, at-copy, at-fill-h,
• nat-basic/l-01 is used by idexcept-n-widden, copy-rec, copy-append, copy-coalesce, idexcept-n-fill-other, idexcept-n-trans-successive, at-fill-h, copy-other-weak,
• nat-basic/l-02 is used by copy-append, idexcept-n-trans-successive, idexcept-eq-below, cmp-write-below, at-copy,
• nat-basic/l-08 is used by idexcept-n-trans-successive,
• nat-basic/less-zero is used by copy-coalesce, copy-exact, copy-self, cmp-0, at-fill-h0, copy-other-weak,
• nat-basic/lf-02 is used by copy-rec,
• nat-basic/ls-02 is used by copy-rec, at-fill-h,
• nat-basic/neq-01 is used by copy-rec,
• nat-basic/one-01 is used by copy-rec,
• nat-basic/refl-Nat is used by copy-rec, cmp-cmp, cmp-cmp-eq, cmp-write-above, idexcept-n-trans-successive, at-copy, at-fill-h,
• nat-basic/s-04 is used by copy-rec, at-fill-h0, cmp-move-1, cmp-write-above, at-fill-h,
• nat-basic/succ is used by at-fill-h0, at-copy, at-fill-h, copy-other-weak,
• nat-basic/zero is used by cmp-at-0,