[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 list-last

list-last/mk-rec is used by ocs-same-length-all, ocs-same-length-mklist, ocs-mklist, perm-mklist,
list-last/mk-elem is used by ocs-mklist, perm-mklist,
list-last/mk-empty is used by perm-mklist,
list-last/mk-zero is used by ocs-same-length-all, ocs-same-length-mklist, ocs-mklist, perm-mklist,
list-last/rev-e is used by perm-rmdup-rev, perm-rev,
list-last/rev-empty is used by perm-rmdup-rev,
list-last/rev-in is used by perm-rmdup-rev,
list-last/rev-r is used by perm-rev,

Used from specification nat

nat/add-01 is used by ocs-sw, ocs-same-length-all, ocs-same-length-mklist, perm-put-del1, ocs-mklist, ocs-put-02, oc-del-01, perm-mklist,
nat/add-num-01 is used by ocs-put,
nat/add-num-03 is used by ocs-dups-ex,
nat/elim-pred-c is used by ocs-put, in-put, del-04, ocs-put-01, del-05, perm-put-del1, ocs-put-02, oc-del-01, del1,
nat/eq-02 is used by ocs-sw,
nat/fle is used by oc-del-02, subsize, subdel-01, del-02, subapp-02, subdel, subapp-03, oc, trans,
nat/fle-01 is used by subsize, oc,
nat/gr-def is used by ocs-dups-ex,
nat/le-add is used by delapp, app-all-beg,
nat/le-def is used by ocs-sw, rest, del, app-beg-end, subdel-03, app-end-end, delapp, c, subrec-01, oc-del-02, ocnodups, subsize, oc-del, subdel-01, del-02, perm-all, subrec, nodups, subapp-02, size-perm, ocnodups-01, ocone, ref, app-beg-beg, subdel, subdel-02, subapp-03, diff, sub-del, filter, trans, ad,
nat/le-ls-simp is used by app-beg-end, subdel-03, app-end-end, c, oc-del-02, perm-all, subrec, app-beg-beg, diff, filter, trans,
nat/le-num-06 is used by perm-dups, in-01, subrec,
nat/le-one is used by subdel-02,
nat/lels is used by ocs-sw, ocs-put, in-put, subdel-03, ocs-put-01, subsize, subrec, ocs-put-02,
nat/lels-02 is used by l, perm-all, ocone,
nat/lep is used by app-all-beg,
nat/lep-02 is used by rest, app-beg-end, app-end-end, c, subrec-01, subsize, app-beg-beg, ad,
nat/ler is used by delapp, perm-all,
nat/let is used by subdel-03,
nat/lez is used by in-put, subrec-01, subempty, diff, filter,
nat/lez-01 is used by subdel-03, ocnodups, subsize, in, diff, filter,
nat/ls is used by delapp, oc-del-02, oc-del,
nat/ls-01 is used by subdel-01, del-02, ad,
nat/ls-02 is used by subdel-03, delapp, subrec, subdel-02,
nat/ls-03 is used by del, del-02, subdel-02, ad,
nat/ls-le-simp is used by ocs-sw, del, del-02, subrec, subdel-02, sub-del,
nat/one-02 is used by ocnodups,
nat/pred-03 is used by ocs-sw, in-put, del-04, del, subdel-03, delapp, oc-del-02, del-05, oc-del, subdel-01, del-02, perm-put-del1, subrec, ocs-put-02, subdel-02, ocs-del1-if, oc-del-01, del1, ad,
nat/sub-ls is used by subdel-03, oc-del-02, subrec, ad,
nat/succ-01 is used by ocs-put, in-put, subdel-03, delapp, ocs-put-01, subsize, subrec, ocs-put-02, subdel-02,

Used from specification list-set

list-set/diff-y is used by oc-diff-01,
list-set/filt-y is used by oc-filt,
list-set/subset is used by subperm, subperm-01,
list-set/diff-e is used by oc-diff-01,
list-set/diff-n is used by oc-diff-01,
list-set/filt-e is used by oc-filt,
list-set/filt-n is used by oc-filt,
list-set/notin-01 is used by oc-diff,
list-set/notin-02 is used by oc-filt-01,
list-set/sub-in is used by subperm-01,
list-set/sub-notin is used by subperm,

Used from specification list-dup

list-dup/adjoin-notin is used by oc-adjoin, adjoin,
list-dup/dups is used by perm-dups, ocs-dups-ex,
list-dup/dups-eqsize-02 is used by size-perm,
list-dup/adjoin-in is used by oc-adjoin, adjoin,
list-dup/app-01-02 is used by perm-dups-03,
list-dup/app-05 is used by perm-dups-02,
list-dup/in-08 is used by adjoin,
list-dup/rec is used by ocnodups, ocs-dups-ex, oc-dups,
list-dup/rm-empty is used by perm-rmdup-rev,
list-dup/rm-in-02 is used by perm-rmdup-rev,
list-dup/rmdup-e is used by perm-rmdup-rev,

Used from specification list-getput

list-getput/get-rec is used by ocs-put, ocs-put-01, ocs-put-02,
list-getput/put-at is used by ocs-sw,
list-getput/put-length is used by ocs-sw,
list-getput/put-same is used by ocs-sw,
list-getput/putset-same is used by ocs-sw, perm-put-del1,

Used from specification list-data

list-data/elim-list-c is used by delapp, perm-mklist,
list-data/l is used by ocs-sw, ocs-put, in-put, perm-swap, l, ocs-put-01, subsize, perm-put-del1, perm-put, ocs-put-02, perm-switch,
list-data/size-nil is used by ocs-same-length-all, ocs-not-more, ocs-same-length-mklist, subsize, ocs-put-02,

Used from specification nat-basic

nat-basic/a is used by ocs-sw, ocs-put, ocs-same-length-all, rest, in-put, del-04, app-beg-end, subdel-03, app-end-end, oc-diff-01, delapp, ocs-not-more, c, ocs-put-01, subrec-01, perm-dups, oc-del-02, ocs-same-length-mklist, ocnodups, subsize, ocappend, del-05, oc-del, in-01, subdel-01, ocs-del-length, del-02, perm-put-del1, subrec, subapp-02, ocs-mklist, ocs-put-02, ocs-del-del1, app-beg-beg, subdel-02, oc-filt, in-05, subapp-03, ocs-del1, ocs-dups-ex, one, oc-del-01, app-all-beg, perm-mklist, notin, del1, oc-dups, del1-01, ad,
nat-basic/add-base is used by ocs-sw, ocs-put, ocs-same-length-all, in-put, oc-diff-01, ocs-not-more, ocs-put-01, subrec-01, ocs-same-length-mklist, ocnodups, ocappend, ocs-del-length, perm-put-del1, subrec, ocs-mklist, ocs-put-02, ocs-del-del1, oc-filt, oc-del-01, perm-mklist, notin, del1, oc-dups, del1-01,
nat-basic/c is used by ocs-sw, ocs-put, ocs-same-length-all, rest, in-put, del-04, app-beg-end, subdel-03, app-end-end, oc-diff-01, delapp, ocs-not-more, c, ocs-put-01, subrec-01, perm-dups, oc-del-02, ocs-same-length-mklist, ocnodups, subsize, ocappend, del-05, oc-del, in-01, subdel-01, ocs-del-length, del-02, perm-put-del1, subrec, subapp-02, ocs-mklist, shift-02, ocs-put-02, ocs-del-del1, app-beg-beg, subdel-02, oc-filt, in-05, subapp-03, ocs-del1, ocs-dups-ex, one, oc-del-01, app-all-beg, perm-mklist, notin, del1, oc-dups, del1-01, ad,
nat-basic/eq-01 is used by ocs-put, del-04, oc-diff-01, ocs-put-01, ocs-same-length-mklist, ocappend, ocs-del-length, oc-filt, del1, del1-01,
nat-basic/eq-02 is used by ocs-sw, del-05,
nat-basic/f is used by ocs-sw, ocs-put, in-put, perm-swap, del, app-beg-end, subdel-03, app-end-end, delapp, l, ocs-not-more, c, ocs-put-01, oc-del-02, subsize, oc-del, subdel-01, del-02, perm-put-del1, perm-all, subrec, nodups, subapp-02, perm-put, size-perm, ocs-put-02, app-beg-beg, subdel, subdel-02, subapp-03, diff, sub-del, oc, filter, trans, perm-switch, oc-dups, ad,
nat-basic/l is used by ocs-not-more, subdel-01, ad,
nat-basic/l-02 is used by delapp, oc-del, subapp-02, subapp-03,
nat-basic/less-zero is used by delapp, subsize, ocs-put-02,
nat-basic/lf is used by subdel-03, subrec,
nat-basic/lf-01 is used by perm-all,
nat-basic/lf-02 is used by ocs-sw, perm-all,
nat-basic/ls-02 is used by l, perm-all,
nat-basic/nls-fst is used by ocs-not-more,
nat-basic/one is used by in-put, ocnodups, ocone, ocs-del1, ocs-dups-ex,
nat-basic/one-01 is used by ocs-sw, del, subdel-03, delapp, oc-del-02, oc-del, subdel-01, del-02, subrec, nodups, size-perm, ocnodups-01, ocone, subdel-02, oc-dups, ad,
nat-basic/one-03 is used by in-put, ocs-del1, ocs-dups-ex, oc-dups,
nat-basic/one-06 is used by ocs-del-del1,
nat-basic/oz is used by ocs-put, ocs-same-length-all, in-put, ocs-put-01, ocs-same-length-mklist, ocs-mklist, ocs-put-02, oc-del-01, app-all-beg, perm-mklist, del1,
nat-basic/pred is used by perm-put-del1,
nat-basic/refl-nat is used by rest, ocs-same-length-mklist, subsize, oc-del, subdel-01, del-02, perm-all, ref, subdel-02, oc, ad,
nat-basic/s-04 is used by ocs-put, in-put, ocs-put-01, ocs-same-length-mklist, subsize, subdel-01, del-02, subrec, ocs-put-02, ad,
nat-basic/succ is used by subdel-03, subrec, ocs-put-02, perm-mklist,
nat-basic/trans-nat is used by subdel-03, subrec,
nat-basic/z-01 is used by subdel-01, in-05, oc-del-01, ad,
nat-basic/z-02 is used by delapp, subsize,
nat-basic/zero is used by diff, filter,

Used from specification list

list/c-06 is used by ocs-same-length-all, ocs-same-length-mklist,
list/in-def is used by subsize,
list/Last is used by perm-rev,
list/Nil is used by subapp-01, subapp, app-all-end, ocappend, perm-same-prefix, perm-last-rec, app-end-all, shift-03,
list/a is used by ocs-put, del-01, ocs-same-length-all, rest, app-end-in, papp-01, subapp-01, in-put, in-03, perm-common-postfix, del, app-beg-end, perm-rmdup-rev, app-end-end, subapp, oc-diff-01, delapp, ocs-not-more, one-01, shift, c, perm-mklist-del, ocs-put-01, subrec-01, app-all-end, papp, perm-dups, shift-01, ocs-same-length-mklist, ocnodups, app-in-in, perm-dups-03, oc-adjoin, subsize, ocappend, in-01, subdel-01, ocs-del-length, papp-02, subrec, perm-same-prefix, adjoin, a, subapp-02, perm-rmcommon-beg-beg, perm-shift-out2, app-beg-in, perm-rec, perm-rmv-in, perm-one, app-in-beg, perm-last-rec, ocs-mklist, shift-02, perm-com1, ocs-put-02, app-beg-all, ocs-del-del1, perm-common-prefix, in-02, perm-rmv-in-list, app-beg-beg, app-attach, cons, oc-filt, in-05, perm-com2, subapp-03, app-end-all, rec, ocs-del1, perm-rmcommon-beg-end, ocs-dups-ex, shift-03, papp-03, perm-rmcommon-end-end, one, app-in-end, perm-rev, oc-del-01, rec-01, app-all-beg, perm-shift-in2, perm-mklist, notin, del1, empty-01, perm-dups-02, app-end-beg, oc-dups, del1-01, ad,
list/app is used by one-01, perm-mklist-del, perm-one, app-beg-all, one,
list/app-01 is used by ocs-mklist, ocs-del-del1,
list/c is used by ocs-put, ocs-same-length-all, subapp-01, in-put, perm-rmdup-rev, subapp, oc-diff-01, delapp, ocs-not-more, perm-mklist-del, ocs-put-01, subrec-01, app-all-end, perm-dups, ocs-same-length-mklist, ocnodups, oc-adjoin, subsize, ocappend, ocs-del-length, adjoin, perm-rmv-in, perm-one, perm-last-rec, ocs-mklist, ocs-put-02, ocs-del-del1, oc-filt, in-05, ocs-del1, ocs-dups-ex, shift-03, perm-rev, app-all-beg, perm-mklist, notin, del1, empty-01, oc-dups, del1-01,
list/c-03 is used by perm-one,
list/c-04 is used by perm-one,
list/c-07 is used by ocs-put, ocs-put-01, ocs-put-02,
list/e is used by perm-one, perm-last-rec,
list/e-01 is used by ocs-put, delapp, ocs-put-01, app-all-end, subsize, ocs-mklist, ocs-put-02, app-all-beg, perm-mklist, empty-01,
list/in-01 is used by in-put, rec, ocs-del1, ocs-dups-ex, perm-mklist,
list/in-06 is used by in-put, perm-mklist-del, notin,
list/in-10 is used by adjoin,
list/in-11 is used by subapp,
list/in-12 is used by subapp-01, oc-del-01,
list/in-14 is used by ocs-mklist, perm-mklist,
list/in-17 is used by ocs-same-length-all, in-put, ocs-not-more, subrec-01, perm-one, perm-last-rec, in-05, ocs-del1, ocs-dups-ex, shift-03, del1, oc-dups,
list/in-append is used by ocs-same-length-all, ocs-not-more, subrec-01, in-05, ocs-del1, ocs-dups-ex, shift-03, del1,
list/in-empty is used by ocs-same-length-all, perm-last-rec, in-05, ocs-del1, ocs-dups-ex, perm-mklist, empty-01, oc-dups,
list/in-rec is used by ocs-dups-ex, oc-dups,
list/len is used by ocs-put, ocs-same-length-all, in-put, ocs-not-more, ocs-put-01, ocs-same-length-mklist, subsize,
list/len-02 is used by ocs-put, ocs-same-length-all, in-put, ocs-not-more, ocs-put-01, ocs-same-length-mklist, subsize,
list/len-05 is used by ocs-put-02,

Used from specification list-del

list-del/del-n is used by ocs-del-length,
list-del/del-rev is used by perm-rmdup-rev,
list-del/del1-del-switch is used by perm-mklist-del,
list-del/del1-empty is used by perm-last-rec,
list-del/del1-first is used by perm-mklist,
list-del/del1-n is used by del1-01,
list-del/in-del-new is used by perm-del-01,
list-del/put-rec-02 is used by in-put, ocs-put-02,
list-del/rmdup-del1-del is used by perm-rmdup-rev,
list-del/sw-02 is used by perm-last-rec, shift-03,
list-del/app is used by subapp,
list-del/del-e is used by ocs-del-length, ocs-mklist,
list-del/del-n is used by ocs-del-length, ocs-mklist, ocs-del-del1,
list-del/del-y is used by ocs-del-length, ocs-mklist, ocs-del-del1,
list-del/del1-del is used by subdel-03, subdel-02,
list-del/del1-e is used by subrec-01, perm-last-rec, perm-mklist, del1-01,
list-del/del1-in is used by del-04, perm-put-del1, perm-last-rec, shift-03,
list-del/del1-n is used by subrec-01, ocs-del-del1, rec, ocs-del1, perm-mklist, del1, del1-01,
list-del/del1-y is used by subrec-01, adjoin, ocs-del-del1, ocs-del1, del1, del1-01,
list-del/get-in is used by ocs-sw, perm-put-del1, ocs-put-02,
list-del/get-succ is used by ocs-put-02,
list-del/get-zero is used by ocs-put, ocs-put-01, ocs-put-02,
list-del/in-01-01 is used by del-04, oc-del-02, oc-del, perm-put-del1, subdel-02, shift-03,
list-del/in-02 is used by perm-del-in, ocs-del,
list-del/in-02-01 is used by del-04, subdel-03, delapp, del-05, perm-put-del1, ocs-del1-if, shift-03, oc-del-01,
list-del/in-03 is used by subdel-03, ocs-del-del1,
list-del/in-05 is used by ocs-del1, shift-03,
list-del/in-del-new is used by perm-mklist-del, perm-del-01, sub-del,
list-del/one-01 is used by perm-one, perm-last-rec,
list-del/put-del1-in is used by perm-put-del1,
list-del/put-in is used by perm-put-del1,
list-del/put-in-02 is used by perm-put,
list-del/put-succ is used by ocs-put, ocs-put-01, ocs-put-02,
list-del/put-sw-in is used by perm-swap, perm-switch,
list-del/put-zero is used by ocs-put, in-put, ocs-put-01, ocs-put-02,