[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Used simplifier rules/spec theorems by specification

Used from specification nat-basic

nat-basic/a is used by subarray-write-below, subarray-write-above, subarray-up-same, subarray-subarray-elim-0, subarray-subarray-elim, subarray-longer-eq-eq, subarray-copy-lower, subarray-copy-higher, subarray-copy-elim, subarray-copy, subarray-at, size-fill-h, size-copy, idexcept-n-trans-successive, idexcept-n-subarrays, idexcept-n-shorter, idexcept-eq-below, copy-subarray2, copy-subarray1-elim, copy-self, copy-rec, copy-other-weak, copy-is-subarray, copy-exact, copy-coalesce, copy-append, cmp-write-below, cmp-write-above, cmp-move-1, cmp-fill, cmp-cmp, cmp-at-0, cmp-at, at-subarray, at-fill-other, at-fill-mkarray, at-fill-h0, at-fill-h, at-copy,
nat-basic/add-base is used by subarray-write-below, subarray-up-same, subarray-subarray-elim-0, subarray-subarray-elim, subarray-longer-eq-eq, subarray-copy-lower, subarray-copy-higher, subarray-copy-elim, subarray-copy, subarray-at, idexcept-n-subarrays, copy-subarray2, copy-subarray1-elim, copy-self, copy-rec, copy-other-weak, copy-is-subarray, copy-exact, copy-coalesce, cmp-fill, cmp-cmp, cmp-at-0, cmp-at, at-subarray, at-fill-other, at-fill-mkarray, at-fill-h0, at-fill-h, at-copy,
nat-basic/c is used by subarray-write-below, subarray-write-above, subarray-up-same, subarray-subarray-elim-0, subarray-subarray-elim, subarray-longer-eq-eq, subarray-copy-lower, subarray-copy-higher, subarray-copy-elim, subarray-copy, subarray-at, size-fill-h, size-copy, idexcept-n-trans-successive, idexcept-n-subarrays, idexcept-n-shorter, idexcept-eq-below, copy-subarray2, copy-subarray1-elim, copy-self, copy-rec, copy-other-weak, copy-is-subarray, copy-exact, copy-coalesce, copy-append, cmp-write-below, cmp-write-above, cmp-move-1, cmp-fill, cmp-cmp, cmp-at-0, cmp-at, at-subarray, at-fill-other, at-fill-mkarray, at-fill-h0, at-fill-h, at-copy,
nat-basic/eq-01 is used by subarray-longer-eq-eq,
nat-basic/eq-02 is used by copy-rec, cmp-write-above,
nat-basic/f is used by subarray-write-below, subarray-up-same, subarray-subarray-elim, subarray-longer-eq-eq, subarray-copy-lower, subarray-copy-higher, subarray-copy-elim, subarray-copy, subarray-at, idexcpt-n-copy-hole, idexcept-write-at0-right, idexcept-write-at0, idexcept-trans, idexcept-same, idexcept-n-widden, idexcept-n-trans-successive, idexcept-n-trans-rev, idexcept-n-trans, idexcept-n-subarrays, idexcept-n-shorter, idexcept-n-fill-other, idexcept-n-copy-other, idexcept-extract-right, idexcept-extract-left, idexcept-eq-below, idexcept-eq-above, idexcept-comm-simp, idexcept-comm, copy-subarray2, copy-subarray1-elim, copy-rec, copy-other-weak, copy-is-subarray, copy-exact, copy-coalesce, copy-append, cmp-write-value, cmp-write-below, cmp-write-above, cmp-move-1, cmp-full-write, cmp-full-at, cmp-fill, cmp-cmp-eq, cmp-cmp, cmp-at, at-subarray, at-fill-other, at-fill-mkarray, at-fill-h0, at-fill-h, at-copy,
nat-basic/l is used by subarray-copy, idexcept-n-trans-successive, idexcept-n-subarrays, idexcept-n-shorter, copy-subarray2, copy-subarray1-elim, copy-rec, copy-other-weak, copy-coalesce, copy-append, at-fill-h, at-copy,
nat-basic/l-01 is used by subarray-copy-higher, idexcept-n-subarrays, copy-subarray1-elim, copy-coalesce, copy-append,
nat-basic/l-02 is used by subarray-write-below, subarray-longer-eq-eq, subarray-copy-lower, subarray-copy-elim, idexcept-n-trans-successive, idexcept-n-subarrays, idexcept-eq-below, copy-rec, copy-append, cmp-write-below, at-copy,
nat-basic/l-05 is used by idexcept-n-subarrays, at-fill-h,
nat-basic/l-06 is used by idexcept-n-subarrays,
nat-basic/l-08 is used by idexcept-n-trans-successive,
nat-basic/less-zero is used by subarray-write-below, subarray-up-same, subarray-subarray-elim, subarray-longer-eq-eq, subarray-copy-lower, subarray-copy-higher, subarray-copy-elim, subarray-copy, subarray-at, idexcept-n-subarrays, copy-subarray2, copy-subarray1-elim, copy-self, copy-other-weak, copy-is-subarray, copy-exact, copy-coalesce, cmp-0, at-subarray, at-fill-h0,
nat-basic/lf is used by subarray-up-same, at-fill-h,
nat-basic/lf-01 is used by idexcept-n-subarrays,
nat-basic/lf-02 is used by idexcept-n-subarrays, copy-other-weak,
nat-basic/ls-02 is used by at-fill-h,
nat-basic/neq-01 is used by at-fill-h,
nat-basic/neq-04 is used by copy-rec,
nat-basic/one-01 is used by copy-rec,
nat-basic/oz is used by cmp-write-above,
nat-basic/refl-nat is used by subarray-subarray-elim-0, copy-rec, copy-other-weak, at-fill-h, at-copy,
nat-basic/s-04 is used by cmp-move-1, at-fill-h0, at-fill-h,
nat-basic/succ is used by subarray-up-same, size-fill-h, size-copy, copy-other-weak, at-fill-h0, at-fill-h, at-copy,
nat-basic/trans-nat is used by subarray-up-same, at-fill-h,
nat-basic/zero is used by cmp-at-0,

Used from specification nat

nat/ge is used by subarray-write-above,
nat/add-01 is used by subarray-copy-higher, copy-subarray1-elim, copy-coalesce, copy-append,
nat/cancel-01 is used by subarray-copy, copy-subarray2, copy-rec, copy-append,
nat/elim-sub is used by subarray-copy, idexcept-n-subarrays, copy-subarray1-elim, copy-coalesce,
nat/eq-01 is used by subarray-copy-elim, copy-rec, at-copy,
nat/fle is used by subarray-copy-lower, subarray-copy-elim, idexcept-n-widden, idexcept-n-trans-successive, idexcept-n-shorter, idexcept-n-fill-other, idexcept-n-copy-other, copy-other-weak, copy-coalesce, at-fill-h,
nat/fle-01 is used by subarray-longer-eq-eq, subarray-copy-higher, idexcept-n-widden, idexcept-n-trans-successive, idexcept-n-trans-rev, idexcept-n-trans, idexcept-n-subarrays, idexcept-n-shorter, idexcept-n-fill-other, idexcept-n-copy-other, idexcept-eq-below, idexcept-eq-above, copy-subarray1-elim, copy-other-weak, copy-coalesce, copy-append, at-fill-other,
nat/ge is used by subarray-copy, copy-subarray2, at-fill-other,
nat/le-def is used by subarray-subarray-elim-0, subarray-copy-lower, subarray-copy-higher, idexcept-n-trans-successive, idexcept-n-subarrays, idexcept-n-shorter, copy-subarray1-elim, copy-other-weak, copy-coalesce, copy-append,
nat/le-ls-simp is used by idexcept-n-widden, idexcept-n-trans-successive, idexcept-n-trans-rev, idexcept-n-trans, idexcept-n-subarrays, idexcept-n-shorter, idexcept-n-fill-other, idexcept-n-copy-other, copy-rec, copy-append, at-fill-other, at-fill-h,
nat/lels is used by subarray-write-below, subarray-up-same, subarray-subarray-elim, subarray-longer-eq-eq, subarray-copy-lower, subarray-copy-higher, subarray-copy-elim, subarray-copy, subarray-at, idexcept-n-widden, idexcept-n-trans-successive, idexcept-n-trans-rev, idexcept-n-trans, idexcept-n-subarrays, idexcept-n-shorter, idexcept-n-fill-other, idexcept-n-copy-other, idexcept-extract-right, idexcept-eq-below, copy-subarray2, copy-subarray1-elim, copy-rec, copy-other-weak, copy-is-subarray, copy-coalesce, copy-append, cmp-write-same, cmp-fill, at-subarray, at-fill-mkarray, at-fill-h0, at-fill-h, at-copy,
nat/lels-02 is used by copy-rec, at-fill-h0, at-copy,
nat/lels-03 is used by idexcept-n-widden, idexcept-n-trans-successive, idexcept-n-trans-rev, idexcept-n-trans, idexcept-n-subarrays, idexcept-n-fill-other, idexcept-n-copy-other, idexcept-eq-above, copy-other-weak,
nat/lels-04 is used by subarray-copy-lower,
nat/lep is used by subarray-copy, idexcept-n-subarrays, copy-subarray1-elim, copy-coalesce, at-fill-h,
nat/lep-02 is used by subarray-write-above, subarray-subarray-elim, subarray-copy-lower, subarray-copy-higher, subarray-copy-elim, subarray-copy, idexcept-n-subarrays, copy-subarray2, copy-subarray1-elim, copy-rec, copy-other-weak, copy-coalesce, cmp-fill,
nat/ler is used by subarray-copy-elim-exact, copy-other,
nat/let is used by subarray-subarray-elim, subarray-copy-lower, subarray-copy-higher, subarray-copy-elim, subarray-copy, idexcept-n-widden, idexcept-n-subarrays, idexcept-n-fill-other, idexcept-n-copy-other, idexcept-eq-below, copy-subarray2, copy-subarray1-elim, copy-other-weak, copy-coalesce, cmp-fill,
nat/lez is used by cmp-fill, at-fill-other, at-fill-mkarray,
nat/ls-01 is used by idexcept-n-subarrays,
nat/ls-le-simp is used by subarray-write-below, subarray-write-above, subarray-up-same, subarray-subarray-elim, subarray-longer-eq-eq, subarray-copy-lower, subarray-copy-higher, subarray-copy-elim, subarray-copy, subarray-at, idexcept-n-subarrays, idexcept-n-fill-other, idexcept-extract-right, copy-subarray2, copy-subarray1-elim, copy-rec, copy-other-weak, copy-is-subarray, copy-exact, copy-coalesce, copy-append, cmp-write-same, cmp-fill, 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-longer-eq-eq, subarray-copy-lower, subarray-copy-higher, subarray-copy-elim, subarray-copy, subarray-at, idexcept-n-subarrays, 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 copy-rec, copy-other-weak, cmp-write-above, at-copy,

Used from specification array

array/Extension is used by subarray-write-below, subarray-write-above, subarray-up-same, subarray-subarray-elim, subarray-longer-eq-eq, subarray-copy-lower, subarray-copy-higher, subarray-copy-elim, subarray-copy, idexcept-same, idexcept-n-subarrays, 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, cmp-cmp-eq,
array/Put-other is used by copy-rec, cmp-write-value, at-fill-h0, at-fill-h, at-copy,
array/Put-other is used by subarray-write-above, idexcept-write-at0-right, idexcept-write-at0, idexcept-extract-right, idexcept-extract-left, cmp-full-write,
array/Put-same is used by idexcept-extract-left, cmp-write-value, cmp-full-write,
array/Size-mkarray is used by subarray-write-below, subarray-up-same, subarray-subarray-elim-0, subarray-subarray-elim, subarray-longer-eq-eq, subarray-elim, subarray-copy-lower, subarray-copy-higher, subarray-copy-elim, subarray-copy, subarray-at, size-subarray, idexcept-n-subarrays, 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, idexcept-write-at0-right, idexcept-write-at0, idexcept-extract-right, idexcept-extract-left, copy-rec, cmp-full-write, at-fill-h,
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, cmp-write-below, cmp-write-above,
array/eq-write-left is used by cmp-write-same,
array/ngp-07 is used by subarray-up-same,