Used simplifier rules/spec theorems by specification

Used from specification nat-inf-basic

• nat-inf-basic/disj is used by zero-len, toinf-empty2, toinf-empty, swap-to-from-app, size-empty-equiv, less-size-from, inf-size-from, from-append-add, finlen-tolen, extensionality, elim-fromto, appendend-equal, append-split, append-from-ge-02, append-cut1,
• nat-inf-basic/elim is used by swap-to-from-app,
• nat-inf-basic/inj is used by zero-len, swap-to-from-app, swap-from-to, size-toinf, size-to, size-empty-equiv, size-empty, inf-size-to, from-append-add, finlen-tolen, fin-size-from2, fin-size-from, extensionality-to, extensionality, elim-fromto-inf, elim-fromto, append-split, append-from-ge-02,
• nat-inf-basic/sel is used by to-append-add, swap-to-from-app, swap-from-to, get-append-notls, from-append-tofrom, from-append-add, fin-size-from2, fin-size-from, contractinf-tl, contractinf-from1, append-from-gr-02, append-from-ge-02,

Used from specification nat

• nat/add-01 is used by to-succ-cons, tl-lem, tl-inf-1, one-inf, get-cons-succ, from-cons-one, cons-eq-inf, cons-eq,
• nat/anti is used by from-append-add, append-from-ge-01,
• nat/cancel-01 is used by swap-to-from-app, from-append-add, append-to-gr-01,
• nat/elim-pred-c is used by to-unwind-end, intrace-expand, get-infto, get-finto, get-cons-num, from-succ, expand-cons, elim-hd-tl, contractinf-tl, contractinf-from1, cons-to-num, cons-to-addnum, cons-from-num, cons-from-addnum, cons-eq-inf, append-to-gr-01,
• nat/elim-sub is used by to-plus-from-inf-simp, swap-to-from-app, swap-to-from, swap-inf-to-from-app, swap-inf-to-from, length-from, get-append-notls, from-append-tofrom, from-append-add, append-to-gr-01, append-to-gr, append-from-gt, append-from-gr-01, append-assoc,
• nat/eq-01 is used by swap-to-from-app, swap-inf-to-from-app, swap-from-to, get-append-notls, from-infto-exchange, from-append-add, elim-fromto, append-to-gr-01, append-to-addsize-01, append-to-addsize, append-from-addsize, append-cancel-l, append-assoc,
• nat/eqle-one is used by to-to-leq-inf, to-to-leq,
• nat/fle is used by to-to-leq, swap-from-to, get-finto,
• nat/fle-01 is used by to-to-leq, swap-from-to, from-append-tofrom, append-assoc,
• nat/le-add is used by swap-to-from-app, from-append-add, append-to-addsize-01, append-to-addsize, append-from-addsize,
• nat/le-ls-simp is used by ton-fromn-fin, ton-fromn, to-empty-fin2, swap-to-from-app, swap-from-to, get-from, get-finto, from-append-tofrom, from-append-add, elim-fromto,
• nat/lels is used by ton-fromn-fin, ton-fromn, toinf-to-leq, to-unwind-end-fin, to-to-leq-inf, to-to-leq, to-plus-from-inf-simp, to-from-01, to-empty2, to-append-add, swap-to-from-app, swap-from-to, size-to-02, size-to, size-from-less, length-to, length-from, get-toinf, get-to-02, get-to, get-infto, get-from-01, get-from, get-finto, get-append-notls, from-succ, from-from, from-append-tofrom, from-append-add, fin-size-from2, elim-fromto-fin, elim-fromto, append-to-ls, append-to-addsize-01, append-to-addsize, append-from-ge-02, append-from-ge-01, append-from-addsize, append-assoc,
• nat/lels-01 is used by to-to-leq-inf, to-to-leq, to-plus-from-inf-simp, to-append-add, swap-from-to, size-from-less, less-size-from, from-append-tofrom, append-to-size-01, append-to-size, append-from-addsize, append-assoc,
• nat/lels-03 is used by to-to-ls, to-to-leq, from-append-tofrom, from-append-add, append-to-gr-01, append-to-gr, append-from-gt, append-from-gr-01,
• nat/lep is used by swap-to-from-app, swap-to-from, swap-inf-to-from-app, swap-inf-to-from, length-from, get-append-notls, from-infto-exchange, from-append-tofrom, elim-fromto,
• nat/lep-02 is used by to-to-leq-inf, to-to-leq, to-plus-from-fin, swap-from-to, get-finto, from-from, append-to-le-01, append-to-le, append-from-le-01, append-from-le,
• nat/ler is used by to-to-leq-inf, to-to-leq, to-to-eq-inf, to-to-eq, from-append-add, append-from-ge-02,
• nat/les is used by to-to-leq-inf, to-to-leq,
• nat/let is used by to-to-leq, swap-from-to, get-finto,
• nat/lez is used by to-to-leq, swap-to-from-app,
• nat/lez-01 is used by to-to-leq-inf, to-to-leq, to-plus-from-fin, from-from, append-to-le-01, append-to-le, append-from-le-01, append-from-le,
• nat/ls is used by less-size-from, from-append-add,
• nat/ls-01 is used by to-append-add, swap-from-to, size-from-less, from-append-tofrom, append-assoc,
• nat/ls-le-simp is used by to-plus-from-inf-simp, to-append-add, swap-to-from-app, swap-from-to, size-to-02, size-to, size-from-less, get-toinf, get-to-02, get-to, from-append-tofrom, fin-size-from2, elim-fromto,
• nat/pred-03 is used by to-unwind-end, to-succ-cons, tl-inf-1, one-inf, intrace-expand, get-cons-zero, get-cons-succ, from-succ, from-cons-one, expand-cons, elim-hd-tl, cons-append,
• nat/sub-base is used by swap-to-from-app, empty-append, append-to-gr-01,
• nat/succ-01 is used by to-unwind-end-fin, to-to-leq, to-from-01, length-to, get-infto, get-from-01, get-finto, from-succ,
• nat/zero is used by ton-fromn-inf, ton-fromn-fin, to-to-leq-inf, to-to-leq, from-append-add, append-from-ge-02, append-from-ge-01,
• nat/zero-01 is used by lslen-fromnotempty-list,

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 zero-len, to-unwind-end-fin, to-unwind-end, to-unwind-begin-fin, to-to-leq, to-from-01, to-empty-fin, swap-to-from-app, swap-from-to, size-empty-equiv, lslen-fromnotempty-list, length-to, get-from-01, get-finto, get-append-ls, from-succ, from-append-add, extensionality, append-split, append-assoc,
• list-data/size-01 is used by ton-fromn-inf, ton-fromn-fin, to-plus-from-fin, to-empty-inf, to-empty-fin2, to-empty-fin, to-attach, to-all, size-inf-to, size-empty, lslen-fromnotempty-list, length-to, length-from, from-from, from-append-add, from-all, empty-append, append-to-le-01, append-to-le, append-to-gr-01, append-to-gr, append-split, append-from-le-01, append-from-le, append-from-gt, append-from-addsize-01,

