[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-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 nat

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

Used from specification list-last

list-last/mk-rec is used by perm-mklist, ocs-same-length-mklist, ocs-same-length-all, ocs-mklist,
list-last/mk-elem is used by perm-mklist, ocs-mklist,
list-last/mk-empty is used by perm-mklist,
list-last/mk-zero is used by perm-mklist, ocs-same-length-mklist, ocs-same-length-all, ocs-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 list-data

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

Used from specification list

list/In is used by subsize,
list/c-06 is used by ocs-same-length-mklist, ocs-same-length-all,
list/Last is used by perm-rev,
list/Nil is used by subapp-01, subapp, shift-03, perm-same-prefix, perm-last-rec, ocappend, app-04,
list/a is used by subsize, subrec-01, subrec, subdel-01, subapp-03, subapp-02, subapp-01, subapp, shift-03, shift-02, shift-01, shift, rest, rec-01, rec, perm-shift-out2, perm-shift-in2, perm-same-prefix, perm-rmv-in-list, perm-rmv-in, perm-rmdup-rev, perm-rev, perm-rec, perm-one, perm-mklist-del, perm-mklist, perm-last-rec, perm-l, perm-dups-03, perm-dups-02, perm-dups, perm-com2, perm-com1, papp-03, papp-02, papp-01, papp, one-01, one, ocs-same-length-mklist, ocs-same-length-all, ocs-put-02, ocs-put-01, ocs-put, ocs-not-more, ocs-mklist, ocs-dups-ex, ocs-del1, ocs-del-length, ocs-del-del1, ocnodups, ocappend, oc-filt, oc-dups, oc-diff-01, oc-del-01, oc-adjoin, notin, in-put, in-05, in-03, in-02, in-01, empty-01, delapp, del1-01, del1, del-03, del-01, del, cons, c, app-05, app-04, app-03, app-02, app-01, app, adjoin, ad, a,
list/app is used by perm-one, perm-mklist-del, one-01, one,
list/app-08 is used by ocs-mklist, ocs-del-del1,
list/c is used by subsize, subrec-01, subapp-01, subapp, shift-03, perm-rmv-in, perm-rmdup-rev, perm-rev, perm-one, perm-mklist-del, perm-mklist, perm-last-rec, perm-dups, ocs-same-length-mklist, ocs-same-length-all, ocs-put-02, ocs-put-01, ocs-put, ocs-not-more, ocs-mklist, ocs-dups-ex, ocs-del1, ocs-del-length, ocs-del-del1, ocnodups, ocappend, oc-filt, oc-dups, oc-diff-01, oc-adjoin, notin, in-put, in-05, empty-01, delapp, del1-01, del1, app-04, app-03, adjoin,
list/c-03 is used by perm-one,
list/c-04 is used by perm-one,
list/c-07 is used by ocs-put-02, ocs-put-01, ocs-put,
list/e is used by perm-one, perm-last-rec,
list/e-01 is used by subsize, perm-mklist, ocs-put-02, ocs-put-01, ocs-put, ocs-mklist, empty-01, delapp, app-04, app-03,
list/in-01 is used by rec, perm-mklist, ocs-dups-ex, ocs-del1, in-put,
list/in-06 is used by perm-mklist-del, notin, 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, in-put,
list/in-14 is used by perm-mklist, ocs-mklist,
list/in-17 is used by perm-one, perm-last-rec, ocs-dups-ex, ocs-del1, oc-dups, in-put,
list/in-append is used by shift-03, ocs-dups-ex, ad,
list/in-empty is used by perm-mklist, perm-last-rec, ocs-same-length-all, ocs-dups-ex, ocs-del1, in-05, empty-01,
list/in-rec is used by subrec-01, shift-03, ocs-same-length-all, ocs-not-more, ocs-dups-ex, ocs-del1, oc-dups, in-05, del1,
list/len is used by subsize,
list/len-02 is used by subsize,
list/len-05 is used by ocs-same-length-mklist, ocs-same-length-all, ocs-put-02, ocs-put-01, ocs-put, ocs-not-more, in-put,

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 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 nat-basic2

nat-basic2/a is used by subsize, subrec-01, subrec, subdel-03, subdel-01, subapp-03, subapp-02, rest, perm-put-del1, perm-mklist, perm-dups, one, ocs-sw, ocs-same-length-mklist, ocs-same-length-all, ocs-put-02, ocs-put-01, ocs-put, ocs-not-more, ocs-mklist, ocs-dups-ex, ocs-del1, ocs-del-length, ocs-del-del1, ocnodups, ocappend, oc-filt, oc-dups, oc-diff-01, oc-del-02, oc-del-01, oc-del, notin, in-put, in-05, in-01, delapp, del1-01, del1, del-05, del-04, del-02, c, app-03, app-02, app-01, app, ad,
nat-basic2/add-base is used by subrec-01, subrec, perm-put-del1, perm-mklist, ocs-sw, ocs-same-length-mklist, ocs-same-length-all, ocs-put-02, ocs-put-01, ocs-not-more, ocs-mklist, ocs-del-length, ocs-del-del1, ocnodups, ocappend, oc-filt, oc-dups, oc-diff-01, oc-del-01, notin, in-put, del1-01, del1,
nat-basic2/c is used by subsize, subrec-01, subrec, subdel-03, subdel-01, subapp-03, subapp-02, shift-02, rest, perm-put-del1, perm-mklist, perm-dups, one, ocs-sw, ocs-same-length-mklist, ocs-same-length-all, ocs-put-02, ocs-put-01, ocs-put, ocs-not-more, ocs-mklist, ocs-dups-ex, ocs-del1, ocs-del-length, ocs-del-del1, ocnodups, ocappend, oc-filt, oc-dups, oc-diff-01, oc-del-02, oc-del-01, oc-del, notin, in-put, in-05, in-01, delapp, del1-01, del1, del-05, del-04, del-02, c, app-03, app-02, app-01, app, ad,
nat-basic2/eq is used by ocs-sw, ocs-put-01, del-05,
nat-basic2/eq-01 is used by ocs-same-length-mklist, ocs-put-01, ocs-put, ocs-del-length, ocappend, oc-filt, oc-diff-01, del1-01, del1, del-04,
nat-basic2/l is used by subdel-01, ocs-not-more, ad,
nat-basic2/l-01 is used by oc-dups,
nat-basic2/l-02 is used by subapp-03, subapp-02, oc-del, delapp,
nat-basic2/nls-fst is used by ocs-not-more,
nat-basic2/one is used by subdel-01, ocs-dups-ex, ocs-del1, oc-dups, in-put,
nat-basic2/one-03 is used by ocs-del-del1,
nat-basic2/oz is used by subrec, perm-mklist, ocs-same-length-mklist, ocs-same-length-all, ocs-put-02, ocs-put-01, ocs-put, ocs-not-more, ocs-mklist, oc-del-01, in-put, app-03,
nat-basic2/pred is used by perm-put-del1,
nat-basic2/s is used by subsize, subrec, subdel-01, ocs-same-length-mklist, ocs-put-02, ocs-put-01, ocs-put, in-put, del-02, ad,
nat-basic2/succ is used by subrec, perm-mklist, ocs-same-length-mklist, ocs-same-length-all, ocs-put-02, ocs-put-01, ocs-put, ocs-not-more, in-put,
nat-basic2/z is used by subsize, delapp,
nat-basic2/z-01 is used by subdel-01, perm-mklist, ocs-same-length-mklist, ocs-same-length-all, ocs-mklist, oc-del-01, in-05, del1, ad,

Used from specification nat-basic1

nat-basic1/f is used by trans, subsize, subrec, subdel-01, subdel, subapp-03, subapp-02, sub-del-any, size-perm, perm-switch, perm-put-del1, perm-put, perm-all, ocs-sw, ocs-put-02, ocs-put-01, ocs-put, ocs-not-more, oc-dups, oc-del-02, oc-del, oc, nodups, l, in-put, filter, diff, delapp, del-02, del, c, app-02, app-01, app, ad,
nat-basic1/less-1 is used by subsize, delapp,
nat-basic1/lf is used by subrec,
nat-basic1/lf-01 is used by size-perm, perm-all, nodups,
nat-basic1/lf-02 is used by perm-all, ocs-sw, nodups,
nat-basic1/ls-02 is used by perm-all, l,
nat-basic1/one is used by ocs-dups-ex, ocs-del1, ocone, ocnodups, in-put,
nat-basic1/one-01 is used by subrec, subdel-03, subdel-02, subdel-01, size-perm, ocs-sw, ocone, ocnodups-01, oc-dups, oc-del-02, oc-del, nodups, delapp, del-02, del, ad,
nat-basic1/ref-1 is used by subsize, subdel-01, rest, ref, perm-all, ocs-same-length-mklist, oc-del, oc, del-02, ad,
nat-basic1/trans-1 is used by subrec,
nat-basic1/z is used by nodups,
nat-basic1/zero is used by subdel-03, size-perm, filter, diff,
nat-basic1/zero-01 is used by subdel-03, ocs-put-02, oc-dups,

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-02, ocs-put-01, 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-mklist, ocs-del-length, ocs-del-del1,
list-del/del-y is used by ocs-mklist, ocs-del-length, ocs-del-del1,
list-del/del1-del is used by subdel-03, subdel-02,
list-del/del1-e is used by subrec-01, perm-mklist, perm-last-rec, del1-01,
list-del/del1-in is used by shift-03, perm-put-del1, perm-last-rec, del-04, ad,
list-del/del1-n is used by subrec-01, rec, perm-mklist, ocs-del1, ocs-del-del1, del1-01, del1,
list-del/del1-y is used by subrec-01, ocs-del1, ocs-del-del1, del1-01, del1, adjoin,
list-del/get-in is used by perm-put-del1, ocs-sw, ocs-put-02,
list-del/get-succ is used by ocs-put-02,
list-del/get-zero-01 is used by ocs-put-02, ocs-put-01, ocs-put,
list-del/in-01-01 is used by shift-03, perm-put-del1, oc-del-02, oc-del, del-04, ad,
list-del/in-02 is used by perm-del-in, ocs-del,
list-del/in-02-01 is used by subdel-03, subdel-02, shift-03, perm-put-del1, ocs-del1-if, oc-del-01, delapp, del-05, del-04,
list-del/in-03 is used by ocs-del-del1,
list-del/in-04 is used by shift-03,
list-del/in-05 is used by shift-03, ocs-del1,
list-del/in-del-new is used by perm-mklist-del, perm-del-01,
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-02, ocs-put-01, ocs-put,
list-del/put-sw-in is used by perm-switch,
list-del/put-zero is used by ocs-put-02, ocs-put-01, ocs-put, in-put,
list-del/putset-same is used by perm-put-del1, ocs-sw,