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

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-01, subperm,
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 adjoin, oc-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 adjoin, oc-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 ocs-dups-ex, ocnodups, 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-data

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

Used from specification nat-basic

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

Used from specification list

list/c-06 is used by ocs-same-length-mklist, ocs-same-length-all,
list/in-def is used by subsize,
list/Last is used by perm-rev,
list/Nil is used by app-all-end, subapp-01, perm-same-prefix, shift-03, ocappend, app-end-all, perm-last-rec, subapp,
list/a is used by perm-one, del1-01, adjoin, subsize, app-beg-end, perm-dups, ocs-del1, rest, app-all-end, ocs-same-length-mklist, app-end-in, perm-rmdup-rev, app-in-in, ocs-del-del1, ocs-dups-ex, perm-rec, subapp-01, ocnodups, perm-app-right-rev-sym, perm-rmcommon-beg-end, subapp-03, oc-dups, subapp-02, perm-same-prefix, perm-rmcommon-beg-beg, perm-rmcommon-end-end, perm-rev, ocs-mklist, app-attach, del1, app-beg-all, app-end-beg, perm-common-postfix, oc-adjoin, subrec-01, rec, perm-common-prefix, perm-rmv-in, subrec, oc-filt, papp, app-beg-beg, shift-02, oc-del-01, shift-01, perm-rmv-in-list, shift-03, app-beg-in, ocappend, perm-com1, notin, perm-com2, app-end-all, app-all-beg, one-01, subdel-01, perm-dups-03, perm-dups-02, perm-last-rec, one, del-01, c, perm-append-trans-01, a, perm-append-trans-02, ocs-put-01, ocs-put-02, ocs-del-length, ocs-same-length-all, perm-app-right, perm-app-right-rev, in-05, in-01, in-03, in-02, delapp, ocs-put, app-in-end, app-end-end, ocs-not-more, perm-mklist, perm-mklist-del, subapp, perm-shift-out2, perm-app-right-sym, perm-append-le-01, in-put, perm-app-left-rev-sym, perm-app-left-rev, ad, cons, oc-diff-01, rec-01, app-in-beg, empty-01, perm-app-left, perm-shift-in2, del, shift, perm-app-left-sym, perm-append-le-02, papp-02, papp-03, papp-01,
list/app is used by perm-one, app-beg-all, one-01, one, perm-mklist-del,
list/app-01 is used by ocs-del-del1, ocs-mklist,
list/c is used by perm-one, del1-01, adjoin, subsize, perm-dups, ocs-del1, app-all-end, ocs-same-length-mklist, perm-rmdup-rev, ocs-del-del1, ocs-dups-ex, subapp-01, ocnodups, oc-dups, perm-rev, ocs-mklist, del1, oc-adjoin, subrec-01, perm-rmv-in, oc-filt, shift-03, ocappend, notin, app-all-beg, perm-last-rec, ocs-put-01, ocs-put-02, ocs-del-length, ocs-same-length-all, in-05, delapp, ocs-put, ocs-not-more, perm-mklist, perm-mklist-del, subapp, in-put, oc-diff-01, empty-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-01, ocs-put-02, ocs-put,
list/e is used by perm-one, perm-last-rec,
list/e-01 is used by subsize, app-all-end, ocs-mklist, app-all-beg, ocs-put-01, ocs-put-02, delapp, ocs-put, perm-mklist, empty-01,
list/in-01 is used by ocs-del1, ocs-dups-ex, rec, perm-mklist, in-put,
list/in-06 is used by notin, perm-mklist-del, in-put,
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 perm-one, ocs-del1, ocs-dups-ex, oc-dups, del1, subrec-01, shift-03, perm-last-rec, ocs-same-length-all, in-05, ocs-not-more, in-put,
list/in-append is used by ocs-del1, ocs-dups-ex, del1, subrec-01, shift-03, ocs-same-length-all, in-05, ocs-not-more,
list/in-empty is used by ocs-del1, ocs-dups-ex, oc-dups, perm-last-rec, ocs-same-length-all, in-05, perm-mklist, empty-01,
list/in-rec is used by ocs-dups-ex, oc-dups,
list/len is used by subsize, ocs-same-length-mklist, ocs-put-01, ocs-same-length-all, ocs-put, ocs-not-more, perm-append-le-01, in-put, perm-append-le-02,
list/len-02 is used by subsize, ocs-same-length-mklist, ocs-put-01, ocs-same-length-all, ocs-put, ocs-not-more, in-put,
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/get-rec is used by ocs-put-01, ocs-put-02, ocs-put,
list-del/in-del-new is used by perm-del-01,
list-del/put-at is used by ocs-sw,
list-del/put-rec-02 is used by ocs-put-02, in-put,
list-del/rmdup-del1-del is used by perm-rmdup-rev,
list-del/sw-02 is used by shift-03, perm-last-rec,
list-del/app is used by subapp,
list-del/del-e is used by ocs-mklist, ocs-del-length,
list-del/del-n is used by ocs-del-del1, ocs-mklist, ocs-del-length,
list-del/del-y is used by ocs-del-del1, ocs-mklist, ocs-del-length,
list-del/del1-del is used by subdel-02, subdel-03,
list-del/del1-e is used by del1-01, subrec-01, perm-last-rec, perm-mklist,
list-del/del1-in is used by shift-03, perm-last-rec, del-04, perm-put-del1,
list-del/del1-n is used by del1-01, ocs-del1, ocs-del-del1, del1, subrec-01, rec, perm-mklist,
list-del/del1-y is used by del1-01, adjoin, ocs-del1, ocs-del-del1, del1, subrec-01,
list-del/get-in is used by ocs-sw, ocs-put-02, perm-put-del1,
list-del/get-succ is used by ocs-put-02,
list-del/get-zero is used by ocs-put-01, ocs-put-02, ocs-put,
list-del/in-01-01 is used by oc-del-02, shift-03, subdel-02, del-04, oc-del, perm-put-del1,
list-del/in-02 is used by perm-del-in, ocs-del,
list-del/in-02-01 is used by oc-del-01, shift-03, subdel-03, del-04, del-05, delapp, perm-put-del1, ocs-del1-if,
list-del/in-03 is used by ocs-del-del1, subdel-03,
list-del/in-05 is used by ocs-del1, shift-03,
list-del/in-del-new is used by perm-del-01, sub-del, perm-mklist-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-length is used by ocs-sw,
list-del/put-same is used by ocs-sw,
list-del/put-succ is used by ocs-put-01, ocs-put-02, ocs-put,
list-del/put-sw-in is used by perm-swap, perm-switch,
list-del/put-zero is used by ocs-put-01, ocs-put-02, ocs-put, in-put,
list-del/putset-same is used by ocs-sw, perm-put-del1,