Used from specification list

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

Used from specification stream-basic

• stream-basic/disj is used by neq-fin-inf-03,
• stream-basic/ex is used by finp-empty,
• stream-basic/inj-01 is used by cons-eq,
• stream-basic/inj-02 is used by fin-empty, eq-stream-to-list-3-2, eq-stream-to-list-2-2, eq-stream-to-list-2-1, append-empty-01,
• stream-basic/sel-02 is used by extract-empty, cons-extract-list,
• stream-basic/sel-embed-inf is used by to-plus-from-inf,
• stream-basic/disj is used by neq-fin-inf-03, neq-fin-inf-01, inf-not-to, fun-nonempty, finp-append-02, finp-append-01, elim-fromto, cons-eq-inf, cons-eq, append-cancel-r-04, append-cancel-r-02,
• stream-basic/elim is used by cons-extract-list, append-extract-list-2, append-extract-list,
• stream-basic/inj-01 is used by toinflen, to-plus-from-inf-simp, tl-lem, tl-inf-1, neq-fin-inf-03, intrace-expand, inf-not-toinf-exceptinf, from-zero, from-succ-cons, from-succ, from-from, from-cons-one, from-append-add, extensionality, expand-cons, empty-append, elim-hd-tl, elim-fromto-inf, elim-fromto, cons-eq-inf, cons-eq, cons-append, append-split, append-eq-inf, append-empty, append-cut1, append-cancel-l-02, append-cancel-l, append-assoc,
• stream-basic/inj-02 is used by toone-one, toone-equal, toone-cons, toinflen, toinf-to-leq-inf, to-unwind-end, to-to-leq, tl-lem, tl-fin-1, swap-to-from-app, swap-inf-from-to, leq-prefix, from-zero, from-succ-cons, from-from, from-append-add, finlen-tolen, extensionality-to, extensionality, empty-append, elim-fromto-inf, elim-fromto, cons-eq, append-to-size-01, append-to-ls, append-to-addsize-01, append-split, append-empty, append-cancel-r-04, append-cancel-r-01, append-cancel-l-02,
• stream-basic/sel-01 is used by elim-fromto-inf,
• stream-basic/sel-02 is used by size-to-02, get-to-02, append-extract-list,
• stream-basic/stream-fin-forward is used by swap-to-from-app, swap-from-to, leq-prefix, from-append-tofrom, from-append-add, finp-append-02, finp-append-01, fin-toinf, fin-size-from2, fin-size-from, appendend-equal, append-cancel-r-02, append-cancel-r-01,
• stream-basic/stream-inf-forward is used by swap-to-from-app, notfin-sizeinf, from-append-add, finp-append-02, finp-append-01, fin-toinf,
• stream-basic/test-01 is used by to-plus-from-inf, from-append-add, finp-append-02, fin-toinf, append-split, append-cancel-l-02,
• stream-basic/test-02 is used by swap-to-from-app, swap-from-to, leq-prefix, from-append-tofrom, from-append-add, finp-infto, finp-append-02, fin-to, fin-size-from2, cons-extract-list, append-split, append-extract-list, append-cancel-r-02, append-cancel-l-02,

