Used simplifier rules/spec theorems by specification

Used from specification nat

• nat/add-01 is used by subarray-copy-higher, subarray-copy, copy-subarray2, copy-subarray1-elim, copy-coalesce, copy-append, at-copy,
• nat/cancel-01 is used by subarray-copy, copy-subarray2, copy-rec, copy-append,
• nat/elim-sub is used by subarray-copy, rev-rev, rev-at-h, rev-at, copy-subarray2, copy-subarray1-elim, copy-coalesce, at-copy,
• nat/eq-01 is used by subarray-copy-elim, subarray-copy, copy-subarray2, copy-rec, at-copy,
• nat/fle is used by subarray-copy-lower, subarray-copy-elim, rev-rev, rev-at-h, copy-other-weak, copy-coalesce,
• nat/fle-01 is used by subarray-copy-higher, subarray-copy, rev-at-h, copy-subarray2, copy-subarray1-elim, copy-other-weak, copy-coalesce, copy-append, at-fill-other, at-fill-h, at-copy,
• nat/ge is used by subarray-copy, copy-subarray2, at-fill-other,
• nat/le-ls-simp is used by rev-at-h, copy-rec, copy-append, at-fill-h,
• nat/lels is used by subarray-write-below, subarray-up-same, subarray-subarray-elim, subarray-copy-lower, subarray-copy-higher, subarray-copy-elim, subarray-copy, rev-rev, rev-at-h, rev-at, idexcept-extract-right, copy-subarray2, copy-subarray1-elim, copy-rec, copy-other-weak, copy-is-subarray, copy-coalesce, copy-append, at-subarray, at-fill-mkarray, at-fill-h0, at-fill-h, at-copy,
• nat/lels-01 is used by subarray-copy-lower, subarray-copy-higher, subarray-copy, rev-size, copy-subarray2, copy-subarray1-elim, copy-other-weak, copy-coalesce, copy-append,
• nat/lels-02 is used by rev-at-h, copy-rec, at-fill-h0, at-copy,
• nat/lels-03 is used by rev-size-h, rev-at-h, copy-other-weak, at-fill-other,
• nat/lels-04 is used by subarray-copy-lower,
• nat/lep is used by subarray-copy, rev-at-h, copy-subarray2, copy-subarray1-elim, copy-coalesce, at-fill-h, at-copy,
• nat/lep-02 is used by subarray-subarray-elim, subarray-copy-lower, subarray-copy-higher, subarray-copy-elim, subarray-copy, copy-subarray2, copy-subarray1-elim, copy-rec, copy-other-weak, copy-coalesce, at-copy,
• nat/ler is used by subarray-copy-elim-exact, rev-at-h, rev-at, copy-other,
• nat/let is used by subarray-subarray-elim, subarray-copy-lower, subarray-copy-higher, subarray-copy-elim, subarray-copy, rev-at-h, copy-subarray2, copy-subarray1-elim, copy-other-weak, copy-coalesce,
• nat/lez is used by at-fill-mkarray,
• nat/ls-le-simp is used by subarray-write-below, subarray-up-same, subarray-subarray-elim, subarray-copy-lower, subarray-copy-higher, subarray-copy-elim, subarray-copy, subarray-at, rev-rev, rev-at-h, rev-at, idexcept-extract-right, copy-subarray2, copy-subarray1-elim, copy-rec, copy-other-weak, copy-is-subarray, copy-exact, copy-coalesce, copy-append, at-subarray, at-fill-mkarray, at-fill-h0, at-fill-h, at-copy,
• nat/sub-base is used by subarray-write-below, subarray-up-same, subarray-subarray-elim, subarray-copy-lower, subarray-copy-higher, subarray-copy-elim, subarray-copy, subarray-at, copy-subarray2, copy-subarray1-elim, copy-self, copy-other-weak, copy-is-subarray, copy-exact, copy-coalesce, at-subarray,
• nat/succ-01 is used by rev-size-h, rev-rev, rev-at-h, rev-at, copy-rec, copy-other-weak, at-fill-other, at-copy,

Used from specification nat-basic2

