[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

nat/add-01 is used by lastn-mklist, lastN-rest, l-01, firstn-last-01, firstn-butlast, firstn-append-01, first-mklist, blastN-firstN,
nat/anti is used by lastN-dups-01, lastN-dups, firstn-last-01,
nat/cancel-01 is used by firstn-last-01, firstn-butlast, firstn-append-01, blastN-firstN,
nat/elim-pred-c is used by sublist-rec-01, sublist-rec, sublist-prefix, sublist-part, sublist-num-01, sublist-move, sublist-firsteq, sublist-append-04, size-rmdup-del, size-del-nodups, rmpos-size, rmpos-in, rmpos-get, restn-nonempty-2, restn-nonempty, restn-last, restn-first-get, restn-empty, restN-dups, rest-rec, put-sw-in, put-rec-02, put-rec-01, put-rec, put-length, put-in-02, put-in-01, put-in, put-del1-in, put-at-eq, put-at, put-app-left, pos-get, num-lastN, lastn-restn, lastn-rec, lastn-lastn-01, lastn-app, lastN-blastN, l-02, l, get-numrec, get-nodups, get-last-nonempty, get-last-04, get-in, get-firstn, get-butlast, get-append-less, get-add-num, firstn-twice, firstn-prefix, firstn-last-rec, firstn-last, firstn-firstn, firstn-butlast, firstn-append-01, firstN-rec-01, firstN-num-rec, firstN-lastN, first-num, first-mklist, dups-def, at-last,
nat/elim-sub is used by sublist-mklist, sublist-first-skip, sublist-append-02, sublist-append-01, restn-firstn-better, restn-firstn, rest-sub, rest-mklist, rest-len, rest-app, put-app-right, lastn-restn-01, lastn-app, lastN-ex, get-rec, get-append-grt, firstn-last-eq, firstn-last-01, firstn-butlast, firstn-append-01, firstn-app-02, firstn-app-01, firstN-lastN, append-mod,
nat/eq is used by get-last-04,
nat/eq-01 is used by sublist-restn-02, lastn-mklist-01, lastN-ex, lastN-append, get-append-grt-02, firstn-length-02, firstn-last-eq, firstn-append-01, firstN-lastN, elim-lastn-butlastn,
nat/eq-02 is used by size-del-nodups, rmpos-size, l,
nat/eqle-one is used by lastn-mklist, get-last-04,
nat/fle is used by sublist-mklist-01, sublist-lenrec, sublist-at, rmpos-get, lastN-append-01, get-firstn, firstn-firstn,
nat/fle-01 is used by sublist-mklist-01, sublist-mklist, sublist-first-skip, sublist-at, rmpos-get, rest-mklist-01, rest-append, lastn-restn, first-mklist-01, first-append-01, append-mod,
nat/ge is used by firstn-length,
nat/gr-def is used by firstn-length-01,
nat/l-num-06 is used by get-mklist-01,
nat/le-ls-simp is used by sublist-lenrec, sublist-first-skip, sublist-at, rmpos-size, rmpos-get, restn-at, get-firstn, firstn-last-rec, firstn-firstn, firstN-in-02, first-append-01,
nat/le-num-02 is used by restn-firstn,
nat/le-num-06 is used by restn-firstn,
nat/lels is used by sublist-prefix, sublist-lenrec-01, sublist-lenrec, rmtoobigpos, rmpos-size, rmpos-in, rmpos-get, restn-nonempty-2, restn-nonempty, restn-less, restn-last, restn-firstn-better, restn-first-get, restn-empty, restn-at, restN-append, put-sw-in, put-length, put-in-02, put-in-01, put-in, put-firstn-restn, put-del1-in, put-at-eq, put-at, put-app-left, pos-get, nodups-rmposnodups, lastn-restn, lastn-neq-01, lastn-mklist, lastn-lastn-01, lastN-rest, lastN-dups-01, lastN-dups, lastN-append-01, inl, get-nodups, get-last-04, get-in, get-firstn, get-butlast, get-append-less, get-append-grt, firstn-restn-in, firstn-restn-eq, firstn-length-01, firstn-last-rec, firstn-last-01, firstn-last, firstn-firstn, firstn-butlast-intro, firstN-dups-04, first-append, dups-def, blastN-firstN,
nat/lels-01 is used by sublist-restn-02, sublist-mklist-01, sublist-mklist, sublist-first-skip, sublist-at, size-del-nodups, rmpos-size, restN-len, rest-mklist-02, rest-mklist-01, rest-append, put-last, put-firstn-restn, len, lastn-restn-01, lastn-mklist-01, lastn-app, lastN-rest, lastN-ex, lastN-append, lastN-all, l, get-rec, get-mklist-01, get-mklist, firstn-prefix-04, firstn-prefix-03, firstn-prefix-02, firstn-last-eq, firstn-last-01, firstn-butlast, firstn-append-01, firstN-lastN, firstN-in-02, first-mklist-03, first-mklist-02, first-mklist-01, first-append-01, elim-lastn-butlastn, delete-one-le, del-rmdup-length-nle,
nat/lels-02 is used by restn-empty, blastN-firstN,
nat/lels-03 is used by rmpos-get, restn-firstn, lastN-in, firstn-last-01, firstn-at-in-dups, firstN-lastN-in-01, firstN-in-03, firstN-in-01, firstN-dups-05, firstN-dups-01, firstN-dups,
nat/lep is used by sublist-mklist, sublist-first-skip, sublist-append-01, restn-firstn-better, restn-firstn, rest-sub, rest-len, rest-in, rest-app, put-firstn-restn, put-app-right, lastn-restn-01, lastn-app, lastN-in-01, lastN-ex, get-append-grt, firstn-length, firstn-last-eq, firstn-app-02, firstN-lastN, firstN-in-03, firstN-in-02, firstN-in, elim-lastn-butlastn, append-mod,
nat/lep-02 is used by sublist-move, sublist-mklist, sublist-first-skip, sublist-append-04, restN-dups, rest-app, lastn-restn, lastN-blastN, get-firstn, firstn-twice, firstn-prefix, firstn-length, firstn-firstn, first-mklist, blastN-firstN,
nat/ler is used by put-firstn-restn, blastN-firstN,
nat/les is used by lastn-mklist, get-last-04,
nat/let is used by sublist-move, sublist-first-skip, restn-firstn-better, rest-app, get-firstn, firstn-firstn, firstn-app-02,
nat/lez is used by sublist-prefix, sublist-move, rmpos-in, restN-dups, put-sw-in, put-in-02, put-at, get-nodups, firstn-prefix, dups-def,
nat/lez-01 is used by sublist-move, sublist-append-04, rmpos-size, rmpos-in, restn-nonempty-2, restn-nonempty, restn-last, restn-empty, restN-dups, lastn-restn, lastn-mklist, lastN-blastN, get-firstn, get-butlast, firstn-twice, firstn-prefix, first-mklist, blastN-firstN,
nat/ls is used by sublist-at, get-mklist-01,
nat/ls-01 is used by sublist-at, lastn-app, lastN-ex, get-mklist,
nat/ls-02 is used by sublist-first-skip, rmpos-size, first-append-01, del-rmdup-length-nle,
nat/ls-03 is used by firstN-in-03, firstN-in-02,
nat/ls-le-simp is used by sublist-lenrec-01,
nat/one-02 is used by get-firstn,
nat/pred-03 is used by sublist-rec-01, sublist-rec, sublist-prefix, sublist-part, sublist-num-01, sublist-move, sublist-firsteq, sublist-append-04, restn-nonempty-2, restn-nonempty, restn-last, restn-first-get, restn-empty, restN-dups, rest-rec, put-rec-02, put-rec-01, put-rec, put-length, put-in-02, put-in-01, put-in, put-del1-in, put-at-eq, put-at, put-app-left, num-lastN, lastn-restn, lastn-rec, lastn-lastn-01, lastn-app, lastN-blastN, l-02, l-01, l, get-numrec, get-nodups, get-mklist-01, get-last-04, firstn-twice, firstn-prefix, firstn-last-rec, firstn-last, firstn-firstn, firstn-first, firstn-butlast, firstn-append-01, firstN-rec-01, firstN-num-rec, firstN-lastN, first-num, first-mklist, dups-def, blastN-firstN,
nat/succ-01 is used by sublist-prefix, sublist-lenrec-01, rmtoobigpos, rmpos-size, rmpos-in, rmpos-get, restn-nonempty-2, restn-nonempty, restn-less, restn-last, restn-firstn-better, restn-firstn, restn-first-get, restn-empty, restN-append, put-sw-in, put-length, put-in-02, put-in-01, put-in, put-del1-in, put-at-eq, put-at, put-app-left, pos-get, lastn-neq-01, lastn-lastn-01, inl-01, inl, get-nodups, get-in, get-firstn, get-butlast, get-append-less, firstn-restn-in, firstn-restn-eq, firstn-length-01, firstn-last-rec, firstn-last-01, firstn-last, firstn-firstn, firstN-dups-04, first-append, dups-def, del-rmdup-length-nle,
nat/zero is used by put-last, put-firstn-restn, lastN-all, get-app-1, blastN-firstN,
nat/zero-02 is used by blastN-firstN,

Used from specification list-last

list-last/blastN-all-01 is used by blastN-firstN,
list-last/blastN-rec-01 is used by blastN-firstN,
list-last/l-02 is used by firstn-last-01,
list-last/mk-plus is used by rest-mklist-03, first-mklist-03,
list-last/mk-rec is used by lastn-mklist, first-mklist,
list-last/mk-rest is used by get-mklist-01,
list-last/prefix is used by firstn-prefix-01, firstn-allprefix,
list-last/b is used by firstn-butlast,
list-last/bapp is used by lastn-app,
list-last/btwo is used by firstn-butlast,
list-last/butlast-def is used by lastn-lastn-01, lastN-rec-01, lastN-blastN,
list-last/butlast-last is used by lastn-app,
list-last/butlast-len is used by blastN-firstN,
list-last/butlastN-base is used by lastN-blastN, blastN-firstN,
list-last/butlastN-rec is used by lastN-blastN, blastN-firstN,
list-last/l is used by sublist-last, restn-size-last, restn-last, lastn-one-01, get-last2, get-last-04, get-last-01, firstn-last-01, firstn-last, at-last,
list-last/l-02 is used by restn-size-last, restn-last, get-last-04, at-last,
list-last/l-05 is used by sublist-last, get-last2, get-last-01, firstn-last,
list-last/lapp is used by lastn-app,
list-last/last-def is used by lastn-lastn-01, lastN-rec-01,
list-last/last-elim is used by restn-size-last, lastn-restn-01, lastn-neq-01, get-last-04, firstn-butlast-intro,
list-last/lb is used by lastn-app,
list-last/mk-empty is used by lastn-mklist, get-mklist-01,
list-last/mk-first-01 is used by get-mklist-01,
list-last/mk-inj-01 is used by sublist-mklist-02, sublist-mklist-01, sublist-mklist, rest-mklist-03, rest-mklist-02, rest-mklist, lastn-mklist, first-mklist-02,
list-last/mk-last is used by rest-mklist-04,
list-last/mk-len is used by sublist-mklist-01, rest-mklist-02, lastn-mklist-03, lastn-mklist-02, lastn-mklist-01, lastn-mklist, first-mklist-04, first-mklist-02,
list-last/mk-plus is used by rest-mklist-04, rest-mklist,
list-last/mk-zero is used by rest-mklist-04, lastn-mklist, get-mklist-01, get-mklist, first-mklist,
list-last/mklist-one is used by rest-mklist-04,
list-last/prefix-empty is used by firstn-prefix,
list-last/prefix-nil is used by sublist-prefix, firstn-prefix,
list-last/prefix-rec-02 is used by sublist-prefix, firstn-prefix-04, firstn-prefix,
list-last/rev-e is used by del-rev,
list-last/rev-r is used by del-rev,

Used from specification list-data

list-data/length-neq is used by lastn-neq-02,
list-data/elim-list-c is used by sublist-prefix, sublist-lenrec-01, sublist-lenrec, sublist-last, rmpos-get, restn-less, restn-firstn-better, restn-firstn, restN-append, rest-sub, rest-len, putset-same, put-zero-01, put-rec-01, put-rec, put-firstn-restn, lastn-mklist, lastN-rest-01, lastN-rest, get-zero, get-restn, get-rec-01, firstrestex, firstn-restn-in, firstn-restn-eq, firstn-prefix-04, firstn-last-rec, firstn-last, firstn-firstn, firstn-first, firstn-butlast, firstn-append-01, firstn-append, firstN-dups-04, first-append, extension, del1-first,
list-data/l is used by sublist-prefix, sublist-lenrec-01, sublist-lenrec, sublist-last, size-rmdup-del, size-del-nodups, rmpos-size, rmpos-in, rmpos-get, restn-nonempty-2, restn-nonempty, restn-less, restn-last, restn-firstn-better, restn-firstn, restn-first-get, restn-empty, restN-append, putset-same, put-sw-in, put-length, put-in-02, put-in-01, put-in, put-firstn-restn, put-del1-in, put-at-eq, put-at, put-app-left, possize-notin, pos-get, lastn-neq-01, lastn-app, lastN-rest, lastN-in, l-02, l, get-restn, get-nodups, get-last-nonempty, get-last-04, get-in, get-firstn, get-butlast, get-append-less, firstrestex, firstn-restn-in, firstn-restn-eq, firstn-last-rec, firstn-last, firstn-firstn, firstn-butlast-intro, firstn-at-in-dups, firstN-lastN-in-01, firstN-dups-05, firstN-dups-04, firstN-dups-01, firstN-dups, first-append, extension, dups-def, delete-one-nls, del-rmdup-length-nle, del-length, at-last, append-mod,
list-data/lr-05 is used by lastN-rest,
list-data/size-01 is used by sublist-part, sublist-move, sublist-append-04, sublist-append-01, size-rmdup-del, size-del-nodups, rmpos-size, rmpos-in, restn-size-last, restn-nonempty-2, restn-nonempty, restn-last, restn-firstn, restn-first-get, restn-empty, restn-at, restN-dups, restN-all, rest-sub, rest-len, rest-app, put-sw-in, put-in-02, put-in-01, put-in, put-firstn-restn, put-del1-in, put-at-eq, put-at, put-app-right, put-app-left, possize-notin, notin-03, lastn-restn-01, lastn-restn, lastn-length, lastn-app, lastN-rest-01, lastN-dups, lastN-blastN, l-02, l-01, l, inl-01, get-last2, get-last-04, get-last-01, get-last, get-firstn, get-butlast, get-append-grt, get-app, firstn-twice, firstn-prefix-04, firstn-prefix, firstn-last-01, firstn-butlast, firstn-append-01, firstn-app, firstN-len, firstN-lastN, first-length, first-all, extension, dups-def, delpos-atsizeid, delete-one-nls, blastN-firstN, at-last, append-mod, app-05-neg,

Used from specification list

list/In is used by in-get,
list/in-append is used by firstN-lastN-in,
list/lastdiv is used by lastN-blastN,
list/len-01 is used by put-firstn-restn,
list/Last is used by sublist-lenrec-01, sublist-lenrec, lastn-restn-01, lastn-rec, lastn-one, lastn-neq-01, lastn-length, lastn-lastn-01, lastn-lastn, lastn-app, lastN-rec-01, lastN-empty, firstn-last-rec, del-rev,
list/Nil is used by sublist-part, sublist-lenrec-01, sublist-append-04, sublist-append-01, rmdup-last, restN-len, rest-mklist-02, rest-app, put-firstn-restn, put-app-right, put-app-left, lastn-one, lastn-app, lastN-blastN, lastN-append-01, get-last-04, get-last, get-butlast, get-append-grt, get-app, firstrestex, firstn-restn-eq, firstn-last-rec, firstn-last-01, firstn-butlast, firstn-append-01, firstn-append, firstn-app, firstN-len, firstN-lastN, del-append, append-mod, app-05-neg, app-05, app-01, app,
list/a is used by weak-restN-rec, weak-firstN-rec, sw-02, sw, sublist-rec-01, sublist-rec, sublist-prefix, sublist-part, sublist-one, sublist-num-01, sublist-not-empty-02, sublist-not-empty, sublist-move, sublist-lenrec-01, sublist-lenrec, sublist-last, sublist-good, sublist-firsteq, sublist-append-04, sublist-append-03, sublist-append-02-01, sublist-append-02, sublist-append-01-01, sublist-append-01, sublist-append, sub-zerorec-01, sub-zerorec, sub-len-01, size-rmdup-del, size-del-nodups, rmtoobigpos, rmpos-size, rmpos-in, rmpos-get, rmdup-last, rmdup-del1-del, restn-size-last, restn-prefix, restn-nonempty-2, restn-nonempty, restn-less, restn-last, restn-firstn-better, restn-firstn, restn-first-get, restn-empty, restn-at, restN-len, restN-dups, restN-append, restN-all, rest-two-01, rest-two, rest-sub, rest-one, rest-mklist-04, rest-mklist-03, rest-mklist-02, rest-mklist, rest-len, rest-in, rest-app, putset-same, put-zero-01, put-sw-in, put-rec-02, put-rec-01, put-rec, put-one-01, put-one, put-length, put-last, put-in-02, put-in-01, put-in, put-firstn-restn, put-del1-in, put-butlast, put-at-eq, put-at, put-app-right, put-app-left, possize-notin, pos-one, pos-get, pos-equal, one-01-01, one-01, one, num-lastN, notin-03, nodups-rmposnodups, list-select-not-first, len-01, lastn-restn-01, lastn-restn, lastn-rec, lastn-one, lastn-neq-04, lastn-neq-02, lastn-neq-01, lastn-neq, lastn-mklist-02, lastn-mklist-01, lastn-mklist, lastn-length, lastn-lastn-01, lastn-lastn, lastn-app, lastN-rest-01, lastN-rest, lastN-rec-01, lastN-in-01, lastN-ex, lastN-empty, lastN-dups, lastN-blastN, lastN-append-01, lastN-append, l-02, l-01, l, inl-01, inl, in-get, in-04, in-03, in-02-01, in-02, in-01-01, in-01, in, get-zero, get-restn, get-rec-01, get-numrec, get-nodups, get-mklist, get-last2, get-last-nonempty, get-last-04, get-last-01, get-last, get-in, get-firstn, get-butlast, get-append-less, get-append-grt, get-app, get-add-num, get, from-rest, from-notin, firstrestex, firstn-two, firstn-twice, firstn-restn-in, firstn-restn-eq, firstn-prefix-04, firstn-prefix, firstn-one-02, firstn-one-01, firstn-one, firstn-length-02, firstn-length-01, firstn-length, firstn-last-rec, firstn-last-01, firstn-last, firstn-firstn, firstn-first, firstn-butlast-intro, firstn-butlast, firstn-append-01, firstn-append, firstn-app-exact, firstn-app-02, firstn-app-01, firstn-app, firstn-allprefix, firstN-rec-01, firstN-num-rec, firstN-len, firstN-lastN, firstN-in, firstN-empty, firstN-dups-04, firstN-dups-03, firstN-dups-02, firstN-dups-01, firstN-dups, first-num, first-mklist, first-length, first-append, first-all, extension, elim-lastn-butlastn, elim-firstn-restn, dups-def, dups-01, dups, delpos-in, delpos-atsizeid, delnr-one, delete-one-nls, delete-dups, del1-first, del1-empty, del1-del-switch, del1-del, del-rmdup-length-nle, del-rmdup, del-rev, del-n-simp, del-length, del-del1-switch, del-del1-nodups, del-del, del-append, blastN-firstN, at-last, append-mod, app-05-neg, app-05, app-01, app,
list/app is used by sublist-one, sublist-not-empty-02, sublist-lenrec-01, sublist-last, size-rmdup-del, rmpos-size, rmpos-in, restn-size-last, restn-nonempty, restn-last, put-one, put-firstn-restn, pos-one, one-01-01, one-01, one, lastn-app, lastN-ex, lastN-blastN, get-mklist, get-last2, get-last-04, get-last-01, get-firstn, get-butlast, firstn-one-02, firstn-one-01, firstn-one, firstn-last-rec, firstn-last-01, firstn-last, firstn-butlast, firstn-append, delnr-one, del-rev, at-last,
list/app-01 is used by sublist-lenrec, sublist-append-02-01, sublist-append-02, restN-append, put-last, put-firstn-restn, put-butlast, num-lastN, lastn-rec, lastn-app, lastN-rec-01, lastN-blastN, firstn-app-02, firstn-app-01, app,
list/app-02-ant is used by size-rmdup-del, restn-nonempty-2, restn-nonempty, restn-empty, lastn-neq-01, lastN-empty, firstn-last-01, firstn-butlast, firstn-append-01, firstn-append, firstN-empty, del1-empty,
list/app-03 is used by lastn-restn-01, lastn-lastn-01, lastn-lastn, lastN-blastN, del-rev,
list/app-08 is used by weak-firstN-rec, sw-02, sw, sublist-rec-01, sublist-rec, sublist-part, sublist-num-01, sublist-move, sublist-lenrec-01, sublist-firsteq, sublist-append-04, sub-zerorec-01, sub-zerorec, rmtoobigpos, rmdup-last, rmdup-del1-del, restn-less, putset-same, put-zero-01, put-rec-02, put-rec-01, put-rec, put-one-01, put-firstn-restn, put-app-right, put-app-left, in-03, in-02-01, from-rest, firstrestex, firstn-two, firstn-twice, firstn-restn-eq, firstn-last-rec, firstn-last-01, firstn-firstn, firstn-butlast, firstn-append-01, firstn-append, firstn-app, firstN-rec-01, firstN-num-rec, firstN-len, firstN-lastN, first-num, first-mklist, first-append, first-all, delpos-atsizeid, del1-first, del1-del-switch, del1-del, del-rmdup, del-n-simp, del-del1-switch, del-del1-nodups, del-del, del-append, blastN-firstN, append-mod, app-01, app,
list/c is used by weak-firstN-rec, sw-02, sw, sublist-rec-01, sublist-rec, sublist-prefix, sublist-part, sublist-num-01, sublist-num, sublist-not-empty, sublist-move, sublist-lenrec-01, sublist-lenrec, sublist-last, sublist-firsteq, sublist-append-04, sublist-append-01, sub-zerorec-01, sub-zerorec, size-rmdup-del, size-del-nodups, rmtoobigpos, rmpos-size, rmpos-in, rmpos-get, rmdup-last, rmdup-del1-del, restn-nonempty-2, restn-nonempty, restn-less, restn-last, restn-firstn-better, restn-firstn, restn-first-get, restn-empty, restn-at, restN-dups, restN-append, restN-all, rest-sub, rest-len, rest-app, putset-same, put-zero-01, put-sw-in, put-rec-02, put-rec-01, put-rec, put-one, put-length, put-in-02, put-in-01, put-in, put-firstn-restn, put-del1-in, put-at-eq, put-at, put-app-right, put-app-left, possize-notin, pos-get, pos-equal, notin-03, nodups-rmposnodups, len-01, lastn-restn, lastn-mklist, lastN-rest-01, lastN-rest, lastN-dups, lastN-append-01, l-02, l-01, l, inl-01, inl, in-get, in-04, in-03, in-02-01, in-02, in-01-01, in-01, in, get-zero, get-restn, get-rec-01, get-nodups, get-last2, get-last-nonempty, get-last-01, get-last, get-in, get-firstn, get-butlast, get-append-less, get-append-grt, get-app, get, from-rest, from-notin, firstrestex, firstn-twice, firstn-restn-in, firstn-restn-eq, firstn-prefix-04, firstn-prefix, firstn-last-rec, firstn-last-01, firstn-last, firstn-firstn, firstn-first, firstn-butlast, firstn-append-01, firstn-append, firstn-app, firstN-rec-01, firstN-num-rec, firstN-len, firstN-lastN, firstN-empty, firstN-dups-04, first-num, first-mklist, first-length, first-append, first-all, extension, dups-def, dups-01, dups, delpos-in, delpos-atsizeid, delete-one-nls, delete-dups, del1-first, del1-empty, del1-del-switch, del1-del, del-rmdup-length-nle, del-rmdup, del-rev, del-length, del-del1-switch, del-del1-nodups, del-del, del-append, blastN-firstN, at-last, append-mod, app-05-neg, app-05, app-01, app,
list/c-03 is used by del1-empty,
list/c-04 is used by sublist-one-01, sublist-one, sublist-lenrec-01, rmdup-last, restn-size-last, lastn-one-01, lastn-one, firstn-one-02, firstn-one-01, firstn-one, firstn-last-rec, firstn-butlast, firstn-append-01, firstn-append,
list/c-05 is used by firstn-last-01,
list/c-06 is used by sublist-firsteq, put-firstn-restn, lastn-mklist, firstn-last-01, firstn-firstn, firstn-first, firstn-append, extension,
list/c-07 is used by weak-restN-rec, weak-firstN-rec, sublist-part, sublist-num-01, sublist-move, sublist-lenrec-01, sublist-last, sublist-append-04, sublist-append-01, rmpos-get, restn-size-last, restn-nonempty-2, restn-nonempty, restn-less, restn-last, restn-firstn-better, restn-firstn, restn-first-get, restn-empty, restN-dups, restN-all, rest-two-01, rest-two, rest-one, rest-mklist-04, rest-app, put-sw-in, put-one-01, put-length, put-in-02, put-in-01, put-in, put-del1-in, put-at, lastn-restn, lastN-rest, lastN-append-01, get-mklist, get-in, get-firstn, get-butlast, get-append-less, from-rest, firstn-twice, firstn-last-rec, firstn-last-01, firstn-butlast, firstn-append-01, firstn-append, firstn-app, firstN-rec-01, firstN-num-rec, firstN-len, firstN-lastN, first-all, at-last,
list/c-08 is used by weak-firstN-rec, sublist-part, sublist-num-01, sublist-move, sublist-lenrec-01, sublist-append-04, restn-first-get, put-one-01, put-length, put-in-02, put-in-01, put-in, put-del1-in, put-at, get-firstn, firstn-twice, firstn-last-rec, firstn-last-01, firstn-butlast, firstn-append-01, firstn-append, firstn-app, firstN-rec-01, firstN-num-rec, firstN-len, first-all,
list/e is used by sublist-not-empty-02, size-rmdup-del, restn-nonempty-2, restn-nonempty, restn-empty, one-03, lastn-neq-01, lastN-empty, firstN-empty, del1-empty,
list/e-01 is used by sublist-prefix, sublist-not-empty, sublist-lenrec-01, sublist-lenrec, sublist-last, sublist-firsteq, size-rmdup-del, size-del-nodups, rmpos-size, rmpos-in, rmpos-get, restn-nonempty-2, restn-nonempty, restn-less, restn-firstn-better, restn-firstn, restN-append, rest-sub, rest-len, putset-same, put-sw-in, put-rec-01, put-rec, put-one-01, put-length, put-in-02, put-in-01, put-in, put-firstn-restn, put-del1-in, put-at, pos-get, lastN-rest, l, get-restn, get-nodups, get-mklist, get-last-nonempty, get-in, get-firstn, get-butlast, get-append-less, firstrestex, firstn-restn-in, firstn-restn-eq, firstn-prefix-04, firstn-last-rec, firstn-last-01, firstn-last, firstn-firstn, firstn-first, firstn-butlast, firstn-append-01, firstn-append, firstN-dups-04, first-append, extension, delete-one-nls, del1-empty, del-length, at-last,
list/e-02 is used by restn-size-last, lastn-restn-01, lastn-neq-01, lastN-blastN, get-last-04, firstn-butlast-intro,
list/first is used by one-03, firstn-one-02,
list/first-01 is used by first-append,
list/in-01 is used by rmpos-in, put-sw-in, put-in-01, put-in, put-del1-in, in-04, in-02, in-01-01, in-01, in, dups-01, delpos-in,
list/in-06 is used by rmpos-in, put-in-02, notin-03, in-04, in-03, in-02-01, in-01-01, in-01, in, get-in, from-notin, delpos-in, app-05-neg, app-01,
list/in-11 is used by firstn-last-01, firstN-in,
list/in-12 is used by rest-in, lastN-in-01,
list/in-14 is used by put-firstn-restn, lastn-neq-02, lastn-neq-01, lastn-neq, lastn-mklist, firstn-last-01, firstn-firstn, firstn-first, firstn-butlast, firstn-append-01, firstn-append,
list/in-15 is used by lastn-neq-01, lastN-blastN,
list/in-17 is used by size-rmdup-del, rmdup-last, lastn-neq-01, lastN-blastN, del-rev, del-one-simp,
list/in-append is used by size-rmdup-del, rmdup-last, put-firstn-restn, lastn-neq-01, lastN-blastN, firstn-last-01, firstn-butlast, firstn-append-01, firstn-append,
list/in-empty is used by size-rmdup-del, size-del-nodups, rmpos-in, put-sw-in, put-in-01, put-in, put-firstn-restn, put-del1-in, possize-notin, pos-equal, l-02, l-01, l, inl-01, inl, in-04, in-02, in-01-01, in-01, in, get, firstn-restn-in, dups-01, delpos-in, del-rmdup-length-nle, app-05, app,
list/in-rec is used by size-del-nodups, rmpos-in, put-sw-in, put-in-01, put-in, put-firstn-restn, put-del1-in, possize-notin, pos-equal, lastn-neq-02, lastn-neq-01, lastn-mklist, l-02, l, inl-01, inl, in-04, in, get, from-rest, firstn-restn-in, firstn-last-01, firstn-firstn, firstn-first, firstn-butlast, firstn-append-01, firstn-append, dups-01, app-05, app,
list/inapp-02 is used by firstn-last-01,
list/inapp-13 is used by lastn-neq-01,
list/len is used by size-rmdup-del, restn-size-last, rest-in, put-firstn-restn, lastn-restn-01, lastn-neq-01, lastn-mklist-01, lastn-length, lastN-rest, lastN-in-01, lastN-blastN, lastN-append-01, lastN-append, in-get, get-last-04, firstn-length-02, firstn-length-01, firstn-length, firstn-butlast-intro, firstN-in, elim-lastn-butlastn, dups-def,
list/len-02 is used by size-rmdup-del, rmpos-in, rmpos-get, restn-size-last, put-firstn-restn, pos-get, lastn-restn-01, lastn-neq-01, lastn-length, lastN-rest, lastN-blastN, get-last-04, firstn-butlast-intro, dups-def,
list/len-03 is used by firstn-last-01, firstn-butlast, firstn-append-01,
list/len-05 is used by sublist-prefix, sublist-part, sublist-move, sublist-lenrec-01, sublist-lenrec, sublist-last, sublist-append-04, sublist-append-01, size-del-nodups, rmtoobigpos, rmpos-size, rmpos-in, rmpos-get, restn-nonempty-2, restn-nonempty, restn-less, restn-last, restn-firstn-better, restn-firstn, restn-first-get, restn-empty, restn-at, restN-dups, restN-append, restN-all, rest-sub, rest-len, rest-app, putset-same, put-sw-in, put-length, put-in-02, put-in-01, put-in, put-firstn-restn, put-del1-in, put-at-eq, put-at, put-app-right, put-app-left, possize-notin, pos-get, notin-03, len-01, lastn-restn, lastn-neq-02, lastn-mklist-02, lastN-rest-01, lastN-dups, lastN-append-01, l-02, l-01, l, inl-01, inl, in-get, get-restn, get-nodups, get-last2, get-last-nonempty, get-last-01, get-last, get-in, get-firstn, get-butlast, get-append-less, get-append-grt, get-app, firstrestex, firstn-twice, firstn-restn-in, firstn-restn-eq, firstn-prefix-04, firstn-prefix, firstn-length-02, firstn-length-01, firstn-length, firstn-last-rec, firstn-last-01, firstn-last, firstn-firstn, firstn-butlast, firstn-append-01, firstn-app, firstN-len, firstN-lastN, firstN-dups-04, first-length, first-append, first-all, extension, delpos-atsizeid, delete-one-nls, del-rmdup-length-nle, del-length, blastN-firstN, at-last, append-mod, app-05-neg,
list/len-06 is used by firstn-last-01, firstn-butlast, firstn-append-01,
list/rest is used by rest-one-01, firstn-one-02,
list/rest-01 is used by restN-append, first-append,

Used from specification list-dup

list-dup/dups-appex is used by firstN-dups-03, firstN-dups-02,
list-dup/rm-ifrec is used by rmdup-last, rmdup-del1-del, del-rmdup,
list-dup/rmdup-n is used by del-rmdup-length-nle,
list-dup/rmdup-y is used by size-rmdup-del,
list-dup/a is used by firstN-dups-03, firstN-dups-02, firstN-dups-01, firstN-dups,
list-dup/e-01 is used by rmpos-in, restN-dups, nodups-rmposnodups, firstN-dups-04, dups-def, dups, delete-dups,
list-dup/in-06 is used by firstN-dups-03, firstN-dups-02,
list-dup/rec is used by size-del-nodups, rmpos-in, restN-dups, pos-get, nodups-rmposnodups, lastN-dups, get-nodups, firstN-dups-04, dups-def, dups-01, dups, delete-dups, del-del1-nodups,
list-dup/rm-empty is used by size-rmdup-del, del-rmdup-length-nle,
list-dup/rm-one is used by size-rmdup-del, rmdup-last,
list-dup/rmdup-e is used by size-rmdup-del, rmdup-last, rmdup-del1-del, del-rmdup,
list-dup/rmdup-n is used by size-rmdup-del, del-rmdup,
list-dup/rmdup-y is used by size-rmdup-del, del-rmdup-length-nle, del-rmdup,

Used from specification nat-basic2

nat-basic2/a is used by weak-restN-rec, weak-firstN-rec, sublist-two-num, sublist-restn-02, sublist-rec-01, sublist-rec, sublist-prefix, sublist-part, sublist-num-01, sublist-not-empty, sublist-move, sublist-mklist-01, sublist-mklist, sublist-lenrec-01, sublist-lenrec, sublist-last, sublist-firsteq, sublist-first-skip, sublist-at, sublist-append-04, sublist-append-02, sublist-append-01, sublist-append, sub-zerorec-01, sub-zerorec, sub-rec-01, sub-rec, size-rmdup-del, size-del-nodups, rmtoobigpos, rmpos-size, rmpos-in, rmpos-get, restn-size-last, restn-rest, restn-nonempty-2, restn-nonempty, restn-less, restn-last, restn-firstn-better, restn-firstn, restn-first-get, restn-empty, restn-at, restn-apprec, restN-dups, restN-append, restN-all, rest-sub, rest-rec, rest-one-01, rest-one, rest-mklist-04, rest-mklist-01, rest-mklist, rest-len, rest-in, rest-append, rest-app, putset-same, put-sw-in, put-rec-02, put-rec-01, put-rec, put-length, put-in-02, put-in-01, put-in, put-firstn-restn, put-del1-in, put-at-eq, put-at, put-app-right, put-app-left, possize-notin, pos-get, pos-equal, num-lastN, notin-03, nodups-rmposnodups, list-select-not-first, len-01, lastn-restn-01, lastn-restn, lastn-rec, lastn-neq-02, lastn-neq-01, lastn-mklist-02, lastn-mklist-01, lastn-mklist, lastn-length, lastn-lastn-01, lastn-lastn, lastn-app, lastN-rest-01, lastN-rest, lastN-rec-01, lastN-in-01, lastN-ex, lastN-empty, lastN-dups, lastN-blastN, lastN-append-01, lastN-append, l-02, l-01, l, inl-01, inl, in-get, get-restn, get-rec-01, get-rec, get-numrec, get-nodups, get-mklist-01, get-mklist, get-last2, get-last-nonempty, get-last-04, get-last-01, get-last, get-in, get-firstn, get-butlast, get-append-less, get-append-grt-02, get-append-grt, get-app, get-add-num, get, from-rest, firstrestex, firstn-twice, firstn-restn-in, firstn-restn-eq, firstn-prefix-04, firstn-prefix-03, firstn-prefix-02, firstn-prefix, firstn-length-02, firstn-length-01, firstn-length, firstn-last-rec, firstn-last-eq, firstn-last-01, firstn-last, firstn-firstn, firstn-butlast-intro, firstn-butlast, firstn-append-01, firstn-append, firstn-app-02, firstn-app-01, firstn-app, firstN-rec-01, firstN-num-rec, firstN-len, firstN-lastN, firstN-in-03, firstN-in-02, firstN-in, firstN-empty, firstN-dups-04, first-num, first-mklist-03, first-mklist-01, first-mklist, first-length, first-append-01, first-append, first-all, extension, elim-lastn-butlastn, dups-def, delpos-in, delpos-atsizeid, delete-one-nls, del-rmdup-length-nle, del-length, blastN-firstN, at-last, append-mod, app-05-neg, app-05,
nat-basic2/add-base is used by sublist-part, sublist-move, sublist-lenrec, sublist-last, sublist-append-04, sublist-append-01, restn-firstn-better, restn-firstn, restn-apprec, rest-sub, rest-len, rest-app, put-app-right, lastn-restn-01, lastn-mklist, lastn-app, lastN-ex, l-02, l-01, get-restn, get-append-grt, firstn-last-01, firstn-butlast, firstn-append-01, firstn-app, firstN-lastN, first-mklist, blastN-firstN, append-mod, app-05-neg,
nat-basic2/c is used by weak-restN-rec, weak-firstN-rec, sublist-two-num, sublist-restn-02, sublist-rec-01, sublist-rec, sublist-prefix, sublist-part, sublist-num-01, sublist-not-empty, sublist-move, sublist-mklist-01, sublist-mklist, sublist-lenrec-01, sublist-lenrec, sublist-last, sublist-firsteq, sublist-first-skip, sublist-at, sublist-append-04, sublist-append-02, sublist-append-01, sublist-append, sub-zerorec-01, sub-zerorec, sub-rec-01, sub-rec, size-rmdup-del, size-del-nodups, rmtoobigpos, rmpos-size, rmpos-in, rmpos-get, restn-size-last, restn-rest, restn-nonempty-2, restn-nonempty, restn-less, restn-last, restn-firstn-better, restn-firstn, restn-first-get, restn-empty, restn-at, restn-apprec, restN-dups, restN-append, restN-all, rest-sub, rest-rec, rest-one-01, rest-one, rest-mklist-04, rest-mklist-03, rest-mklist-01, rest-mklist, rest-len, rest-in, rest-append, rest-app, putset-same, put-sw-in, put-rec-02, put-rec-01, put-rec, put-length, put-in-02, put-in-01, put-in, put-firstn-restn, put-del1-in, put-at-eq, put-at, put-app-right, put-app-left, possize-notin, pos-get, pos-equal, num-lastN, notin-03, nodups-rmposnodups, list-select-not-first, len-01, lastn-restn-01, lastn-restn, lastn-rec, lastn-neq-02, lastn-neq-01, lastn-mklist-02, lastn-mklist-01, lastn-mklist, lastn-length, lastn-lastn-01, lastn-lastn, lastn-app, lastN-rest-01, lastN-rest, lastN-rec-01, lastN-in-01, lastN-ex, lastN-empty, lastN-dups, lastN-blastN, lastN-append-01, lastN-append, l-02, l-01, l, inl-01, inl, in-get, get-restn, get-rec-01, get-rec, get-numrec, get-nodups, get-mklist-01, get-mklist, get-last2, get-last-nonempty, get-last-04, get-last-01, get-last, get-in, get-firstn, get-butlast, get-append-less, get-append-grt-02, get-append-grt, get-app, get-add-num, get, from-rest, firstrestex, firstn-twice, firstn-restn-in, firstn-restn-eq, firstn-prefix-04, firstn-prefix-03, firstn-prefix-02, firstn-prefix, firstn-length-02, firstn-length-01, firstn-length, firstn-last-rec, firstn-last-eq, firstn-last-01, firstn-last, firstn-firstn, firstn-butlast-intro, firstn-butlast, firstn-append-01, firstn-append, firstn-app-02, firstn-app-01, firstn-app, firstN-rec-01, firstN-num-rec, firstN-len, firstN-lastN, firstN-in-03, firstN-in-02, firstN-in, firstN-empty, firstN-dups-04, first-num, first-mklist-03, first-mklist-01, first-mklist, first-length, first-append-01, first-append, first-all, extension, elim-lastn-butlastn, dups-def, delpos-in, delpos-atsizeid, delete-one-nls, del-rmdup-length-nle, del-length, blastN-firstN, at-last, append-mod, app-05-neg, app-05,
nat-basic2/eq is used by put-firstn-restn, l-02, l-01,
nat-basic2/eq-01 is used by sublist-part, sublist-append-04, size-rmdup-del, size-del-nodups, rmpos-size, restn-empty, rest-sub, rest-len, put-length, put-at, possize-notin, pos-get, pos-equal, notin-03, lastn-restn-01, lastn-neq-02, lastn-mklist-02, lastn-length, lastn-app, lastN-rest-01, l-02, l, get-nodups, get-last-nonempty, get-last-04, firstn-prefix-04, firstn-butlast, firstn-append-01, firstN-lastN, first-length, extension, dups-def, at-last, app-05-neg, app-05,
nat-basic2/eqs is used by firstn-last-01, firstn-butlast, firstn-append-01,
nat-basic2/l is used by sublist-prefix, sublist-lenrec, sublist-last, rmpos-get, putset-same, len-01, get-restn, firstrestex, firstn-last-rec, delete-one-nls, del-length, append-mod,
nat-basic2/l-01 is used by lastN-ex, append-mod,
nat-basic2/l-02 is used by sublist-restn-02, sublist-mklist, sublist-lenrec, sublist-first-skip, sublist-at, rest-mklist-01, rest-append, put-firstn-restn, lastn-restn-01, lastn-restn, lastn-mklist-01, lastN-ex, lastN-append-01, lastN-append, in-get, get-append-grt-02, firstn-prefix-04, firstn-prefix-03, firstn-prefix-02, firstn-length-01, firstn-last-eq, firstN-lastN, first-mklist-03, first-mklist-01, first-append-01, elim-lastn-butlastn, delete-one-nls,
nat-basic2/l-08 is used by sublist-prefix,
nat-basic2/nls-fst is used by sublist-prefix, del-length,
nat-basic2/one-03 is used by size-rmdup-del,
nat-basic2/oz is used by sublist-rec-01, sublist-rec, sublist-prefix, sublist-part, sublist-num-01, sublist-move, sublist-firsteq, sublist-append-04, rmtoobigpos, rmpos-size, rmpos-in, rmpos-get, restn-nonempty-2, restn-nonempty, restn-last, restn-first-get, restn-empty, restN-dups, rest-sub, rest-len, put-sw-in, put-rec-02, put-rec-01, put-rec, put-length, put-in-02, put-in-01, put-in, put-del1-in, put-at-eq, put-at, put-app-left, pos-get, len-01, lastn-restn-01, lastn-restn, lastn-rec, lastn-mklist, lastn-lastn-01, lastn-app, lastN-blastN, inl-01, inl, get-numrec, get-nodups, get-last-04, get-in, get-firstn, get-butlast, get-append-less, firstn-twice, firstn-prefix, firstn-last-rec, firstn-last, firstn-firstn, firstn-butlast, firstn-append-01, firstN-rec-01, firstN-num-rec, firstN-lastN, first-num, first-mklist, dups-def, append-mod,
nat-basic2/pred is used by lastn-lastn-01, firstn-last-rec,
nat-basic2/s is used by sublist-prefix, sublist-lenrec-01, rmtoobigpos, rmpos-size, rmpos-in, rmpos-get, restn-nonempty-2, restn-nonempty, restn-less, restn-last, restn-firstn-better, restn-first-get, restn-empty, restn-at, restN-append, put-sw-in, put-length, put-in-02, put-in-01, put-in, put-firstn-restn, put-del1-in, put-at-eq, put-at, put-app-left, pos-get, lastn-restn, lastn-neq-01, lastn-mklist, lastn-lastn-01, lastn-app, lastN-rest, lastN-dups, lastN-blastN, lastN-append-01, inl-01, inl, in-get, get-nodups, get-mklist, get-last-04, get-in, get-firstn, get-butlast, get-append-less, firstn-restn-in, firstn-restn-eq, firstn-last-rec, firstn-last, firstn-firstn, firstn-butlast-intro, firstN-dups-04, first-append, extension, dups-def, blastN-firstN,
nat-basic2/succ is used by sublist-prefix, sublist-part, sublist-move, sublist-lenrec-01, sublist-lenrec, sublist-last, sublist-append-04, sublist-append-01, size-del-nodups, rmtoobigpos, rmpos-size, rmpos-in, rmpos-get, restn-rest, restn-nonempty-2, restn-nonempty, restn-less, restn-last, restn-firstn-better, restn-firstn, restn-first-get, restn-empty, restn-at, restn-apprec, restN-dups, restN-append, restN-all, rest-sub, rest-mklist-04, rest-len, rest-app, putset-same, put-sw-in, put-length, put-in-02, put-in-01, put-in, put-firstn-restn, put-del1-in, put-at-eq, put-at, put-app-right, put-app-left, possize-notin, pos-get, notin-03, nodups-rmposnodups, len-01, lastn-restn-01, lastn-restn, lastn-neq-02, lastn-neq-01, lastn-mklist-02, lastn-mklist, lastn-length, lastn-lastn-01, lastn-lastn, lastN-rest-01, lastN-rest, lastN-empty, lastN-dups, lastN-append-01, l-02, l-01, l, inl-01, inl, in-get, get-restn, get-nodups, get-mklist-01, get-last2, get-last-nonempty, get-last-01, get-last, get-in, get-firstn, get-butlast, get-append-less, get-append-grt, get-app, firstrestex, firstn-twice, firstn-restn-in, firstn-restn-eq, firstn-prefix-04, firstn-prefix, firstn-length-02, firstn-length-01, firstn-length, firstn-last-rec, firstn-last-01, firstn-last, firstn-firstn, firstn-butlast, firstn-at-in-dups, firstn-append-01, firstn-append, firstn-app, firstN-len, firstN-lastN, firstN-empty, firstN-dups-04, first-mklist, first-length, first-append, first-all, extension, dups-def, delpos-in, delpos-atsizeid, delete-one-nls, del-rmdup-length-nle, del-length, blastN-firstN, at-last, append-mod, app-05-neg,
nat-basic2/z-01 is used by sublist-part, sublist-move, sublist-append-04, rest-sub, rest-len, put-firstn-restn, possize-notin, pos-equal, lastn-restn-01, lastn-restn, lastn-mklist, lastn-lastn-01, lastn-app, lastN-rest-01, l-02, firstn-prefix-04, firstn-length-02, firstn-butlast, firstn-append-01, firstN-lastN, first-mklist, extension, append-mod,

Used from specification nat-basic1

nat-basic1/f is used by sublist-prefix, sublist-mklist-01, sublist-mklist, sublist-lenrec-01, sublist-lenrec, sublist-last, sublist-first-skip, sublist-at, rmtoobigpos, rmpos-size, rmpos-in, rmpos-get, restn-nonempty-2, restn-nonempty, restn-less, restn-last, restn-firstn-better, restn-firstn, restn-first-get, restn-empty, restN-append, rest-mklist-01, rest-append, putset-same, put-sw-in, put-length, put-in-02, put-in-01, put-in, put-firstn-restn, put-del1-in, put-at-eq, put-at, put-app-left, pos-get, len-01, lastn-restn-01, lastn-restn, lastn-neq-01, lastn-mklist, lastn-lastn-01, lastN-rest, lastN-in, lastN-ex, lastN-append-01, inl-01, inl, get-restn, get-nodups, get-mklist-01, get-last-04, get-in, get-firstn, get-butlast, get-append-less, firstrestex, firstn-restn-in, firstn-restn-eq, firstn-prefix-04, firstn-prefix-03, firstn-prefix-02, firstn-last-rec, firstn-last-eq, firstn-last-01, firstn-last, firstn-firstn, firstn-butlast-intro, firstn-at-in-dups, firstN-lastN-in-01, firstN-lastN, firstN-dups-05, firstN-dups-04, firstN-dups-01, firstN-dups, first-mklist-01, first-append-01, first-append, extension, dups-def, delete-one-nls, del-length, append-mod,
nat-basic1/less-1 is used by dups-def,
nat-basic1/lf is used by rmpos-get, firstn-at-in-dups,
nat-basic1/lf-01 is used by rmpos-size, put-firstn-restn, lastn-mklist, get-last-04, get-firstn, firstn-last-01, firstn-at-in-dups, extension,
nat-basic1/lf-02 is used by rmpos-get, put-firstn-restn, lastn-restn-01, lastN-ex, get-firstn, firstn-prefix-04, firstn-prefix-03, firstn-prefix-02, firstn-last-eq, firstn-at-in-dups, firstN-lastN,
nat-basic1/ls-02 is used by rmpos-get, put-firstn-restn, lastN-rest, firstn-at-in-dups,
nat-basic1/one-01 is used by size-del-nodups, rmpos-size, rmpos-in, rmpos-get, pos-get, lastn-app, l, get-rec, get-mklist-01, get-mklist, del-rmdup-length-nle,
nat-basic1/ref-1 is used by sublist-mklist-01, restN-len, rest-mklist-02, put-last, lastn-app, lastN-blastN, lastN-all, get-mklist, get-last-04, get-app-1, first-mklist-02, del-rmdup-length-nle,
nat-basic1/trans is used by lastN-rest,
nat-basic1/trans-1 is used by rmpos-get, lastN-rest, firstn-at-in-dups,
nat-basic1/z is used by get-mklist-01,
nat-basic1/zero is used by sublist-move, sublist-append-04, restn-nonempty-2, restn-nonempty, restn-last, restn-first-get, restn-empty, restN-dups, rest-rec, putset-same, num-lastN, lastn-restn, lastN-blastN, get-last-nonempty,
nat-basic1/zero-01 is used by rmpos-in, restn-nonempty, restn-last, restn-first-get, restn-at, put-sw-in, put-in-02, put-in-01, put-in, put-del1-in, put-at-eq, put-at, put-app-left, lastN-dups, get-butlast, extension,