[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

Used from specification nat

nat/le-addex is used by array-le-kill-prefix,
nat/add-01 is used by rev-subarray-split-step, remains-ordered-by-swap, ordered-step-down, next-proper-permutation, array-le-one-diffrent-position,
nat/add-num-01 is used by rev-subarray-split-step, rev-subarray-split-last-swap, next-proper-permutation, get-rev,
nat/add-num-03 is used by rev-subarray-split-step, rev-subarray-split-last-swap, remains-ordered-by-swap, next-proper-permutation, get-rev,
nat/anti is used by subarray-inc, rev-subarray-split-step, rev-subarray-split-last-swap, next-proper-permutation, next-perm,
nat/cancel-01 is used by subarray-inc-offset, rev-subarray-split-step, rev-subarray-split-last-swap, remains-ordered-by-swap, next-proper-permutation,
nat/elim-pred-c is used by subarray-inc-offset0, ordered-all-rev, next-proper-permutation, next-perm, array-le-one-diffrent-position,
nat/elim-sub is used by rev-subarray-split-step, rev-subarray-split-last-swap, remains-ordered-by-swap, next-proper-permutation, get-rev, array-split-into-subarrays, array-le-same-prepart, array-le-kill-prefix,
nat/eq is used by ordered-step-down, next-proper-permutation,
nat/eq-01 is used by rev-subarray-split-step, rev-subarray-split-last-swap, remains-ordered-by-swap, next-proper-permutation,
nat/eq-03 is used by next-proper-permutation,
nat/eqle-one is used by subarray-inc-offset, ordered-step-down, next-proper-permutation, next-perm,
nat/fle is used by rev-subarray-last, remains-ordered-by-swap, ordered-all-rev, next-proper-permutation, next-perm, get-rev, array-le-swap, array-le-one-diffrent-position,
nat/fle-01 is used by rev-subarray-split-step, rev-subarray-split-last-swap, remains-ordered-by-swap, ordered-step-down, ordered-all-rev, next-proper-permutation, next-perm, array-split-into-subarrays,
nat/ge is used by subarray-write-above, next-proper-permutation, next-perm,
nat/gr-def is used by not-ordered, next-proper-permutation, next-perm, descending-order-is-max-permuted,
nat/l-num-01 is used by rev-subarray-split-step, next-proper-permutation,
nat/l-num-02 is used by next-proper-permutation,
nat/l-num-03 is used by rev-subarray-split-step, next-proper-permutation,
nat/l-num-04 is used by next-proper-permutation,
nat/l-num-05 is used by rev-subarray-split-step,
nat/l-num-06 is used by rev-subarray-split-step, next-proper-permutation, array-le-swap,
nat/le-def is used by subarray-inc-offset0, rev-subarray-split-step, rev-subarray-split-last-swap, remains-ordered-by-swap, next-proper-permutation, next-perm, array-le-swap, array-le-one-diffrent-position, array-le-kill-prefix,
nat/le-ls-simp is used by subarray-inc-offset0, subarray-inc, remains-ordered-by-swap, ordered-all-rev, next-proper-permutation, array-le-one-diffrent-position,
nat/le-num-01 is used by rev-subarray-split-last-swap, next-proper-permutation,
nat/le-num-04 is used by rev-subarray-split-step,
nat/le-num-05 is used by next-proper-permutation,
nat/le-num-06 is used by rev-subarray-split-step, rev-subarray-split-last-swap, remains-ordered-by-swap,
nat/le-sum is used by ordered-all-rev,
nat/lels is used by subarray-inc-offset0, subarray-inc-offset, subarray-inc, rev-subarray-split-step, rev-subarray-split-last-swap, rev-subarray-last, remains-ordered-by-swap, permut-correct, ordered-step-down, ordered-all-rev, next-proper-permutation, next-perm, get-rev, array-split-into-subarrays, array-le-swap, array-le-same-prepart, array-le-one-diffrent-position, array-le-kill-prefix,
nat/lels-02 is used by rev-subarray-split-last-swap, next-proper-permutation, descending-order-is-max-permuted, ascending-order-is-min-permuted, array-neg-le-eq-2, array-neg-le-eq, array-le-trans, array-le-swap, array-le-same-prefix, array-le-one-diffrent-position,
nat/lels-03 is used by subarray-prefix-fistn, rev-subarray-split-step, next-proper-permutation, array-split-into-subarrays, array-le-same-prepart, array-le-one-diffrent-position, array-le-kill-prefix,
nat/lep is used by rev-subarray-split-step, rev-subarray-split-last-swap, remains-ordered-by-swap, next-proper-permutation, array-split-into-subarrays, array-le-kill-prefix,
nat/lep-02 is used by subarray-write-above, rev-subarray-split-step, rev-subarray-split-last-swap, remains-ordered-by-swap, ordered-step-down, ordered-all-rev, next-proper-permutation, array-le-one-diffrent-position,
nat/ler is used by rev-subarray-split-step, remains-ordered-by-swap, permut-correct, ordered-step-down, next-proper-permutation, array-le-one-diffrent-position,
nat/les is used by subarray-inc-offset, ordered-step-down, next-proper-permutation,
nat/let is used by rev-subarray-split-step, rev-subarray-split-last-swap, ordered-all-rev, next-proper-permutation,
nat/lez is used by subarray-inc-offset0, rev-subarray-split-step, rev-subarray-split-last-swap, ordered-all-rev, array-le-swap, array-le-one-diffrent-position,
nat/lez-01 is used by ordered-all-rev, next-proper-permutation, next-perm, array-le-one-diffrent-position,
nat/ls is used by next-proper-permutation,
nat/ls-01 is used by subarray-inc-offset0, next-proper-permutation, next-perm,
nat/ls-02 is used by next-proper-permutation, next-perm,
nat/ls-03 is used by next-proper-permutation,
nat/ls-add-not-01 is used by ordered-all-rev,
nat/ls-le-simp is used by subarray-write-above, rev-subarray-split-step, rev-subarray-split-last-swap, remains-ordered-by-swap, next-proper-permutation, next-perm, get-rev, array-le-same-prepart,
nat/not-zero is used by rev-subarray-split-step,
nat/one-02 is used by rev-subarray-split-last-swap,
nat/pred-03 is used by next-proper-permutation, next-perm,
nat/prop-07 is used by next-proper-permutation,
nat/sub-add is used by next-proper-permutation,
nat/sub-base is used by next-proper-permutation,
nat/succ-01 is used by subarray-inc-offset0, subarray-inc, rev-subarray-split-step, remains-ordered-by-swap, permut-correct, ordered-step-down, ordered-all-rev, next-proper-permutation, next-perm, get-rev, array-le-swap, array-le-one-diffrent-position,
nat/zero is used by subarray-inc-offset, subarray-inc, rev-subarray-split-step, rev-subarray-split-last-swap, next-proper-permutation,

Used from specification set-basic

set-basic/array-set/Extension is used by permut-correct, perm-all-perms-eq, ordered-smallerPerms, ordered-append, nil-toSet, next-perm-smallerPerms, next-perm-greaterPerms, max-smaller-perms-all-perms,
set-basic/array-set/Size-insert is used by permut-correct,
set-basic/array-set/In-empty is used by ordered-smallerPerms, nil-toSet,
set-basic/array-set/In-insert is used by permut-correct, next-perm-smallerPerms, next-perm-greaterPerms, max-smaller-perms-all-perms,
set-basic/array-set/eq is used by permut-correct,
set-basic/array-set/size-zero is used by ordered-smallerPerms, nil-toSet,
set-basic/array-set/size-zero-01 is used by ordered-smallerPerms, nil-toSet,

Used from specification list-last

list-last/natarray-oarray-sort/rev-rewrite is used by rev-subarray-last,
list-last/natarray-oarray-sort/last-def is used by ordered-step-down, ordered-all-rev,
list-last/natarray-oarray-sort/last-elim is used by rev-subarray-last,
list-last/natarray-oarray-sort/rev-app is used by rev-subarray-last, get-rev,
list-last/natarray-oarray-sort/rev-e is used by rev-subarray-last, ordered-step-down, ordered-all-rev, descending-order-is-max-permuted,
list-last/natarray-oarray-sort/rev-empty is used by rev-subarray-last, rev-mkarray-empty, ordered-step-down,
list-last/natarray-oarray-sort/rev-in is used by rev-subarray-last, descending-order-is-max-permuted,
list-last/natarray-oarray-sort/rev-length is used by rev-subarray-split-step, rev-subarray-split-last-swap, rev-subarray-last, remains-ordered-by-swap, next-proper-permutation,
list-last/natarray-oarray-sort/rev-one is used by rev-subarray-last, get-rev,
list-last/natarray-oarray-sort/rev-r is used by ordered-step-down, ordered-all-rev, descending-order-is-max-permuted,
list-last/natarray-oarray-sort/revert-equal is used by next-proper-permutation,

Used from specification list-data

list-data/natarray-oarray-sort/elim-list-c is used by subarray-inc-offset,
list-data/natarray-oarray-sort/l is used by subarray-prefix-fistn, subarray-inc-offset0, subarray-inc-offset, subarray-inc, rev-subarray-last, remains-ordered-by-swap, ordered-step-down, next-proper-permutation, next-perm, get-rev, array-split-into-subarrays, array-le-swap, array-le-same-prepart2, array-le-same-prepart, array-le-one-diffrent-position, array-le-kill-prefix,
list-data/natarray-oarray-sort/size-nil is used by rev-subarray-last, rev-mkarray-empty, ordered-all-rev, array-le-one-diffrent-position,

Used from specification list

list/natarray-oarray-sort/Noassoc is used by not-ordered,
list/list-of-natarray/lastdiv-rew is used by ordered-append,
list/natarray-oarray-sort/lastdiv-rew is used by get-rev,
list/list-of-natarray/Last is used by permut-correct,
list/natarray-oarray-sort/Last is used by subarray-inc-offset, subarray-inc, rev-subarray-last, ordered-step-down, ordered-all-rev, descending-order-is-max-permuted,
list/list-of-natarray/Nil is used by ordered-arraylist-append-last, ordered-append,
list/natarray-oarray-sort/Nil is used by ordered-step-down, ordered-all-rev, next-proper-permutation, array-le-same-prefix2, array-le-same-prefix,
list/list-of-natarray/a is used by permut-correct, ordered-arraylist-two, ordered-arraylist-append-last, ordered-append,
list/natarray-oarray-sort/a is used by subarray-inc-offset0, subarray-inc-offset, subarray-inc, rev-subarray-split-step, rev-subarray-split-last-swap, rev-subarray-last, ordered-step-down, ordered-all-rev, not-ordered, next-proper-permutation, get-rev, descending-order-is-max-permuted, ascending-order-is-min-permuted, array-split-into-subarrays, array-neg-le-eq-2, array-neg-le-eq, array-le-trans, array-le-swap, array-le-same-prepart, array-le-same-prefix3, array-le-same-prefix2, array-le-same-prefix, array-le-refl, array-le-one-diffrent-position,
list/list-of-natarray/app is used by ordered-arraylist-two,
list/natarray-oarray-sort/app is used by ordered-all-rev, next-proper-permutation, array-le-one-diffrent-position,
list/natarray-oarray-sort/app-02 is used by subarray-inc-offset, descending-order-is-max-permuted, ascending-order-is-min-permuted,
list/list-of-natarray/c is used by ordered-arraylist-append-last,
list/natarray-oarray-sort/c is used by subarray-inc-offset0, subarray-inc-offset, ordered-step-down, ordered-all-rev, not-ordered, next-proper-permutation, descending-order-is-max-permuted, ascending-order-is-min-permuted, array-neg-le-eq-2, array-neg-le-eq, array-le-trans, array-le-swap, array-le-same-prefix2, array-le-same-prefix, array-le-refl, array-le-one-diffrent-position,
list/natarray-oarray-sort/c-06 is used by next-proper-permutation, array-le-one-diffrent-position,
list/natarray-oarray-sort/e is used by subarray-inc-offset, descending-order-is-max-permuted, ascending-order-is-min-permuted,
list/natarray-oarray-sort/e-01 is used by ordered-step-down, array-neg-le-eq-2, array-neg-le-eq, array-le-swap, array-le-one-diffrent-position,
list/natarray-oarray-sort/e-02 is used by subarray-inc-offset, rev-subarray-last, ordered-all-rev,
list/natarray-oarray-sort/in-01 is used by next-proper-permutation,
list/natarray-oarray-sort/in-12 is used by not-ordered,
list/natarray-oarray-sort/in-14 is used by subarray-inc-offset, rev-subarray-last, array-le-one-diffrent-position,
list/natarray-oarray-sort/in-15 is used by subarray-inc-offset, rev-subarray-last,
list/list-of-natarray/in-15 is used by permut-correct,
list/list-of-natarray/in-17 is used by permut-correct, ordered-append,
list/natarray-oarray-sort/in-17 is used by subarray-inc-offset, rev-subarray-last, descending-order-is-max-permuted,
list/natarray-oarray-sort/in-append is used by subarray-inc-offset, rev-subarray-last,
list/list-of-natarray/in-append is used by permut-correct, ordered-append,
list/natarray-oarray-sort/in-empty is used by not-ordered,
list/list-of-natarray/in-empty is used by nil-toSet,
list/natarray-oarray-sort/in-rec is used by subarray-inc-offset, not-ordered, array-le-one-diffrent-position,
list/natarray-oarray-sort/len is used by subarray-inc-offset, subarray-inc, rev-subarray-split-step, rev-subarray-split-last-swap, get-rev, array-split-into-subarrays, array-le-same-prepart,
list/natarray-oarray-sort/len-01 is used by array-neg-le-eq-2, array-neg-le-eq, array-le-same-prefix,
list/natarray-oarray-sort/len-02 is used by subarray-inc-offset0, subarray-inc-offset, subarray-inc, ordered-all-rev, get-rev,
list/natarray-oarray-sort/len-05 is used by subarray-inc-offset0, subarray-inc-offset, rev-subarray-last, ordered-all-rev, array-le-swap, array-le-one-diffrent-position,

Used from specification array-copy

array-copy/natarray/at-subarray is used by subarray-inc-offset0, subarray-inc, rev-subarray-split-step, rev-subarray-split-last-swap, remains-ordered-by-swap,
array-copy/natarray/size-subarray is used by subarray-write-above, subarray-prefix-fistn, subarray-inc-offset0, subarray-inc-offset, subarray-inc, rev-subarray-split-step, rev-subarray-split-last-swap, rev-subarray-last, remains-ordered-by-swap, next-proper-permutation, array-split-into-subarrays, array-le-same-prepart, array-le-one-diffrent-position,
array-copy/natarray/subarray-at is used by subarray-write-above, subarray-prefix-fistn, subarray-inc-offset, subarray-inc, rev-subarray-split-step, rev-subarray-split-last-swap, rev-subarray-last, next-proper-permutation, array-split-into-subarrays, array-le-same-prepart, array-le-one-diffrent-position,
array-copy/natarray/subarray-elim-simp is used by next-proper-permutation,
array-copy/natarray/subarray-write-below is used by next-proper-permutation,
array-copy/natarray/subarray-zero is used by ordered-step-down, next-proper-permutation, array-le-one-diffrent-position,

Used from specification list-dup

list-dup/list-of-natarray/e-01 is used by permut-correct,
list-dup/list-of-natarray/f is used by permut-correct,

Used from specification list-perm

list-perm/natarray-oarray-sort/app-beg-beg is used by array-le-kill-prefix,
list-perm/natarray-oarray-sort/del is used by next-proper-permutation,
list-perm/natarray-oarray-sort/del-01 is used by next-proper-permutation,
list-perm/natarray-oarray-sort/l is used by next-proper-permutation, array-le-same-prepart2, array-le-kill-prefix,
list-perm/natarray-oarray-sort/perm-switch is used by next-proper-permutation, next-perm,
list-perm/natarray-oarray-sort/rec is used by descending-order-is-max-permuted, ascending-order-is-min-permuted,
list-perm/natarray-oarray-sort/sym is used by permut-correct, perm-all-perms-eq, next-proper-permutation, next-perm-smallerPerms, next-perm-greaterPerms, next-perm,
list-perm/natarray-oarray-sort/trans is used by permut-correct, perm-all-perms-eq, next-proper-permutation, next-perm-smallerPerms, next-perm-greaterPerms,
list-perm/natarray-oarray-sort/cons is used by next-proper-permutation, descending-order-is-max-permuted, ascending-order-is-min-permuted,
list-perm/natarray-oarray-sort/empty is used by descending-order-is-max-permuted, ascending-order-is-min-permuted,
list-perm/natarray-oarray-sort/empty-01 is used by next-proper-permutation, descending-order-is-max-permuted, ascending-order-is-min-permuted,
list-perm/natarray-oarray-sort/neq is used by permut-correct, next-perm-smallerPerms, next-perm-greaterPerms, array-le-kill-prefix,
list-perm/natarray-oarray-sort/perm-e is used by next-perm,
list-perm/natarray-oarray-sort/perm-swap is used by next-perm,
list-perm/natarray-oarray-sort/ref is used by permut-correct, next-proper-permutation, next-perm-smallerPerms, next-perm-greaterPerms, next-perm, max-smaller-perms-all-perms,
list-perm/natarray-oarray-sort/trans is used by perm-all-perms-eq, next-proper-permutation, next-perm-smallerPerms, next-perm-greaterPerms, array-le-same-prepart2, array-le-kill-prefix,

Used from specification oelem

oelem/natarray/irreflexivity is used by rev-subarray-split-step, remains-ordered-by-swap, permut-correct, ordered-step-down, ordered-all-rev, next-proper-permutation, next-perm,
oelem/natarray/lel is used by rev-subarray-split-step, rev-subarray-split-last-swap, remains-ordered-by-swap, next-proper-permutation, array-le-trans, array-le-one-diffrent-position, array-le-kill-prefix,
oelem/natarray/ls-le is used by rev-subarray-split-step, next-proper-permutation, next-perm, array-le-swap,
oelem/natarray/sls is used by descending-order-is-max-permuted, ascending-order-is-min-permuted, array-neg-le-eq,
oelem/natarray/transitivity is used by subarray-prefix-fistn, rev-subarray-split-step, remains-ordered-by-swap, next-proper-permutation, next-perm, array-le-trans, array-le-swap, array-le-one-diffrent-position,

Used from specification olist

olist/natarray-oarray-sort/ole-last-01 is used by ordered-step-down, ordered-all-rev,
olist/natarray-oarray-sort/orderedle-all is used by remains-ordered-by-swap,
olist/natarray-oarray-sort/orderedle-ls is used by not-ordered,
olist/natarray-oarray-sort/app is used by ordered-all-rev, descending-order-is-max-permuted,
olist/natarray-oarray-sort/cons-02 is used by not-ordered, ascending-order-is-min-permuted,
olist/natarray-oarray-sort/le-e is used by ordered-step-down, ordered-all-rev, descending-order-is-max-permuted, ascending-order-is-min-permuted,
olist/natarray-oarray-sort/le-o is used by ordered-step-down, ordered-all-rev,
olist/natarray-oarray-sort/orderedle-ls is used by ascending-order-is-min-permuted,
olist/natarray-oarray-sort/szle1-orderedle is used by ordered-size-smaller-one,

Used from specification list-del

list-del/natarray-oarray-sort/get-append-grt is used by rev-subarray-split-step,
list-del/natarray-oarray-sort/get-append-less is used by subarray-inc-offset0, subarray-inc-offset, rev-subarray-split-step, rev-subarray-split-last-swap, ordered-all-rev, get-rev, array-split-into-subarrays, array-le-same-prepart,
list-del/natarray-oarray-sort/get-butlast is used by subarray-inc,
list-del/natarray-oarray-sort/get-firstn is used by subarray-prefix-fistn,
list-del/natarray-oarray-sort/in-get is used by next-proper-permutation,
list-del/natarray-oarray-sort/del1-n is used by next-proper-permutation,
list-del/natarray-oarray-sort/firstn-length-03 is used by subarray-prefix-fistn,
list-del/natarray-oarray-sort/get-append-grt is used by subarray-inc-offset0, subarray-inc-offset, subarray-inc, rev-subarray-split-step, rev-subarray-split-last-swap, ordered-all-rev, get-rev, array-split-into-subarrays, array-le-same-prepart,
list-del/natarray-oarray-sort/get-append-less is used by rev-subarray-split-step,
list-del/natarray-oarray-sort/get-last is used by get-rev,
list-del/natarray-oarray-sort/get-numrec is used by ordered-all-rev,
list-del/natarray-oarray-sort/get-succ is used by subarray-inc-offset, ordered-all-rev, get-rev, array-le-swap, array-le-one-diffrent-position,
list-del/natarray-oarray-sort/get-zero is used by rev-subarray-last, ordered-all-rev, get-rev, array-le-swap, array-le-one-diffrent-position,
list-del/natarray-oarray-sort/get-zero-01 is used by next-proper-permutation, next-perm, array-le-one-diffrent-position,
list-del/natarray-oarray-sort/one-03 is used by subarray-inc-offset0, subarray-inc-offset, subarray-inc, ordered-all-rev, array-le-one-diffrent-position,
list-del/natarray-oarray-sort/put-length is used by remains-ordered-by-swap, next-proper-permutation, next-perm,
list-del/natarray-oarray-sort/put-succ is used by array-le-swap,
list-del/natarray-oarray-sort/put-zero is used by array-le-swap,

Used from specification array

array/natarray/Extension is used by subarray-write-above, subarray-prefix-fistn, subarray-inc-offset0, subarray-inc-offset, subarray-inc, rev-subarray-split-step, rev-subarray-split-last-swap, rev-subarray-last, rev-mkarray-empty, next-proper-permutation, array-split-into-subarrays, array-le-same-prepart, array-le-one-diffrent-position,
array/natarray/Put-other is used by rev-subarray-split-step, rev-subarray-split-last-swap, remains-ordered-by-swap,
array/natarray/cputput-reverse is used by next-proper-permutation,
array/natarray/Put-other is used by subarray-write-above, remains-ordered-by-swap, next-proper-permutation,
array/natarray/Put-same is used by next-proper-permutation,
array/natarray/Size-mkarray is used by rev-mkarray-empty,
array/natarray/Size-put is used by rev-subarray-split-step, rev-subarray-split-last-swap, remains-ordered-by-swap, next-proper-permutation, next-perm,
array/natarray/cgetput is used by rev-subarray-split-step, rev-subarray-split-last-swap, remains-ordered-by-swap, next-proper-permutation,
array/natarray/eq-write-left is used by next-proper-permutation,
array/natarray/ngp-06 is used by next-proper-permutation,
array/natarray/ngp-07 is used by next-proper-permutation,
array/natarray/ngp-08 is used by next-proper-permutation,
array/natarray/ngp-09 is used by next-proper-permutation,
array/natarray/put-same-content is used by next-proper-permutation, array-le-swap,

Used from specification array-listops

array-listops/natarray/nil is used by ordered-step-down, next-proper-permutation,