• nat-basic2/a is used by subarray-write-below, subarray-up-same, subarray-subarray-elim, subarray-copy-lower, subarray-copy-higher, subarray-copy-elim, subarray-copy, subarray-at, size-fill-h, size-copy, rev-size-h, rev-rev, rev-at-h, rev-at, copy-subarray2, copy-subarray1-elim, copy-self, copy-rec, copy-other-weak, copy-is-subarray, copy-exact, copy-coalesce, copy-append, at-subarray, at-fill-other, at-fill-mkarray, at-fill-h0, at-fill-h, at-copy,
• nat-basic2/add-base is used by subarray-write-below, subarray-up-same, subarray-subarray-elim, subarray-copy-lower, subarray-copy-higher, subarray-copy-elim, subarray-copy, subarray-at, copy-subarray2, copy-subarray1-elim, copy-self, copy-rec, copy-other-weak, copy-is-subarray, copy-exact, copy-coalesce, at-subarray, at-fill-other, at-fill-mkarray, at-fill-h0, at-fill-h, at-copy,
• nat-basic2/c is used by subarray-write-below, subarray-up-same, subarray-subarray-elim, subarray-copy-lower, subarray-copy-higher, subarray-copy-elim, subarray-copy, subarray-at, size-fill-h, size-copy, rev-size-h, rev-rev, rev-at-h, rev-at, copy-subarray2, copy-subarray1-elim, copy-self, copy-rec, copy-other-weak, copy-is-subarray, copy-exact, copy-coalesce, copy-append, at-subarray, at-fill-other, at-fill-mkarray, at-fill-h0, at-fill-h, at-copy,
• nat-basic2/eq is used by copy-rec,
• nat-basic2/eq-01 is used by rev-at-h, at-copy,
• nat-basic2/eqs is used by rev-rev, rev-at-h, rev-at,
• nat-basic2/l is used by subarray-copy, rev-at-h, copy-subarray2, copy-subarray1-elim, copy-rec, copy-other-weak, copy-coalesce, copy-append, at-fill-h, at-copy,
• nat-basic2/l-01 is used by subarray-copy-higher, subarray-copy, rev-at-h, copy-subarray2, copy-subarray1-elim, copy-other-weak, copy-coalesce, copy-append, at-fill-h, at-copy,
• nat-basic2/l-02 is used by subarray-write-below, subarray-copy-lower, subarray-copy-elim, subarray-copy, rev-rev, rev-at-h, rev-at, copy-subarray2, copy-rec, copy-append, at-copy,
• nat-basic2/l-06 is used by rev-at-h,
• nat-basic2/neq-01 is used by copy-rec,
• nat-basic2/one-03 is used by rev-at-h,
• nat-basic2/oz is used by rev-rev, rev-at-h, at-fill-h0,
• nat-basic2/s is used by rev-rev, rev-at-h, rev-at, at-fill-h0, at-fill-h,
• nat-basic2/succ is used by subarray-up-same, size-fill-h, size-copy, rev-size-h, rev-at-h, copy-other-weak, at-fill-other, at-fill-h0, at-fill-h, at-copy,

Used from specification nat-basic1

• nat-basic1/f is used by subarray-write-below, subarray-up-same, subarray-subarray-elim, subarray-copy-lower, subarray-copy-higher, subarray-copy-elim, subarray-copy, subarray-at, rev-size-h, rev-rev, rev-at-h, rev-at, in-at, idexcept-write-at0-right, idexcept-write-at0, idexcept-trans, idexcept-same, idexcept-extract-right, idexcept-extract-left, idexcept-comm-simp, idexcept-comm, copy-subarray2, copy-subarray1-elim, copy-rec, copy-other-weak, copy-is-subarray, copy-exact, copy-coalesce, copy-append, at-subarray, at-fill-other, at-fill-mkarray, at-fill-h0, at-fill-h, at-copy,
• nat-basic1/lf is used by subarray-up-same, rev-at-h, at-fill-other,
• nat-basic1/lf-01 is used by rev-rev, rev-at-h, rev-at, idexcept-write-at0-right, idexcept-write-at0, idexcept-trans, idexcept-same, idexcept-extract-right, idexcept-extract-left, idexcept-comm-simp, idexcept-comm, copy-other-weak, copy-exact,
• nat-basic1/lf-02 is used by copy-other-weak,
• nat-basic1/ls-02 is used by at-fill-h,
• nat-basic1/neq-01 is used by at-fill-h, at-copy,
• nat-basic1/one is used by rev-at-h,
• nat-basic1/one-01 is used by copy-rec,
• nat-basic1/ref-1 is used by rev-size, copy-rec, copy-other-weak, at-fill-other, at-fill-h, at-copy,
• nat-basic1/trans-1 is used by subarray-up-same, at-fill-other,
• nat-basic1/zero-01 is used by subarray-write-below, subarray-up-same, subarray-subarray-elim, subarray-copy-lower, subarray-copy-higher, subarray-copy-elim, subarray-copy, subarray-at, copy-subarray2, copy-subarray1-elim, copy-self, copy-other-weak, copy-is-subarray, copy-exact, copy-coalesce, at-subarray,

Used from specification array

• array/Extension is used by subarray-write-below, subarray-up-same, subarray-subarray-elim, subarray-copy-lower, subarray-copy-higher, subarray-copy-elim, subarray-copy, rev-rev, idexcept-same, idexcept-extract-right, idexcept-extract-left, copy-subarray2, copy-subarray1-elim, copy-self, copy-rec, copy-other-weak, copy-is-subarray, copy-exact, copy-coalesce, copy-append,
• array/Put-other is used by rev-at-h, copy-rec, at-fill-h0,
• array/Put-same is used by rev-at-h,
• array/Put-other is used by idexcept-write-at0-right, idexcept-write-at0, idexcept-extract-right, idexcept-extract-left, at-fill-h, at-copy,
• array/Put-same is used by idexcept-extract-left,
• array/Size-mkarray is used by subarray-write-below, subarray-up-same, subarray-subarray-elim, subarray-elim, subarray-copy-lower, subarray-copy-higher, subarray-copy-elim, subarray-copy, subarray-at, size-subarray, rev-size-h, copy-subarray2, copy-subarray1-elim, copy-other, copy-is-subarray, at-subarray, at-fill-mkarray,
• array/Size-put is used by subarray-up-same, size-fill-h, size-copy, rev-size-h, idexcept-write-at0-right, idexcept-write-at0, idexcept-extract-right, idexcept-extract-left, copy-rec,
• array/cgetput is used by idexcept-extract-right, copy-rec, at-fill-h0, at-fill-h, at-copy,
• array/cngetput is used by subarray-write-below, copy-other-weak, at-fill-other,
• array/ngp-07 is used by subarray-up-same,