Used from specification nat-basic2

• nat-basic2/a is used by toone-cons-fin, toinftoinf-append-add, toinf-empty3, to-unwind-end-inf, to-unwind-end-fin, to-unwind-end, to-unwind-begin-fin, to-unwind-begin, to-to-leq-inf, to-to-leq, to-succ-cons, to-plus-from-fin, to-inf-one, to-from-01, to-empty3, to-attach, to-append-add, to-all, tl-lem, tl-inf-1, swap-to-from-app, swap-to-from, swap-inf-to-from-app, swap-inf-to-from, swap-from-to, size-inf-to, size-from-less, size-append, single-to-one, one-inf, less-size-from, length-to, length-from, get-infto, get-from-zero, get-from-inf-zero, get-from-01, get-finto, get-cons-succ, get-cons-num, get-append-notls, from-to-exchange, from-succ-cons, from-succ, from-nf-zero, from-infto-exchange, from-from-inf, from-from, from-cons-one-fin, from-cons-one, from-append-toinffrom, from-append-tofrom, from-append-add, from-all, extensionality-to, elim-fromto, cons-to-num, cons-to-addnum, cons-from-num, cons-from-addnum, cons-eq-inf, cons-eq, append-to-le-01, append-to-le, append-to-gr-01, append-to-gr, append-to-addsize-01, append-to-addsize, append-split, append-from-size-01, append-from-size, append-from-le-01, append-from-le, append-from-gt, append-from-gr-01, append-from-addsize-01, append-from-addsize, append-cancel-l, append-assoc,
• nat-basic2/add-base is used by to-succ-cons, tl-lem, tl-inf-1, swap-to-from-app, one-inf, length-from, get-from-zero, get-from-inf-zero, get-from-01, get-cons-succ, from-to-exchange, from-succ, from-nf-zero, from-from, from-cons-one, from-append-add, cons-eq-inf, cons-eq, append-to-gr, append-to-addsize-01, append-to-addsize, append-from-size-01, append-from-size, append-from-gt, append-from-addsize-01, append-from-addsize,
• nat-basic2/c is used by toone-cons-fin, toinftoinf-append-add, toinf-empty3, to-unwind-end-inf, to-unwind-end-fin, to-unwind-end, to-unwind-begin-fin, to-unwind-begin, to-to-leq-inf, to-to-leq, to-succ-cons, to-plus-from-fin, to-inf-one, to-from-01, to-empty3, to-attach, to-append-add, to-all, tl-lem, tl-inf-1, swap-to-from-app, swap-to-from, swap-inf-to-from-app, swap-inf-to-from, swap-from-to, size-inf-to, size-from-less, size-append, single-to-one, one-inf, less-size-from, length-to, length-from, get-infto, get-from-zero, get-from-inf-zero, get-from-inf, get-from-01, get-from, get-finto, get-cons-succ, get-cons-num, get-append-notls, from-to-exchange, from-succ-cons, from-succ, from-nf-zero, from-infto-exchange, from-from-inf, from-from, from-cons-one-fin, from-cons-one, from-append-toinffrom, from-append-tofrom, from-append-add, from-all, extensionality-to, elim-fromto, cons-to-num, cons-to-addnum, cons-from-num, cons-from-addnum, cons-eq-inf, cons-eq, append-to-le-01, append-to-le, append-to-gr-01, append-to-gr, append-to-addsize-01, append-to-addsize, append-split, append-from-size-01, append-from-size, append-from-le-01, append-from-le, append-from-gt, append-from-gr-01, append-from-addsize-01, append-from-addsize, append-cancel-l, append-assoc,
• nat-basic2/eq-01 is used by swap-to-from-app, size-inf-to, length-to, length-from, append-split,
• nat-basic2/l is used by swap-to-from-app, swap-from-to, from-append-tofrom, from-append-add, append-to-gr-01,
• nat-basic2/l-01 is used by swap-to-from-app, from-append-tofrom, from-append-add, append-to-gr-01, append-to-gr, append-from-gt,
• nat-basic2/l-02 is used by swap-to-from-app, swap-from-to, get-append-notls, from-append-tofrom, from-append-add, elim-fromto, append-cancel-l, append-assoc,
• nat-basic2/l-05 is used by swap-to-from-app,
• nat-basic2/l-06 is used by from-append-add,
• nat-basic2/oz is used by to-unwind-end, to-to-leq-inf, to-to-leq, to-succ-cons, tl-lem, tl-inf-1, one-inf, length-from, get-infto, get-finto, get-cons-succ, from-succ-cons, from-succ, from-cons-one, cons-eq-inf, cons-eq, append-to-gr-01, append-to-gr, append-split, append-from-gt,
• nat-basic2/pred is used by from-succ-cons,
• nat-basic2/s is used by to-unwind-end-fin, to-to-leq-inf, to-to-leq, to-from-01, length-to, get-infto, get-from-01, get-finto, from-succ,
• nat-basic2/succ is used by to-unwind-end-inf, to-unwind-end-fin, to-unwind-end, to-to-leq-inf, to-to-leq, to-plus-from-fin, to-from-01, to-attach, to-all, tl-lem, tl-inf-1, size-inf-to, length-to, length-from, get-infto, get-from-01, get-finto, from-to-exchange, from-succ, from-from, from-all, elim-hd-tl, contractinf-tl, append-to-le-01, append-to-le, append-to-gr-01, append-to-gr, append-from-le-01, append-from-le, append-from-gt, append-from-addsize-01,
• nat-basic2/z-01 is used by to-empty3, swap-to-from-app, length-from, from-from, append-to-gr, append-from-gt,

