[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 from-cons-one, one-inf, tl-inf-1, appinf-one-to-succ2, appinf-one-get-succ2, tl-lem, cons-eq-inf, appinf-one-to-succ, to-succ-cons, cons-eq, get-cons-succ, appinf-one-get-succ,
nat/anti is used by append-from-ge-01, appinf-to-ge,
nat/cancel-01 is used by append-to-gr-01, from-append-add,
nat/elim-pred-c is used by cons-to-addnum, cons-eq-inf, contractinf-from1, contractinf-tl, cons-to-num, from-succ, to-unwind-end, intrace-expand, cons-from-num, get-finto, get-infto, expand-cons, get-cons-num, elim-hd-tl, append-to-gr-01, cons-from-addnum,
nat/elim-sub is used by append-from-gr-01, get-append-notls, swap-to-from-app, length-from, appinf-to-split, to-plus-from-inf-simp, swap-to-from, swap-inf-to-from-app, append-assoc, from-append-tofrom, append-from-gt, append-to-gr-01, swap-inf-to-from, append-to-gr,
nat/eq-01 is used by get-append-notls, append-from-addsize, swap-to-from-app, to-append-add, appinf-to-ge-01, swap-inf-to-from-app, append-assoc, appinf-get-ge-01, append-to-addsize, elim-fromto, append-to-addsize-01, append-to-gr-01, from-append-add,
nat/eqle-one is used by to-to-leq, to-to-leq-inf,
nat/fle is used by to-to-leq, appinf-to-split, fin-to-to-ls, get-finto,
nat/fle-01 is used by to-to-leq, append-assoc, from-append-tofrom,
nat/l-num-05 is used by to-inf-two,
nat/l-num-06 is used by appinf-one-get-succ2, append-to-gr-01,
nat/le-add is used by append-from-addsize, swap-to-from-app, to-append-add, appinf-to-ge-01, append-to-addsize, append-to-addsize-01,
nat/le-def is used by append-to-size, append-from-addsize, to-to-leq, swap-to-from-app, appinf-to-split, appinf-to-ge-01, to-to-leq-inf, append-to-size-01, append-assoc, from-append-tofrom, less-size-from, size-from-less, from-append-add,
nat/le-ls-simp is used by fin-to-to-leq, appinf-get-ge, appinf-to-split, fin-to-to-eq, to-empty-fin2, fin-to-to-ls, from-append-tofrom, get-finto, ton-fromn-fin, elim-fromto, get-from, from-append-add,
nat/le-num-06 is used by appinf-one-to-succ2,
nat/lels is used by get-append-notls, get-toinf, elim-fromto-fin, append-from-addsize, to-to-leq, swap-to-from-app, get-to, fin-to-to-leq, length-from, to-append-add, appinf-to-split, to-plus-from-inf-simp, append-from-ge-01, to-from-01, get-from-01, to-to-leq-inf, fin-to-to-eq, from-succ, to-empty2, fin-to-to-ls, from-from, append-assoc, toinf-to-leq, to-unwind-end-fin, from-append-tofrom, get-finto, to-inf-two, ton-fromn-fin, append-from-ge-02, append-to-addsize, elim-fromto, append-to-addsize-01, get-infto, length-to, size-from, append-le-to, get-from, size-from-less, size-to, fin-size-from, ton-fromn, from-append-add,
nat/lels-03 is used by append-from-gr-01, to-to-leq, appinf-to-split, to-to-ls, append-from-gt, append-to-gr-01, append-to-gr,
nat/lep is used by get-append-notls, swap-to-from-app, length-from, swap-to-from, swap-inf-to-from-app, from-append-tofrom, elim-fromto, swap-inf-to-from,
nat/lep-02 is used by append-to-le-01, to-to-leq, append-to-le, append-from-le, to-to-leq-inf, from-from, get-finto, to-plus-from-fin, append-from-le-01,
nat/ler is used by to-to-leq, to-to-eq, to-to-leq-inf, to-to-eq-inf, append-from-ge-02,
nat/les is used by to-to-leq, to-to-leq-inf,
nat/let is used by to-to-leq, fin-to-to-leq, get-finto,
nat/lez is used by to-to-leq, get-finto,
nat/lez-01 is used by append-to-le-01, to-to-leq, append-to-le, append-from-le, to-to-leq-inf, from-from, to-plus-from-fin, append-from-le-01,
nat/ls is used by less-size-from, from-append-add,
nat/ls-01 is used by appinf-to-split, append-assoc, from-append-tofrom, size-from-less,
nat/ls-le-simp is used by get-toinf, get-to, appinf-to-split, to-plus-from-inf-simp, from-append-tofrom, to-inf-two, elim-fromto, size-from, size-from-less, size-to, fin-size-from, ton-fromn, from-append-add,
nat/pred-03 is used by cons-append, from-cons-one, one-inf, tl-inf-1, get-cons-zero, from-succ, to-unwind-end, to-succ-cons, intrace-expand, get-cons-succ, expand-cons, elim-hd-tl,
nat/prop-07 is used by appinf-to-split,
nat/sub-base is used by empty-append, append-to-gr-01,
nat/succ-01 is used by to-to-leq, appinf-one-to-succ, to-from-01, get-from-01, from-succ, to-unwind-end-fin, get-finto, get-infto, length-to,
nat/zero is used by to-to-leq, swap-to-from-app, append-from-ge-01, to-to-leq-inf, ton-fromn-fin, append-from-ge-02, ton-fromn-inf,
nat/zero-01 is used by lslen-fromnotempty-list,
nat/zero-02 is used by appinf-to-ge,

Used from specification nat-inf

nat-inf/notinf-fin is used by leq-prefix,
nat-inf/num-add is used by toinf-add,
nat-inf/add-all-inf is used by size-append, toinftoinf-append-add,
nat-inf/add-all-zero is used by from-to-exchange, get-from-zero,
nat-inf/add-assoc is used by from-infto-exchange, toinf-empty3, toinfto-append-add, from-to-exchange, leq-prefix, swap-to-from-app, contractinf-from1, size-append, append-notsmallersize2, to-append-add, contractinf-tl, toinftoinf-append-add, to-unwind-end, from-from, extensionality-to, get-from-zero, nlslen-lslensn-eqlensn, from-append-tofrom, size-succ, prefix-notsmallersize, less-size-from, to-empty3, get-from, size-from-less, append-notsmallersize1, from-append-add, from-append-toinffrom,
nat-inf/add-cancel-num-02 is used by from-to-exchange,
nat-inf/add-comm is used by from-infto-exchange, toinf-empty3, toinfto-append-add, from-to-exchange, leq-prefix, swap-to-from-app, contractinf-from1, size-append, append-notsmallersize2, to-append-add, contractinf-tl, swap-to-from, toinftoinf-append-add, to-unwind-end, from-from, extensionality-to, get-from-zero, nlslen-lslensn-eqlensn, from-append-tofrom, size-succ, prefix-notsmallersize, less-size-from, to-empty3, get-from, size-from-less, append-notsmallersize1, from-append-add, from-append-toinffrom,
nat-inf/add-fin is used by from-to-exchange, swap-to-from-app, size-append, to-append-add, swap-to-from, to-unwind-end, swap-inf-to-from-app, from-from, extensionality-to, from-append-tofrom, less-size-from, to-empty3, size-from-less, from-append-add, from-append-toinffrom,
nat-inf/add-inf1 is used by contractinf-tl,
nat-inf/add-inf2 is used by from-infto-exchange, toinf-empty3, toinfto-append-add, contractinf-from1, size-append, from-append-add, from-append-toinffrom,
nat-inf/add-less-fin-01 is used by leq-prefix,
nat-inf/add-ls-cancel-01 is used by from-append-add,
nat-inf/add-ls-cancel-num-04 is used by from-to-exchange,
nat-inf/add-not-less is used by append-notsmallersize2, prefix-notsmallersize, append-notsmallersize1,
nat-inf/addeqinf-cancel is used by less-size-from, from-append-add,
nat-inf/disj-rqui-infty is used by extensionality, finlen-tolen-02, zero-len, size-empty-equiv, swap-to-from-app, appendend-equal, append-cut1, append-split, finlen-tolen, inf-size-from, toinf-empty2, append-from-ge-02, elim-fromto, less-size-from, size-from, toinf-empty, from-append-add,
nat-inf/eq-natinf-to-nat-2-2 is used by size-append,
nat-inf/inf-less is used by toinfto-append-add, append-toinf-ls, size-toinf, toinf-empty2, less-size-from, from-append-add, from-append-toinffrom,
nat-inf/inj-rqui is used by extensionality, finlen-tolen-02, zero-len, size-empty-equiv, size-empty, size-toinf, elim-fromto-inf, inf-size-to, append-split, finlen-tolen, append-from-ge-02, elim-fromto, size-from, size-to-02, append-split-fin, fin-size-from, from-append-add,
nat-inf/lele-refl is used by append-from-ge-02,
nat-inf/lele-trans is used by toinf-to-leq, from-append-tofrom,
nat-inf/lels-trans is used by extensionality-to, from-append-tofrom,
nat-inf/less-fin is used by extensionality, get-append-notls, get-toinf, leq-prefix, to-to-leq, append-from-gr-02, get-to, fin-to-to-leq, contractinf-from1, toinf-to-ls, contractinf-tl, to-from-01, fin-to-to-eq, from-succ, lslen-fromnotempty, to-empty2, to-unwind-end, fin-to-to-ls, toinf-to-leq, from-append-tofrom, append-gr-to, size-succ, append-from-ge-02, elim-fromto, to-unwind-begin, less-size-from, get-append-ls, size-from, append-le-to, size-from-less, size-to, fin-size-from, to-empty, ton-fromn, from-append-add,
nat-inf/less-inf1 is used by toinf-to-leq-inf, toinf-to-eq-inf, get-inftoinf, toinf-empty3, append-from-gr-02, swap-inf-from-to, elim-fromto-inf, swap-inf-to-from-app, from-from, from-append-tofrom, append-gr-to, size-succ, elim-fromto, toinf-empty, size-from-less, from-append-add, size-inf-toinf, from-append-toinffrom,
nat-inf/less-inf2 is used by extensionality, get-append-notls, contractinf-from1, contractinf-tl, from-succ, to-unwind-end, size-succ, less-size-from,
nat-inf/less-succ-leq is used by to-unwind-end, size-succ,
nat-inf/ls-le is used by to-is-prefix,
nat-inf/ls-lsadd is used by from-append-tofrom, size-from-less,
nat-inf/ls-natinf-to-nat-1-2 is used by swap-to-from-app, to-append-add, from-from, from-append-tofrom, size-from-less,
nat-inf/ls-natinf-to-nat-2-1 is used by from-append-tofrom, less-size-from, get-from,
nat-inf/ls-natinf-to-nat-2-2 is used by from-append-tofrom,
nat-inf/ls-notlssucc is used by nlslen-lslensn-eqlensn,
nat-inf/ls-one is used by to-empty4,
nat-inf/lsle-trans is used by get-toinf, toinf-to-ls, extensionality-to,
nat-inf/prime-add-fin is used by swap-to-from-app,
nat-inf/sel-rqui-dotn is used by get-append-notls, append-from-gr-02, swap-to-from-app, contractinf-from1, contractinf-tl, append-from-ge-02, size-from, fin-size-from, from-append-add,
nat-inf/zerols-neqzero is used by zero-len, from-to-exchange,

Used from specification stream-basic

stream-basic/disj-rqui-rqui0 is used by neq-fin-inf-03,
stream-basic/inj-rqui is used by eq-stream-to-list-2-2, append-empty-01, eq-stream-to-list-3-2, fin-empty, eq-stream-to-list-2-1,
stream-basic/inj-rqui0 is used by cons-eq,
stream-basic/sel-rqui-dotl is used by extract-empty,
stream-basic/disj-rqui-rqui0 is used by neq-fin-inf-01, appfin-sel, appfin-sel-01, cons-eq-inf, cons-eq, inf-not-toinf-exceptinf, fun-nonempty, elim-fromto, neq-fin-inf-03, inf-not-to,
stream-basic/elim-finp-ant is used by appendend-equal, fin-size-from, from-append-add,
stream-basic/elim-finp-suc is used by appfin-sel, appfin-sel-01, appendend-equal, from-append-add,
stream-basic/elim-rqui is used by appfin-sel, appfin-sel-01,
stream-basic/inj-rqui is used by extensionality, from-infto-exchange, append-toinf-ls, from-zero, tl-lem, toinf-to-eq, tl-fin-1, from-succ-cons, toinflen, elim-fromto-inf, append-split, from-from, cons-eq-01, finlen-tolen, cons-eq, empty-append, append-empty, elim-fromto, append-split-fin, append-cancel-l-02,
stream-basic/inj-rqui0 is used by extensionality, cons-append, from-cons-one, from-zero, tl-inf-1, tl-lem, cons-eq-inf, to-plus-from-inf-simp, from-succ-cons, toinflen, elim-fromto-inf, from-succ, appinf-selfun, append-cut1, append-split, from-from, append-assoc, cons-eq, inf-not-toinf-exceptinf, intrace-expand, empty-append, append-empty, append-eq-inf, elim-fromto, expand-cons, neq-fin-inf-03, elim-hd-tl, append-cancel-l-02,
stream-basic/sel-rqui-dotl is used by finlen-tolen-02, to-append-add, finlen-tolen, append-gr-to,
stream-basic/sel-rqui0-dotf is used by appinf-one2-to-succ2, appinf-get-le, appinf-one2-to-succ, appinf-get-ge, appinf-to-split, elim-fromto-inf, appinf-selfun, appinf-get-ge-01, appinf-get-split, appinf-one2-get-succ2, appinf-one2-get-succ,
stream-basic/test-finp-rqui is used by append-split, append-split-fin, append-cancel-l-02,
stream-basic/test-finp-rqui0 is used by append-split, append-cancel-l-02,

Used from specification list-getput

list-getput/extension is used by extensionality, appinf-to-split, to-empty-fin2, from-append-tofrom, to-inf-two, ton-fromn-fin, elim-fromto, lslen-fromnotempty-list, ton-fromn-inf,
list-getput/get-zero-01 is used by toone-equal,

Used from specification list-data

list-data/elim-list-c is used by toone-equal, to-unwind-begin-fin,
list-data/l is used by extensionality, zero-len, size-empty-equiv, to-to-leq, to-empty-fin, to-from-01, get-from-01, from-succ, to-unwind-end, append-split, fin-to-to-ls, append-assoc, to-unwind-end-fin, get-finto, length-to, get-append-ls, to-unwind-begin-fin, lslen-fromnotempty-list, from-append-add,
list-data/size-nil is used by append-to-le-01, size-inf-to, size-empty, append-from-addsize-01, to-empty-fin, length-from, append-to-le, append-from-le, to-empty-fin2, from-all, append-split, from-from, to-empty-inf, empty-append, append-from-gt, ton-fromn-fin, to-plus-from-fin, length-to, lslen-fromnotempty-list, to-all, to-attach, append-to-gr-01, append-to-gr, ton-fromn-inf, append-from-le-01,

Used from specification nat-basic

nat-basic/a is used by appinf-one2-to-succ2, append-from-gr-01, append-to-le-01, from-cons-one, size-inf-to, toinf-empty3, one-inf, get-append-notls, toinfto-append-add, tl-inf-1, appinf-one-to-succ2, single-to-one, append-from-addsize, appinf-one-get-succ2, tl-lem, cons-to-addnum, from-to-exchange, to-to-leq, cons-eq-inf, append-from-addsize-01, appinf-one-to-succ, swap-to-from-app, contractinf-from1, appinf-one2-to-succ, size-append, length-from, to-append-add, appinf-to-split, append-from-size, from-from-inf, appinf-to-ge-01, to-from-01, from-succ-cons, get-from-01, to-succ2-nf, append-to-le, append-from-le, from-cons-one-fin, to-to-leq-inf, to-inf-one, cons-to-num, from-succ, swap-to-from, to-unwind-end, swap-inf-to-from-app, from-all, append-split, to-succ-cons, from-from, extensionality-to, append-assoc, cons-eq, get-from-zero, intrace-expand, cons-from-num, from-nf-zero, to-unwind-end-fin, from-append-tofrom, get-finto, to-inf-two, appinf-get-ge-01, append-from-gt, append-to-addsize, elim-fromto, get-cons-succ, to-plus-from-fin, append-to-addsize-01, to-unwind-begin, append-from-size-01, get-infto, length-to, less-size-from, to-unwind-begin-fin, appinf-one2-get-succ2, to-empty3, expand-cons, to-all, get-cons-num, to-attach, size-from-less, to-unwind-end-inf, toone-cons-fin, appinf-one2-get-succ, append-to-gr-01, swap-inf-to-from, to-succ3-nf, appinf-one-get-succ, cons-from-addnum, append-to-gr, get-from-inf-zero, from-append-add, from-append-toinffrom, append-from-le-01,
nat-basic/add-base is used by from-cons-one, one-inf, append-from-addsize, from-to-exchange, cons-eq-inf, append-from-addsize-01, appinf-one-to-succ, swap-to-from-app, length-from, to-append-add, append-from-size, appinf-to-ge-01, get-from-01, from-succ, to-succ-cons, from-from, cons-eq, get-from-zero, from-nf-zero, append-from-gt, append-to-addsize, get-cons-succ, append-to-addsize-01, append-from-size-01, appinf-one-get-succ, append-to-gr, get-from-inf-zero,
nat-basic/c is used by appinf-one2-to-succ2, append-from-gr-01, append-to-le-01, from-cons-one, size-inf-to, toinf-empty3, one-inf, get-append-notls, toinfto-append-add, tl-inf-1, appinf-one-to-succ2, single-to-one, append-from-addsize, appinf-one-get-succ2, tl-lem, cons-to-addnum, from-to-exchange, to-to-leq, get-from-inf, cons-eq-inf, append-from-addsize-01, appinf-one-to-succ, swap-to-from-app, contractinf-from1, appinf-one2-to-succ, size-append, length-from, to-append-add, appinf-to-split, append-from-size, from-from-inf, appinf-to-ge-01, to-from-01, from-succ-cons, get-from-01, to-succ2-nf, append-to-le, append-from-le, from-cons-one-fin, to-to-leq-inf, to-inf-one, cons-to-num, from-succ, swap-to-from, to-unwind-end, swap-inf-to-from-app, from-all, append-split, to-succ-cons, from-from, extensionality-to, append-assoc, cons-eq, get-from-zero, intrace-expand, cons-from-num, from-nf-zero, to-unwind-end-fin, from-append-tofrom, get-finto, to-inf-two, appinf-get-ge-01, append-from-gt, append-to-addsize, elim-fromto, get-cons-succ, to-plus-from-fin, append-to-addsize-01, to-unwind-begin, append-from-size-01, get-infto, length-to, less-size-from, to-unwind-begin-fin, appinf-one2-get-succ2, to-empty3, get-from, expand-cons, to-all, get-cons-num, to-attach, size-from-less, to-unwind-end-inf, toone-cons-fin, appinf-one2-get-succ, append-to-gr-01, swap-inf-to-from, to-succ3-nf, appinf-one-get-succ, cons-from-addnum, append-to-gr, get-from-inf-zero, from-append-add, from-append-toinffrom, append-from-le-01,
nat-basic/eq-01 is used by size-inf-to, length-from, append-split, from-append-tofrom, length-to,
nat-basic/f is used by extensionality, append-from-gr-01, to-to-leq, get-to, to-empty-fin, appinf-to-split, to-to-ls, to-from-01, get-from-01, to-to-leq-inf, from-succ, to-unwind-end, fin-to-to-ls, append-assoc, to-unwind-end-fin, from-append-tofrom, get-finto, to-inf-two, append-from-gt, get-infto, length-to, get-append-ls, to-unwind-begin-fin, lslen-fromnotempty-list, append-to-gr-01, append-to-gr, from-append-add,
nat-basic/l is used by from-append-tofrom, append-to-gr-01, from-append-add,
nat-basic/l-01 is used by swap-to-from-app, appinf-to-split, from-append-tofrom, append-from-gt, append-to-gr-01, append-to-gr,
nat-basic/l-02 is used by get-append-notls, swap-to-from-app, appinf-to-ge-01, append-assoc, from-append-tofrom, appinf-get-ge-01, elim-fromto, from-append-add,
nat-basic/less-zero is used by to-unwind-end, get-finto, empty-append, ton-fromn-fin, to-unwind-begin, get-infto, ton-fromn-inf,
nat-basic/lf-01 is used by extensionality, to-to-leq, to-to-leq-inf,
nat-basic/ls-02 is used by to-to-leq, to-empty-fin, less-size-from, lslen-fromnotempty-list,
nat-basic/nls-fst is used by appinf-one-get-succ,
nat-basic/one-01 is used by cons-append, tl-lem, cons-eq-inf, appinf-one-to-succ, contractinf-from1, contractinf-tl, hd-lem, cons-eq, get-finto, to-inf-two, get-infto,
nat-basic/oz is used by from-cons-one, one-inf, tl-inf-1, tl-lem, cons-to-addnum, to-to-leq, cons-eq-inf, contractinf-from1, length-from, from-succ-cons, to-to-leq-inf, cons-to-num, from-succ, to-unwind-end, append-split, to-succ-cons, cons-eq, intrace-expand, get-finto, get-cons-succ, get-infto, expand-cons, append-to-gr-01,
nat-basic/pred is used by from-succ-cons,
nat-basic/refl-nat is used by append-to-size, append-from-addsize, leq-prefix, to-to-leq, to-to-leq-inf, append-to-size-01, ton-fromn-fin, ton-fromn-inf,
nat-basic/s-04 is used by to-to-leq, to-from-01, get-from-01, to-to-leq-inf, from-succ, to-unwind-end-fin, get-finto, get-infto, length-to,
nat-basic/succ is used by append-to-le-01, size-inf-to, tl-inf-1, tl-lem, from-to-exchange, to-to-leq, append-from-addsize-01, length-from, contractinf-tl, to-from-01, get-from-01, append-to-le, append-from-le, to-to-leq-inf, from-succ, to-unwind-end, from-all, from-from, to-unwind-end-fin, get-finto, to-inf-two, append-from-gt, to-plus-from-fin, get-infto, length-to, to-all, to-attach, elim-hd-tl, to-unwind-end-inf, append-to-gr-01, append-to-gr, append-from-le-01,
nat-basic/z-01 is used by length-from, from-from, to-empty3,
nat-basic/z-02 is used by tl-inf-1, tl-lem,

Used from specification list

list/c is used by to-succ-cons-l-lem, tl-fin-1, from-succ-cons-l-lem, tl-fin-lem, hd-fin-lem,
list/c-06 is used by append-split,
list/Nil is used by append-from-addsize, append-to-le, append-from-le, to-unwind-end, to-unwind-end-fin, empty-append, append-from-gt, to-plus-from-fin, to-attach, to-unwind-end-inf, append-to-gr-01, append-to-gr,
list/a is used by appinf-one2-to-succ2, append-to-le-01, cons-append, size-inf-to, eq-stream-to-list-3-3, get-append-notls, toinfto-append-add, appinf-one-to-succ2, single-to-one, elim-fromto-fin, append-from-addsize, cons-to-addnum, from-to-exchange, tl-fin-1, to-to-leq, append-from-addsize-01, appinf-one-to-succ, toone-equal, appinf-one2-to-succ, size-append, length-from, to-append-add, appinf-to-split, eq-stream-to-list-3-1, appinf-to-ge-01, to-from-01, from-succ-cons, get-from-01, constrrew, get-cons-zero, append-to-le, append-from-le, to-to-leq-inf, to-inf-one, toone-cons, cons-to-num, from-succ, to-unwind-end, from-all, append-split, to-succ-cons, from-from, cons-eq-01, extensionality-to, append-empty-01, append-assoc, cons-eq, appinf-to-ge, to-unwind-end-fin, from-append-tofrom, get-finto, append-gr-to, to-inf-two, empty-append, append-empty, append-from-gt, eq-stream-to-list-3-2, append-to-addsize, elim-fromto, get-cons-succ, to-plus-from-fin, append-to-addsize-01, to-unwind-begin, get-infto, length-to, get-append-ls, to-unwind-begin-fin, expand-cons, to-all, to-attach, elim-hd-tl, get-append3-fin, to-unwind-end-inf, toone-cons-fin, append-to-gr-01, eq-stream-to-list-2-1, append-to-gr, from-append-add, append-cancel-l-02, append-from-le-01,
list/app is used by single-to-one, appinf-one-to-succ, to-append-add, to-inf-one, to-unwind-end, to-unwind-end-fin, append-empty, append-to-addsize, append-to-addsize-01, toone-cons-fin,
list/app-02 is used by append-empty-01,
list/app-04 is used by appinf-to-ge, append-cancel-l-02,
list/app-06 is used by extensionality-to,
list/c is used by append-to-le-01, cons-append, size-inf-to, single-to-one, cons-to-addnum, from-to-exchange, tl-fin-1, append-from-addsize-01, toone-equal, length-from, to-from-01, get-from-01, constrrew, to-succ2-nf, append-to-le, append-from-le, to-inf-one, cons-to-num, from-succ, to-unwind-end, from-all, append-split, to-succ-cons, from-from, to-unwind-end-fin, get-finto, append-from-gt, to-plus-from-fin, to-unwind-begin, get-infto, length-to, to-unwind-begin-fin, expand-cons, to-all, to-attach, elim-hd-tl, to-unwind-end-inf, toone-cons-fin, append-to-gr-01, to-succ3-nf, append-to-gr, append-from-le-01,
list/c-03 is used by cons-eq-01,
list/c-04 is used by appinf-one-to-succ, toone-equal, toone-cons, to-unwind-end, to-unwind-end-fin, to-unwind-end-inf, toone-one,
list/c-06 is used by cons-eq,
list/e is used by cons-empty, toone-cons,
list/e-01 is used by to-from-01, get-from-01, from-succ, to-unwind-end-fin, get-finto, length-to, expand-cons, append-to-gr-01,
list/in-15 is used by to-unwind-end, extensionality-to,
list/len is used by to-to-leq, size-append, appinf-to-split, to-to-leq-inf, append-split, append-assoc, from-append-tofrom, elim-fromto, from-append-add,
list/len-01 is used by appinf-one2-to-succ2, append-to-le-01, appinf-one-to-succ2, cons-to-addnum, appinf-one2-to-succ, to-append-add, appinf-to-ge-01, append-to-le, append-from-le, cons-to-num, from-succ, to-unwind-end, append-split, to-succ-cons, to-unwind-end-fin, append-gr-to, append-to-addsize, to-plus-from-fin, append-to-addsize-01, to-unwind-begin, to-unwind-begin-fin, to-all, to-attach, to-unwind-end-inf, append-to-gr-01, append-to-gr,
list/len-02 is used by cons-append, appinf-one-to-succ2, appinf-one-get-succ2, tl-lem, from-to-exchange, to-to-leq, cons-eq-inf, appinf-one-to-succ, contractinf-from1, contractinf-tl, hd-lem, to-to-leq-inf, to-unwind-end, append-split, appinf-one-get-zero, cons-eq, get-finto, to-inf-two, get-infto, appinf-one-get-succ,
list/len-05 is used by append-to-le-01, size-inf-to, append-from-addsize-01, length-from, to-from-01, get-from-01, append-to-le, append-from-le, from-succ, from-all, from-from, to-unwind-end-fin, get-finto, to-inf-two, append-from-gt, to-plus-from-fin, length-to, to-all, to-attach, append-to-gr-01, append-to-gr, append-from-le-01,
list/len-06 is used by to-to-leq, to-to-leq-inf,

Used from specification list-del

list-del/get-append-grt is used by to-to-leq, to-to-leq-inf, get-finto, get-infto, from-append-add,
list-del/get-append-less is used by from-append-tofrom,
list-del/get-numrec is used by from-succ,
list-del/get-append-grt is used by appinf-to-split, append-assoc, from-append-tofrom, get-finto,
list-del/get-append-grt-02 is used by get-append-notls,
list-del/get-append-less is used by appinf-to-split, append-assoc, get-finto, get-infto, get-append-ls, from-append-add,
list-del/get-butlast is used by to-to-leq, to-to-leq-inf,
list-del/get-succ is used by get-from-01, to-unwind-end-fin, to-inf-two, get-cons-succ,
list-del/get-zero is used by get-cons-zero, from-succ, to-unwind-end-fin, to-inf-two,
list-del/one-03 is used by cons-append, tl-lem, to-to-leq, cons-eq-inf, contractinf-from1, contractinf-tl, hd-lem, to-to-leq-inf, appinf-one-get-zero, cons-eq, to-inf-two, get-infto,