Used from specification nat-inf

• nat-inf/num-add is used by toinf-add,
• nat-inf/add-all-inf is used by toinftoinf-append-add, swap-to-from-app, size-append,
• nat-inf/add-all-zero is used by swap-to-from-app, get-from-zero, from-to-exchange,
• nat-inf/add-assoc is used by toinftoinf-append-add, toinfto-append-add, toinf-empty3, to-unwind-end, to-empty3, to-append-add, swap-to-from-app, swap-from-to, size-succ, size-from-less, size-append, nlslen-lslensn-eqlensn, less-size-from, leq-prefix, get-from-zero, get-from, from-to-exchange, from-infto-exchange, from-from, from-append-toinffrom, from-append-tofrom, from-append-add, extensionality-to, contractinf-tl, contractinf-from1, append-notsmallersize2, append-notsmallersize1,
• nat-inf/add-cancel-01 is used by swap-to-from-app, from-append-tofrom,
• nat-inf/add-cancel-num-02 is used by from-to-exchange,
• nat-inf/add-comm is used by toinftoinf-append-add, toinfto-append-add, toinf-empty3, to-unwind-end, to-empty3, to-append-add, swap-to-from-app, swap-to-from, swap-from-to, size-succ, size-from-less, size-append, nlslen-lslensn-eqlensn, less-size-from, leq-prefix, get-from-zero, get-from, from-to-exchange, from-infto-exchange, from-from, from-append-toinffrom, from-append-tofrom, from-append-add, extensionality-to, contractinf-tl, contractinf-from1, append-notsmallersize2, append-notsmallersize1,
• nat-inf/add-fin is used by to-unwind-end, to-empty3, to-append-add, swap-to-from-app, swap-to-from, swap-inf-to-from-app, swap-from-to, size-from-less, size-append, less-size-from, from-to-exchange, from-infto-exchange, from-from, from-append-toinffrom, from-append-tofrom, from-append-add, extensionality-to,
• nat-inf/add-inf2 is used by toinftoinf-append-add, toinf-empty3, swap-to-from-app, size-append, from-infto-exchange, from-append-toinffrom, from-append-add, contractinf-tl, contractinf-from1,
• nat-inf/add-less is used by swap-to-from-app,
• nat-inf/add-less-fin-01 is used by swap-to-from-app, leq-prefix,
• nat-inf/add-ls-cancel-01 is used by to-append-add, swap-to-from-app, 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, append-notsmallersize1,
• nat-inf/addeqinf-cancel is used by swap-to-from-app, less-size-from, from-append-add,
• nat-inf/eq-natinf-to-nat-2-1 is used by swap-to-from-app, from-append-add,
• nat-inf/eq-natinf-to-nat-2-2 is used by to-append-add, size-append,
• nat-inf/inf-less is used by toinftoinf-append-add, toinf-empty2, size-toinf, less-size-from, from-append-toinffrom, from-append-add, append-toinf-ls,
• nat-inf/lele-refl is used by append-from-ge-02,
• nat-inf/lele-trans is used by toinf-to-leq, swap-from-to, from-append-tofrom,
• nat-inf/lels-trans is used by swap-to-from-app, from-append-tofrom, extensionality-to,
• nat-inf/less-fin is used by ton-fromn, toinf-to-ls, toinf-to-leq, to-unwind-end, to-unwind-begin, to-to-leq, to-from-01, to-empty2, to-empty, to-append-add, swap-to-from-app, swap-from-to, size-to-02, size-to, size-succ, size-from-less, lslen-fromnotempty, less-size-from, get-toinf, get-to-02, get-to, get-append-notls, get-append-ls, from-succ, from-append-tofrom, from-append-add, fin-size-from2, fin-size-from, extensionality, elim-fromto, contractinf-tl, contractinf-from1, append-to-ls, append-from-gr-02, append-from-ge-02,
• nat-inf/less-inf1 is used by toinf-to-leq-inf, toinf-to-eq-inf, toinf-empty3, toinf-empty, swap-to-from-app, swap-inf-to-from-app, swap-inf-from-to, swap-from-to, size-succ, size-inf-toinf, size-from-less, get-inftoinf, from-from, from-append-toinffrom, from-append-tofrom, from-append-add, elim-fromto-inf, elim-fromto, append-from-gr-02,
• nat-inf/less-inf2 is used by to-unwind-end, size-succ, less-size-from, get-append-notls, from-succ, from-append-add, extensionality, contractinf-tl, contractinf-from1,
• nat-inf/less-succ-leq is used by to-unwind-end, size-succ,
• nat-inf/ls-le is used by from-append-add, extensionality-to,
• nat-inf/ls-lsadd is used by swap-to-from-app, swap-from-to, size-from-less, from-append-tofrom,
• nat-inf/ls-natinf-to-nat-1-2 is used by to-append-add, swap-to-from-app, swap-from-to, size-from-less, from-from, from-append-tofrom,
• nat-inf/ls-natinf-to-nat-2-1 is used by swap-to-from-app, less-size-from, get-from, from-append-tofrom, from-append-add,
• nat-inf/ls-natinf-to-nat-2-2 is used by swap-to-from-app, swap-from-to, from-append-tofrom, from-append-add,
• nat-inf/ls-natinf-to-nat-3-1 is used by from-append-add,
• 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 toinf-to-ls, get-toinf, extensionality-to,
• nat-inf/prime-add-fin is used by swap-to-from-app, from-append-add,
• nat-inf/sum-zero-fin is used by swap-to-from-app,
• nat-inf/zerols-neqzero is used by zero-len, from-to-exchange,

Used from specification nat-basic1

• nat-basic1/f is used by to-unwind-end-fin, to-unwind-end, to-unwind-begin-fin, to-to-ls, to-to-leq-inf, to-to-leq, to-from-01, to-empty-fin, to-append-add, swap-to-from-app, swap-from-to, lslen-fromnotempty-list, length-to, get-to-02, get-to, get-infto, get-from-01, get-finto, get-append-ls, from-succ, from-append-tofrom, from-append-add, extensionality, append-to-gr-01, append-to-gr, append-from-gt, append-from-gr-01, append-assoc,
• nat-basic1/lf-01 is used by to-to-leq-inf, to-to-leq, swap-to-from-app, swap-from-to, from-append-add, extensionality,
• nat-basic1/ls-02 is used by to-to-leq, to-empty-fin, swap-from-to, lslen-fromnotempty-list, less-size-from, fin-size-from,
• nat-basic1/one-01 is used by tl-lem, hd-lem, get-infto, get-finto, contractinf-tl, contractinf-from1, cons-eq-inf, cons-eq, cons-append,
• nat-basic1/ref-1 is used by ton-fromn-inf, ton-fromn-fin, to-to-leq-inf, to-to-leq, from-append-add, append-to-size-01, append-to-size, append-from-addsize,
• nat-basic1/zero-01 is used by ton-fromn-inf, ton-fromn-fin, to-unwind-end, to-unwind-begin, swap-to-from-app, get-infto, from-append-add, empty-append,

Used from specification list-del

• list-del/extension is used by ton-fromn-inf, ton-fromn-fin, to-empty-fin2, lslen-fromnotempty-list, from-append-add, extensionality, elim-fromto,
• list-del/get-append-grt is used by to-to-leq-inf, to-to-leq, get-infto, get-finto,
• list-del/get-numrec is used by from-succ,
• list-del/get-append-grt is used by get-finto, append-assoc,
• list-del/get-append-grt-02 is used by get-append-notls,
• list-del/get-append-less is used by get-infto, get-finto, get-append-ls, append-assoc,
• list-del/get-butlast is used by to-to-leq-inf, to-to-leq,
• list-del/get-succ is used by to-unwind-end-fin, get-from-01, get-cons-succ,
• list-del/get-zero is used by toone-equal,
• list-del/get-zero-01 is used by to-unwind-end-fin, get-cons-zero, from-succ,
• list-del/one-03 is used by to-to-leq-inf, to-to-leq, tl-lem, hd-lem, get-infto, contractinf-tl, contractinf-from1, cons-eq-inf, cons-eq, cons-append,