[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-inf-basic

nat-inf-basic/notinf-fin is used by remnone-cntequal, rem-reminv-cnt-add, rem-equal-inf, rem-cntleq, lim-unique, lim-infsize-strong, lim-infsize, lim-finsize, lim-evconst, lastocfin-cnteqcntto,
nat-inf-basic/disj is used by remfin-fin2, rem-rec-rev, rem-rec-finsize, rem-equal-inf, lim-infsize-strong, lim-finsize, lim-exists, lim-evconst, lastoc-less-size, lastoc-inf-ant, lastoc-finrec-end, finfilter-notinf, filter-rec-gen, filter-infsize, filter-inf-finsize, cntrem-is-inf, cntinf-tocntsurj, cntfin-eqlen, cnt-rec-end,
nat-inf-basic/elim is used by rem-member2-fin, lim-exists,
nat-inf-basic/fin-inject-embed is used by remnone-cntequal, rem-reminv-cnt-add, rem-rec-rev, rem-member2-fin, rem-cntleq, cntinf-tocntsurj,
nat-inf-basic/inj is used by reminf-infsize-strong, rem-reminv-size-add, rem-reminv-cnt-add, rem-rec-rev, rem-member1, rem-cntequal-fin, mon-bd-or-unbound, lim-evconst, getfilter-sat-p, filter-rec-gen, cntinf-tocntsurj, cntinf-fin-zero, cntinf-fin-weak, cntinf-fin-succ, cntfin-eqlen, cnt-zero, cnt-is-zero, cnt-is-succ,
nat-inf-basic/sel is used by rem-rec-gen, rem-rec-finsize, rem-member2-fin, lim-exists, getfilter-sat-p, cntrem-is-inf, cntinf-tocntsurj,

Used from specification nat

nat/add-01 is used by rem-rec-rev, lastoc-finrec-end-expand, filter-rec-gen,
nat/anti is used by reminf-infsize, rem-rec-rev, rem-member2-fin, rem-equal-fin, lastocfin-cnteqcntto, lastoc-finrec-end, cntinf-tocntsurj, cntinf-fin-weak, cntinf-fin-succ,
nat/cancel-01 is used by cntrem-is-inf,
nat/elim-pred-c is used by rem-shortens, rem-cntequal-fin, mon-bd-or-unbound, getfilter-sat-p, cntfin-eqlen, cnt-is-zero, cnt-is-succ,
nat/elim-sub is used by reminf-infsize-strong, reminf-infsize, reminf-finsize, mon-lem, lim-exists, lastoc-inf-ant, filter-rec-gen, filter-lb, filter-infsize, filter-inf-finsize, filter-evconst, cntrem-is-inf, cntinf-tocntsurj,
nat/eq-01 is used by reminf-infsize-strong, reminf-infsize, reminf-finsize, mon-lem, filter-rec-gen, filter-infsize, filter-inf-finsize, filter-evconst, cntrem-is-inf,
nat/eq-02 is used by lim-exists,
nat/fle is used by lim-exists, lastoc-inf-ant, lastoc-finrec-end, cntrem-is-inf, cnt-is-succ,
nat/fle-01 is used by rem-reminv-cnt-add, lim-exists, lastoc-less-size, cntrem-is-inf, cntinf-tocntsurj,
nat/gr-def is used by lim-exists,
nat/le-add is used by filter-lb,
nat/le-ls-simp is used by reminf-infsize, rem-rec-rev, rem-equal-inf, lim-infsize-strong, lim-finsize, lim-exists, lim-evconst, filter-infsize, cntinf-tocntsurj,
nat/lels is used by remnone-cntequal, reminf-infsize-strong, reminf-infsize, reminf-finsize, rem-reminv-cnt-add, rem-rec-rev, rem-member2-fin, rem-member1, rem-equal-inf, rem-equal-fin, rem-cntequal-fin, lim-unique, lim-infsize-strong, lim-finsize, lim-exists, lim-evconst, lastocfin-cnteqcntto, lastoc-less-size, lastoc-inf-ant, lastoc-finrec-end, getfilter-sat-p, filter-rec-gen, filter-lb, cntrem-is-inf, cntinf-tocntsurj, cntinf-fin-weak, cntinf-fin-succ, cntfin-eqlen, cnt-is-zero, cnt-is-succ,
nat/lels-01 is used by reminf-infsize-strong, rem-shortens, rem-rec-rev-fin, rem-rec-rev, rem-equal-fin, mon-bd-or-unbound, lim-unique, lim-exists, lastoc-inf-ant, filter-rec-gen, filter-lb, cntrem-is-inf, cntinf-tocntsurj,
nat/lels-02 is used by reminf-infsize-strong,
nat/lels-03 is used by reminf-infsize-strong, reminf-infsize, reminf-finsize, rem-reminv-cnt-add, rem-rec-rev, rem-member2-fin, mon-bd-or-unbound, lim-unique, lim-infsize-strong, lim-infsize, lim-exists, lastoc-inf-ant, lastoc-finrec-end, filter-rec-gen, filter-lb, filter-infsize, filter-inf-finsize, filter-evconst, cntrem-is-inf, cntinf-lastocinf, cntinf-infmany, cnt-inf,
nat/lep is used by remnone-cntequal, reminf-infsize, reminf-finsize, rem-reminv-cnt-add, rem-cntleq, mon-lem, lim-exists, filter-rec-gen, filter-infsize, filter-inf-finsize, filter-evconst, cntinf-tocntsurj,
nat/lep-02 is used by lim-exists, lastoc-inf-ant, filter-lb,
nat/ler is used by reminf-infsize-strong, reminf-infsize, rem-rec-rev, rem-member2-fin, rem-member1, rem-equal-fin, mon-lem, lim-unique, lim-infsize-strong, lastoc-finrec-end, getfilter-sat-p, filter-rec-gen, cntinf-tocntsurj, cntfin-eqlen,
nat/let is used by cntinf-tocntsurj,
nat/lez is used by rem-cntequal-fin, cntinf-fin-weak, cnt-is-succ,
nat/lez-01 is used by lim-exists,
nat/ls is used by rem-equal-fin, cntinf-tocntsurj,
nat/ls-01 is used by rem-shortens, rem-rec-rev-fin, rem-equal-fin, mon-bd-or-unbound, lastoc-inf-ant, filter-lb, cntinf-tocntsurj,
nat/ls-le-simp is used by remnone-cntequal, rem-member2-fin, rem-member1, lastoc-inf-ant, cntinf-tocntsurj, cnt-is-zero,
nat/one-02 is used by filter-lb,
nat/pred-03 is used by rem-rec-rev, filter-rec-gen,
nat/prop-07 is used by cntrem-is-inf,
nat/succ-01 is used by reminf-finsize, rem-cntequal-fin, lastoc-rw-inf, lastoc-inf-ant, cntrem-is-inf, cntnotinf-lastocinf, cntinf-infmany, cntinf-fin-weak, cntinf-fin-succ, cntfin-eqlen, cnt-is-zero, cnt-is-succ, cnt-inf,
nat/zero is used by remnone-cntequal, rem-reminv-cnt-add, rem-member2-fin, rem-cntleq, lastoc-finrec-end,
nat/zero-01 is used by reminf-infsize-strong, reminf-infsize, reminf-finsize, filter-rec-gen, filter-infsize, filter-inf-finsize,
nat/zero-02 is used by reminf-finsize, mon-lem, filter-evconst,

Used from specification list-last

list-last/butlast-last is used by filter-lb,
list-last/last-elim is used by rem-shortens, rem-rec-rev-fin, rem-equal-fin, lastoc-finrec-end-expand, filter-lb,
list-last/lb is used by rem-shortens, rem-rec-rev-fin, rem-equal-fin, lastoc-finrec-end-expand,

Used from specification list-data

list-data/l is used by remnone-cntequal, rem-shortens, rem-rec-rev-fin, rem-member2-fin, rem-member2, rem-member1-fin, rem-equal-fin, rem-cntequal-fin, mon-bd-or-unbound, lastoc-less-size, lastoc-inf-ant, lastoc-finrec-end, filter-ub, filter-rec-gen, filter-lb, cntfin-eqlen, cnt-is-zero, cnt-is-succ,
list-data/size-01 is used by remfin-append, rem-shortens, rem-reminv-size-add, rem-one, rem-equal-fin, rem-cntequal-fin, cntfin-eqlen, cnt-leq, cnt-is-zero, cnt-is-succ,

Used from specification stream

stream/append-assoc is used by filterfin-rec-end,
stream/append-finfin is used by filter-lb,
stream/append-from-ge-02 is used by remnone-cntequal, rem-reminv-cnt-add, rem-cntleq,
stream/append-split is used by rem-equal-fin,
stream/append-to-ls is used by remnone-cntequal, rem-reminv-cnt-add, rem-rec-rev, rem-member1, rem-equal-inf, rem-cntleq, lim-unique, getfilter-sat-p, filter-rec-gen,
stream/extensionality is used by rem-rec-rev, rem-member1, rem-equal-fin, mon-bd-or-unbound, lim-infsize, lim-exists, lim-evconst, getfilter-sat-p, filter-rec-gen, filter-infsize,
stream/extensionality-to is used by rem-rec-rev, rem-member1, rem-equal-inf, lim-unique, getfilter-sat-p, filter-rec-gen, filter-inf-finsize-strong,
stream/fin-size-from2 is used by lim-exists, cntinf-tocntsurj,
stream/finlen-tolen is used by remnone-cntequal, rem-reminv-cnt-add, rem-cntleq,
stream/get-append-ls is used by rem-member2-fin, lim-exists, getfilter-sat-p,
stream/get-append-notls is used by rem-member2-fin, cntrem-is-inf,
stream/get-from is used by cntinf-tocntsurj,
stream/one-inf is used by rem-rec-rev, filter-rec-gen,
stream/to-plus-from is used by filter-appendfromto,
stream/to-plus-from-inf is used by remnone-cntequal, rem-reminv-cnt-add, rem-cntleq, cntrem-is-inf,
stream/to-succ-nf is used by rem-rec-rev, filter-rec-gen,
stream/to-unwind-end is used by cntinf-tocntsurj,
stream/to-unwind-end-fin is used by filter-lb,
stream/to-unwind-end-inf is used by reminf-infsize-strong, reminf-infsize, reminf-finsize, mon-remfun, mon-filterfun, filter-rec-gen, filter-infsize, filter-inf-finsize, filter-evconst, cntinf-fin-zero, cntinf-fin-weak, cntinf-fin-succ, cnt-is-zero,
stream/append-assoc is used by to-is-prefix, remnone-cntequal, reminf-infsize-strong, reminf-infsize, reminf-finsize, remfin-append, rem-shortens, rem-reminv-size-add, rem-reminv-cnt-add, rem-rec-rev-fin, rem-rec-rev, rem-rec-gen, rem-rec-finsize, rem-one, rem-member2-fin, rem-member2, rem-member1-fin, rem-member1, rem-equal-inf, rem-equal-fin, rem-cntleq, rem-cntequal-fin, prefixself-equal, prefix-trans, prefix-refl, prefix-notsmallersize, prefix-empty2, prefix-empty1, prefix-antisymm, mon-remfun, mon-filterprefix, mon-filterfun, mon-bd-or-unbound, lim-unique, lim-infsize-strong, lim-infsize, lim-finsize, lim-exists, lim-evconst, lastoc-finrec-end, getfilter-sat-p, finfilter-notinf, filterfin-rec-end, filterfin-append, filter-ub, filter-rec-gen, filter-rec-expand, filter-one, filter-lb, filter-infsize, filter-inf-finsize-strong, filter-inf-finsize, filter-evconst, cntrem-is-inf, cntinf-fin-zero, cntinf-fin-succ, cntfin-rec-end, cntfin-append, cnt-rec-gen, cnt-rec-end, cnt-one, cnt-leq, cnt-is-zero, cnt-is-succ, cnt-appendfromto,
stream/append-cancel-l is used by rem-rec-rev, rem-equal-fin, filter-ub, filter-rec-gen,
stream/append-cancel-l-02 is used by lim-evconst,
stream/append-cut1 is used by remfin-append, rem-rec-rev, rem-rec-gen, rem-rec-finsize, filter-rec-gen, filter-lb,
stream/append-empty is used by reminf-infsize, reminf-finsize, rem-rec-rev-fin, rem-rec-gen, rem-member2-fin, rem-equal-fin, lim-evconst, filter-rec-gen, filter-one, filter-infsize, filter-inf-finsize-strong, filter-inf-finsize, filter-evconst, cnt-is-succ,
stream/append-finfin is used by reminf-infsize-strong, reminf-infsize, reminf-finsize, remfin-append, rem-shortens, rem-reminv-size-add, rem-reminv-cnt-add, rem-rec-rev-fin, rem-rec-rev, rem-member2-fin, rem-member1-fin, rem-equal-fin, rem-cntleq, rem-cntequal-fin, mon-remfun, mon-filterfun, lastoc-finrec-end-expand, getfilter-sat-p, finfilter-notinf, filterfin-rec-end, filterfin-append, filter-ub, filter-rec-gen, filter-lb, filter-infsize, filter-inf-finsize, filter-evconst, cntinf-fin-zero, cntinf-fin-weak, cntinf-fin-succ, cntfin-eqlen, cnt-leq, cnt-is-zero, cnt-is-succ,
stream/append-inf is used by mon-filterprefix, lim-evconst, cnt-rec-end,
stream/append-to-size is used by filter-lb,
stream/appendend-equal is used by reminf-infsize, prefixself-equal, prefix-refl, prefix-antisymm, mon-bd-or-unbound, lim-infsize-strong, lim-exists, filter-infsize,
stream/cons-append is used by rem-rec-rev, filter-ub, filter-rec-gen, filter-rec-expand,
stream/cons-empty is used by rem-member2, filter-rec-expand,
stream/contractinf-from1 is used by rem-member2,
stream/elim-fromto is used by to-is-prefix,
stream/elim-hd-tl is used by filter-rec-expand,
stream/empty is used by reminf-infsize-strong, remfin-append, rem-shortens, rem-reminv-size-add, rem-reminv-cnt-add, rem-rec-rev-fin, rem-rec-rev, rem-one, rem-member1-fin, rem-equal-fin, rem-cntleq, rem-cntequal-fin, lastoc-finrec-end-expand, getfilter-sat-p, finfilter-notinf, filterfin-rec-end, filterfin-append, filter-ub, filter-rec-gen, filter-one, cntinf-fin-zero, cntinf-fin-weak, cntinf-fin-succ, cntfin-eqlen, cnt-one, cnt-leq, cnt-is-zero, cnt-is-succ,
stream/empty-append is used by remfin-append, rem-reminv-cnt-add, rem-rec-rev-fin, rem-rec-rev, rem-one, rem-member2, rem-member1-fin, rem-cntleq, rem-cntequal-fin, prefixself-equal, prefix-empty1, getfilter-sat-p, filterfin-rec-end, filterfin-append, filter-ub, filter-rec-gen, filter-rec-expand, cnt-rec-gen, cnt-one,
stream/eq-stream-to-list-2-1 is used by rem-equal-fin,
stream/fin-empty is used by reminf-infsize, rem-rec-rev, rem-member2-fin, rem-equal-fin, mon-bd-or-unbound, lastoc-finrec-end-expand, filter-inf-finsize, cntinf-fin-zero, cnt-is-zero,
stream/fin-to is used by remto-fin, filter-appendfromto, cntto-notinf, cntinf-tocntsurj,
stream/finlen-tolen is used by lim-unique, lim-infsize, filter-inf-finsize-strong, filter-inf-finsize,
stream/from-inf is used by lim-exists,
stream/from-zero is used by remnone-cntequal, rem-reminv-cnt-add, rem-cntleq,
stream/get-append-ls is used by rem-member2-fin, lim-exists, cntrem-is-inf,
stream/get-append-notls is used by rem-member2-fin, lim-exists, getfilter-sat-p,
stream/get-append2-fin is used by lastoc-finrec-end,
stream/get-cons-succ is used by rem-member2, rem-member1-fin,
stream/get-cons-zero is used by rem-member2, rem-member1-fin,
stream/get-finto is used by cnt-is-succ,
stream/get-from is used by lim-exists,
stream/get-from-inf is used by remnone-cntequal, rem-reminv-cnt-add, rem-member2, rem-cntleq, lim-exists, cntrem-is-inf,
stream/get-infto is used by remnone-cntequal, rem-member1, lim-exists, cnt-is-zero,
stream/get-to is used by rem-member1, getfilter-sat-p, cntinf-tocntsurj,
stream/inf-size-to is used by rem-equal-inf, lim-exists, cntrem-is-inf,
stream/length-to is used by cnt-is-succ,
stream/less-size-from is used by cntinf-tocntsurj,
stream/notfin-sizeinf is used by rem-rec-gen, lim-exists, lim-evconst,
stream/sel-fin is used by remnone-cntequal, rem-member2-fin, rem-member2, rem-member1, lim-exists, lastoc-less-size, lastoc-inf-ant, lastoc-finrec-end, getfilter-sat-p, cntfin-eqlen, cnt-is-zero, cnt-is-succ,
stream/sel-inf is used by remnone-cntequal, rem-reminv-cnt-add, rem-member2, rem-member1, rem-cntleq, lim-exists, lastoc-inf-ant, filter-infsize, cntrem-is-inf, cntfin-eqlen, cnt-is-zero, cnt-is-succ,
stream/size-append is used by to-is-prefix, remnone-cntequal, reminf-infsize-strong, rem-shortens, rem-reminv-size-add, rem-reminv-cnt-add, rem-rec-rev, rem-member2-fin, rem-member2, rem-member1-fin, rem-member1, rem-equal-inf, rem-equal-fin, rem-cntleq, prefix-notsmallersize, mon-bd-or-unbound, lim-unique, lim-infsize-strong, lim-infsize, lim-finsize, lim-exists, lim-evconst, lastoc-finrec-end, getfilter-sat-p, finfilter-notinf, filter-ub, filter-rec-gen, filter-infsize, filter-inf-finsize-strong, cntrem-is-inf, cntinf-fin-succ, cntfin-rec-end, cntfin-append, cnt-rec-gen, cnt-leq, cnt-appendfromto,
stream/size-empty is used by reminf-infsize-strong, rem-shortens, rem-reminv-size-add, rem-rec-rev, rem-member2, rem-member1-fin, lastoc-empty, getfilter-sat-p, finfilter-notinf, filter-ub, filter-rec-gen, cntinf-fin-zero, cntinf-fin-succ, cntfin-rec-end, cnt-zero, cnt-rec-gen, cnt-leq, cnt-is-zero,
stream/size-empty-equiv is used by reminf-infsize-strong, rem-rec-rev, rem-member2-fin, rem-equal-inf, lim-unique, lim-infsize-strong, lim-exists, lim-evconst, filter-inf-finsize-strong, cntinf-fin-zero, cnt-is-zero,
stream/size-fin is used by remnone-cntequal, reminf-infsize-strong, remfin-fin2, remfin-fin, rem-shortens, rem-reminv-size-add, rem-rec-rev, rem-rec-gen, rem-member2-fin, rem-member2, rem-member1-fin, rem-member1, rem-equal-inf, rem-equal-fin, mon-bd-or-unbound, lim-finsize, lim-exists, lim-evconst, lastoc-less-size, lastoc-inf-ant, lastoc-finrec-end, getfilter-sat-p, finfilter-notinf, filter-ub, filter-rec-gen, filter-lb, filter-infsize, cntrem-is-inf, cntinf-fin-succ, cntfin-rec-end, cntfin-eqlen, cnt-rec-gen, cnt-rec-end, cnt-leq, cnt-is-zero, cnt-is-succ,
stream/size-inf is used by remnone-cntequal, remfin-fin, rem-shortens, rem-reminv-size-add, rem-reminv-cnt-add, rem-member2, rem-member1, rem-equal-inf, rem-cntleq, mon-bd-or-unbound, lim-finsize, lim-exists, lastoc-less-size, lastoc-inf-ant, filter-ub, filter-rec-gen, filter-lb, filter-infsize, filter-inf-finsize, cntrem-is-inf, cntfin-eqlen, cnt-rec-end, cnt-leq, cnt-is-zero, cnt-is-succ,
stream/size-inf-to is used by remnone-cntequal, reminf-infsize-strong, reminf-infsize, reminf-finsize, rem-reminv-cnt-add, rem-member1, rem-equal-inf, rem-cntleq, mon-remfun, cntrem-is-inf, cnt-is-zero,
stream/size-succ is used by reminf-infsize-strong, rem-member2, rem-member1-fin, rem-member1, mon-bd-or-unbound, lim-unique, lim-infsize-strong, lim-finsize, lim-evconst, lastoc-less-succsize, getfilter-sat-p, filter-ub,
stream/size-to is used by rem-rec-rev, rem-member1, rem-equal-inf, lim-unique, lim-evconst, getfilter-sat-p, filter-rec-gen, cntinf-tocntsurj,
stream/stream-empty is used by rem-rec-rev, prefixself-equal, prefix-empty2, filter-rec-gen, cntinf-fin-zero, cnt-is-zero,
stream/to-empty4 is used by cntinf-fin-zero, cnt-is-zero,
stream/to-fin is used by rem-equal-inf, filter-ub, filter-lb, cnt-is-succ,
stream/to-inf is used by remnone-cntequal, rem-equal-inf, lim-exists, filter-ub, filter-lb, filter-inf-finsize, cnt-is-succ,
stream/to-plus-from-simp is used by lim-exists,
stream/to-succ-cons is used by rem-rec-rev, filter-ub, filter-rec-gen,
stream/to-succ-cons-l-lem is used by filter-ub, cnt-is-succ,
stream/to-to-eq is used by rem-rec-rev, rem-member1, rem-equal-inf, lim-unique, getfilter-sat-p, filter-rec-gen,
stream/to-to-leq is used by cntinf-tocntsurj,
stream/to-to-leq-inf is used by rem-equal-inf,
stream/to-to-ls is used by cntinf-tocntsurj,
stream/to-zero is used by rem-rec-rev, filter-ub, filter-rec-gen, cntinf-tocntsurj, cntinf-fin-zero, cnt-is-zero,
stream/to-zero-l is used by cnt-is-succ,
stream/to-zero-nf is used by reminf-infsize-strong, rem-rec-rev, filter-rec-gen, cntinf-fin-zero, cntinf-fin-weak, cntinf-fin-succ,
stream/toinf-fin is used by mon-filtertoinf, mon-cnttoinf,
stream/toinf-inf is used by mon-cnttoinf,
stream/zero-len is used by rem-member2, lim-exists,

Used from specification list

list/lastdiv-rew is used by rem-member2-fin,
list/a is used by reminf-infsize-strong, reminf-infsize, reminf-finsize, remfin-append, rem-shortens, rem-reminv-size-add, rem-reminv-cnt-add, rem-rec-rev-fin, rem-rec-rev, rem-member2-fin, rem-member1-fin, rem-equal-fin, rem-cntleq, rem-cntequal-fin, mon-remfun, mon-filterfun, lastoc-finrec-end-expand, lastoc-finrec-end, getfilter-sat-p, finfilter-notinf, filterfin-rec-end, filterfin-append, filter-ub, filter-rec-gen, filter-lb, filter-infsize, filter-inf-finsize, filter-evconst, cntinf-fin-zero, cntinf-fin-weak, cntinf-fin-succ, cntfin-eqlen, cnt-leq, cnt-is-zero, cnt-is-succ,
list/app-04 is used by rem-equal-fin,
list/c is used by remfin-append, rem-reminv-size-add, rem-reminv-cnt-add, rem-rec-rev-fin, rem-rec-rev, rem-member1-fin, rem-cntleq, rem-cntequal-fin, getfilter-sat-p, finfilter-notinf, filterfin-rec-end, filterfin-append, filter-ub, filter-rec-gen, cntfin-eqlen, cnt-leq, cnt-is-zero, cnt-is-succ,
list/e is used by reminf-infsize, rem-rec-rev, rem-member2-fin, rem-equal-fin, filter-inf-finsize, cntinf-fin-zero, cnt-is-zero,
list/e-02 is used by rem-shortens, rem-rec-rev-fin, rem-equal-fin, filter-lb,
list/len is used by rem-shortens, rem-member2-fin, rem-equal-fin, lastoc-finrec-end-expand, filter-lb,
list/len-02 is used by reminf-infsize-strong, rem-shortens, rem-reminv-size-add, rem-rec-rev, rem-member2-fin, rem-member2, rem-member1-fin, rem-equal-fin, rem-cntequal-fin, lastoc-finrec-end-expand, lastoc-finrec-end, getfilter-sat-p, finfilter-notinf, filter-ub, filter-rec-gen, filter-lb, filter-infsize, cntinf-fin-succ, cntfin-rec-end, cntfin-eqlen, cnt-rec-gen, cnt-leq, cnt-is-zero, cnt-is-succ,
list/len-05 is used by remfin-append, rem-reminv-size-add, rem-rec-rev-fin, rem-member1-fin, rem-cntequal-fin, filter-ub, cntfin-eqlen, cnt-leq, cnt-is-zero, cnt-is-succ,

Used from specification stream-basic

stream-basic/ex is used by remfin-fin2,
stream-basic/sel-embed-fin is used by remto-fin, rem-rec-gen, filter-appendfromto,
stream-basic/elim is used by cntto-notinf,
stream-basic/inj-01 is used by remfin-fin,
stream-basic/sel-02 is used by rem-rec-gen,
stream-basic/stream-fin-forward is used by rem-rec-gen, lim-exists, lim-evconst,
stream-basic/stream-inf-forward is used by remfin-fin, lim-exists, lim-evconst,
stream-basic/test-01 is used by remfin-fin,
stream-basic/test-02 is used by lim-exists,

Used from specification nat-basic2

nat-basic2/a is used by remnone-cntequal, reminf-infsize-strong, reminf-infsize, reminf-finsize, remfin-append, rem-shortens, rem-reminv-size-add, rem-reminv-cnt-add, rem-rec-rev-fin, rem-rec-rev, rem-member2-fin, rem-member2, rem-member1-fin, rem-member1, rem-equal-inf, rem-equal-fin, rem-cntleq, rem-cntequal-fin, mon-lem, mon-bd-or-unbound, lim-unique, lim-infsize-strong, lim-finsize, lim-exists, lim-evconst, lastocfin-cnteqcntto, lastoc-rw-inf, lastoc-inf-ant, lastoc-finrec-end-expand, getfilter-sat-p, filter-ub, filter-rec-gen, filter-lb, filter-infsize, filter-inf-finsize, filter-evconst, cntrem-is-inf, cntnotinf-lastocinf, cntinf-tocntsurj, cntinf-infmany, cntinf-fin-weak, cntinf-fin-succ, cntfin-eqlen, cnt-leq, cnt-is-zero, cnt-is-succ, cnt-inf,
nat-basic2/add-base is used by reminf-infsize, reminf-finsize, remfin-append, rem-rec-rev, lastoc-finrec-end-expand, filter-rec-gen, filter-infsize, filter-inf-finsize,
nat-basic2/c is used by remnone-cntequal, reminf-infsize-strong, reminf-infsize, reminf-finsize, remfin-append, rem-shortens, rem-reminv-size-add, rem-reminv-cnt-add, rem-rec-rev-fin, rem-rec-rev, rem-member2-fin, rem-member2, rem-member1-fin, rem-member1, rem-equal-inf, rem-equal-fin, rem-cntleq, rem-cntequal-fin, mon-lem, mon-bd-or-unbound, lim-unique, lim-infsize-strong, lim-finsize, lim-exists, lim-evconst, lastocfin-cnteqcntto, lastoc-rw-inf, lastoc-inf-ant, lastoc-finrec-end-expand, getfilter-sat-p, filter-ub, filter-rec-gen, filter-lb, filter-infsize, filter-inf-finsize, filter-evconst, cntrem-is-inf, cntnotinf-lastocinf, cntinf-tocntsurj, cntinf-infmany, cntinf-fin-weak, cntinf-fin-succ, cntfin-eqlen, cnt-leq, cnt-is-zero, cnt-is-succ, cnt-inf,
nat-basic2/eq is used by cntinf-fin-weak, cntinf-fin-succ,
nat-basic2/eq-01 is used by rem-shortens, filter-lb,
nat-basic2/l is used by rem-rec-rev, rem-equal-fin, lastoc-inf-ant, filter-rec-gen, cnt-is-succ,
nat-basic2/l-01 is used by reminf-infsize-strong, reminf-infsize, reminf-finsize, lastoc-inf-ant, filter-rec-gen, filter-lb, filter-infsize, filter-inf-finsize, cntrem-is-inf, cntinf-tocntsurj,
nat-basic2/l-02 is used by reminf-infsize-strong, reminf-infsize, reminf-finsize, rem-shortens, lim-exists, filter-rec-gen, filter-infsize, filter-inf-finsize, cntrem-is-inf, cntinf-tocntsurj, cnt-leq,
nat-basic2/l-05 is used by rem-equal-inf,
nat-basic2/nls-fst is used by lastocfin-cnteqcntto,
nat-basic2/oz is used by reminf-infsize, rem-rec-rev, rem-cntequal-fin, mon-bd-or-unbound, getfilter-sat-p, filter-rec-gen, filter-infsize, filter-inf-finsize, cntfin-eqlen, cnt-is-zero, cnt-is-succ,
nat-basic2/s is used by reminf-infsize-strong, reminf-infsize, reminf-finsize, rem-shortens, rem-reminv-size-add, rem-rec-rev-fin, rem-member2-fin, rem-member1-fin, rem-member1, rem-equal-inf, rem-equal-fin, rem-cntequal-fin, mon-bd-or-unbound, lim-exists, getfilter-sat-p, filter-ub, filter-rec-gen, filter-lb, filter-infsize, filter-inf-finsize, cntrem-is-inf, cntfin-eqlen, cnt-is-zero, cnt-is-succ,
nat-basic2/succ is used by reminf-infsize-strong, reminf-infsize, reminf-finsize, remfin-append, rem-reminv-size-add, rem-reminv-cnt-add, rem-rec-rev-fin, rem-rec-rev, rem-member2, rem-member1-fin, rem-cntequal-fin, mon-lem, mon-bd-or-unbound, lim-infsize-strong, lim-exists, lastocfin-cnteqcntto, lastoc-less-size, lastoc-inf-ant, lastoc-finrec-end, filter-ub, filter-rec-gen, filter-infsize, filter-inf-finsize, filter-evconst, cntrem-is-inf, cntinf-tocntsurj, cntinf-fin-zero, cntinf-fin-weak, cntinf-fin-succ, cntfin-eqlen, cnt-leq, cnt-is-zero, cnt-is-succ,
nat-basic2/z is used by reminf-infsize-strong,
nat-basic2/z-01 is used by reminf-infsize, filter-infsize, filter-inf-finsize,

Used from specification nat-inf

nat-inf/add-comm is used by filter-infsize,
nat-inf/add-all-inf is used by rem-rec-rev, mon-bd-or-unbound, lim-infsize, lim-finsize, lim-exists, filter-rec-gen, filter-infsize,
nat-inf/add-all-zero is used by reminf-infsize-strong, rem-shortens, rem-reminv-size-add, rem-reminv-cnt-add, rem-rec-rev, rem-member2, rem-member1-fin, rem-member1, rem-equal-fin, rem-cntleq, rem-cntequal-fin, lastocfin-cnteqcntto, getfilter-sat-p, finfilter-notinf, filter-ub, filter-rec-gen, cntrem-is-inf, cntinf-tocntsurj, cntinf-fin-weak, cntinf-fin-succ, cntfin-rec-end, cntfin-eqlen, cnt-rec-gen, cnt-rec-end, cnt-one, cnt-leq, cnt-is-zero, cnt-is-succ,
nat-inf/add-assoc is used by remnone-cntequal, reminf-infsize-strong, rem-shortens, rem-reminv-size-add, rem-reminv-cnt-add, rem-rec-rev, rem-member2-fin, rem-member2, rem-member1-fin, rem-member1, rem-equal-inf, rem-equal-fin, rem-cntleq, rem-cntequal-fin, prefix-notsmallersize, mon-cntto, mon-bd-or-unbound, lim-unique, lim-infsize-strong, lim-infsize, lim-finsize, lim-exists, lim-evconst, lastocfin-cnteqcntto, lastoc-less-succsize, lastoc-finrec-end, getfilter-sat-p, finfilter-notinf, filter-ub, filter-rec-gen, filter-infsize, filter-inf-finsize-strong, filter-inf-finsize, cntrem-is-inf, cntinf-tocntsurj, cntinf-fin-weak, cntinf-fin-succ, cntfin-rec-end, cntfin-eqlen, cnt-rec-gen, cnt-rec-end, cnt-one, cnt-leq, cnt-is-zero, cnt-is-succ,
nat-inf/add-cancel-01 is used by reminf-infsize-strong, rem-reminv-cnt-add, rem-rec-rev, rem-cntequal-fin, lim-unique, filter-rec-gen,
nat-inf/add-cancel-02 is used by filter-infsize, cntinf-tocntsurj,
nat-inf/add-cancel-03 is used by remnone-cntequal, rem-equal-inf, lim-unique, lim-evconst, filter-inf-finsize-strong, cntinf-tocntsurj,
nat-inf/add-cancel-num-01 is used by cnt-is-succ,
nat-inf/add-cancel-num-02 is used by rem-rec-rev, filter-infsize, cnt-is-succ,
nat-inf/add-cancel-num-03 is used by rem-reminv-size-add, rem-rec-rev, rem-member1, rem-equal-fin, lastocfin-cnteqcntto, getfilter-sat-p, filter-rec-gen, cntinf-tocntsurj, cntinf-fin-weak, cntinf-fin-succ, cntfin-rec-end, cntfin-eqlen, cnt-rec-gen, cnt-is-succ,
nat-inf/add-cancel-num-04 is used by cnt-is-succ,
nat-inf/add-comm is used by remnone-cntequal, reminf-infsize-strong, rem-shortens, rem-reminv-size-add, rem-reminv-cnt-add, rem-rec-rev, rem-member2-fin, rem-member2, rem-member1-fin, rem-member1, rem-equal-inf, rem-equal-fin, rem-cntleq, rem-cntequal-fin, prefix-notsmallersize, mon-cntto, mon-bd-or-unbound, lim-unique, lim-infsize-strong, lim-infsize, lim-finsize, lim-exists, lim-evconst, lastocfin-cnteqcntto, lastoc-less-succsize, lastoc-finrec-end, getfilter-sat-p, finfilter-notinf, filter-ub, filter-rec-gen, filter-infsize, filter-inf-finsize-strong, filter-inf-finsize, cntrem-is-inf, cntinf-tocntsurj, cntinf-fin-weak, cntinf-fin-succ, cntfin-rec-end, cntfin-eqlen, cnt-rec-gen, cnt-rec-end, cnt-one, cnt-leq, cnt-is-zero, cnt-is-succ,
nat-inf/add-fin is used by remnone-cntequal, reminf-infsize-strong, rem-shortens, rem-reminv-size-add, rem-rec-rev, rem-member2, rem-member1-fin, rem-member1, rem-equal-inf, mon-bd-or-unbound, lim-unique, lim-infsize-strong, lim-finsize, lim-exists, lim-evconst, lastocfin-cnteqcntto, getfilter-sat-p, filter-ub, filter-rec-gen, filter-inf-finsize, cntrem-is-inf, cntinf-tocntsurj, cntinf-fin-weak, cntinf-fin-succ, cntfin-eqlen, cnt-leq, cnt-is-succ,
nat-inf/add-inf-01 is used by rem-reminv-size-add, rem-reminv-cnt-add, cntrem-is-inf,
nat-inf/add-inf2 is used by rem-equal-inf, lastoc-less-succsize, filter-rec-gen, cntrem-is-inf,
nat-inf/add-less is used by rem-rec-rev, rem-member2-fin, rem-cntleq, mon-bd-or-unbound, lim-exists,
nat-inf/add-less-fin-01 is used by lim-unique, lim-infsize-strong, lim-exists, lim-evconst,
nat-inf/add-ls-cancel-01 is used by lim-exists,
nat-inf/add-ls-cancel-num-04 is used by rem-shortens, rem-rec-rev, rem-member1, rem-cntleq, getfilter-sat-p, cntrem-is-inf, cnt-leq,
nat-inf/add-not-less is used by remnone-cntequal, reminf-infsize-strong, rem-reminv-cnt-add, rem-rec-rev, rem-member1, rem-cntleq, prefix-notsmallersize, mon-cntto, lim-unique, lim-infsize-strong, lim-finsize, getfilter-sat-p, filter-rec-gen,
nat-inf/addeqinf-cancel is used by lim-exists, lastoc-finrec-end, finfilter-notinf, filter-inf-finsize, cntrem-is-inf,
nat-inf/eq-natinf-to-nat-2-1 is used by rem-equal-inf, lim-exists, cntinf-fin-weak, cntinf-fin-succ,
nat-inf/eqsucc-ls is used by rem-cntequal-fin, cntinf-tocntsurj,
nat-inf/inf-inseq-reduce is used by lim-exists, cntrem-is-inf, cntfin-eqlen,
nat-inf/inf-less is used by lastoc-less-succsize, filter-inf-finsize,
nat-inf/lele-refl is used by lim-infsize-strong,
nat-inf/lele-trans is used by mon-bd-or-unbound,
nat-inf/lels-trans is used by rem-shortens, rem-cntleq, lim-exists, getfilter-sat-p,
nat-inf/less-fin is used by remnone-cntequal, reminf-infsize-strong, rem-rec-rev, rem-member2-fin, rem-member2, rem-member1-fin, rem-member1, rem-equal-inf, rem-equal-fin, lim-unique, lim-infsize-strong, lim-infsize, lim-finsize, lim-exists, lastoc-less-size, lastoc-inf-ant, lastoc-finrec-end, lastoc-empty, getfilter-sat-p, filter-ub, filter-rec-gen, filter-lb, filter-inf-finsize-strong, filter-inf-finsize, cntrem-is-inf, cntinf-tocntsurj, cntfin-eqlen, cnt-is-zero, cnt-is-succ,
nat-inf/less-inf1 is used by rem-shortens, rem-rec-rev, rem-equal-inf, rem-cntleq, mon-filtertoinf, lim-unique, lim-infsize, lim-exists, lastoc-less-size, filter-rec-gen, cntinf-tocntsurj, cnt-leq,
nat-inf/less-inf2 is used by remnone-cntequal, remfin-fin, rem-reminv-cnt-add, rem-member2, rem-member1, rem-cntleq, mon-bd-or-unbound, lim-exists, lastocfin-cnteqcntto, lastoc-rw-inf, lastoc-less-size, lastoc-inf-ant, filter-ub, filter-lb, filter-inf-finsize, cntrem-is-inf, cntnotinf-lastocinf, cntinf-tocntsurj, cntinf-lastocinf, cntfin-eqlen, cnt-is-zero, cnt-is-succ,
nat-inf/less-succ-leq is used by rem-member2-fin, rem-member2, rem-member1-fin, rem-member1, rem-equal-fin, lim-evconst, lastoc-finrec-end, getfilter-sat-p, filter-ub, cnt-is-succ,
nat-inf/ls-irref is used by remnone-cntequal, rem-reminv-cnt-add, rem-cntleq, mon-cnttoinf,
nat-inf/ls-le is used by to-is-prefix, lim-exists, filter-ub,
nat-inf/ls-lsadd is used by rem-member2-fin,
nat-inf/ls-natinf-to-nat-1-2 is used by reminf-infsize-strong,
nat-inf/ls-natinf-to-nat-2-1 is used by rem-shortens, lim-exists, filter-rec-gen, cntrem-is-inf, cntinf-tocntsurj, cnt-leq,
nat-inf/ls-notlssucc is used by lim-exists,
nat-inf/ls-one is used by rem-rec-rev, cntinf-fin-zero, cnt-is-zero,
nat-inf/lsle-trans is used by rem-shortens, rem-cntleq, cnt-leq,
nat-inf/not-less-zero is used by rem-member1-fin, mon-bd-or-unbound, lim-infsize-strong, getfilter-sat-p, filter-ub,
nat-inf/num-add is used by rem-reminv-size-add, rem-reminv-cnt-add, cnt-is-succ,
nat-inf/prime-add-fin is used by cntrem-is-inf,
nat-inf/sum-zero is used by lim-evconst,
nat-inf/sum-zero-fin is used by remnone-cntequal, rem-rec-rev, rem-equal-inf, lim-unique, lastocfin-cnteqcntto, filter-rec-gen, cntinf-fin-weak, cntinf-fin-succ, cnt-is-zero, cnt-is-succ,
nat-inf/zerols-neqzero is used by rem-shortens, rem-rec-rev, rem-cntleq, cntinf-fin-zero, cnt-leq, cnt-is-zero,

Used from specification nat-basic1

nat-basic1/f is used by remnone-cntequal, reminf-infsize-strong, reminf-infsize, reminf-finsize, rem-reminv-size-add, rem-reminv-cnt-add, rem-rec-rev, rem-member2-fin, rem-member2, rem-member1-fin, rem-member1, rem-equal-inf, rem-equal-fin, rem-cntequal-fin, mon-bd-or-unbound, lim-unique, lim-infsize-strong, lim-infsize, lim-finsize, lim-exists, lim-evconst, lastocfin-cnteqcntto, lastoc-rw-inf, lastoc-less-size, lastoc-inf-ant, lastoc-finrec-end, filter-ub, filter-rec-gen, filter-lb, filter-infsize, filter-inf-finsize, filter-evconst, cntrem-is-inf, cntnotinf-lastocinf, cntinf-tocntsurj, cntinf-lastocinf, cntinf-infmany, cntinf-fin-weak, cntinf-fin-succ, cntfin-eqlen, cnt-is-zero, cnt-is-succ, cnt-inf,
nat-basic1/lf is used by rem-reminv-cnt-add, mon-bd-or-unbound, lastoc-less-size, lastoc-inf-ant, lastoc-finrec-end, cntrem-is-inf, cnt-is-succ,
nat-basic1/lf-01 is used by lastoc-inf-ant, lastoc-finrec-end, filter-lb,
nat-basic1/lf-02 is used by rem-equal-inf, filter-lb,
nat-basic1/ls-02 is used by reminf-infsize-strong, rem-reminv-size-add, rem-equal-fin, lim-exists, lastoc-less-size, lastoc-inf-ant, lastoc-finrec-end, filter-lb, cntinf-tocntsurj,
nat-basic1/one is used by lastoc-inf-ant,
nat-basic1/one-01 is used by rem-shortens, rem-rec-rev-fin, rem-equal-fin, rem-cntequal-fin, mon-bd-or-unbound, getfilter-sat-p, filter-lb, cntfin-eqlen, cnt-is-zero, cnt-is-succ,
nat-basic1/ref-1 is used by reminf-infsize-strong, rem-shortens, rem-reminv-size-add, rem-rec-rev-fin, rem-rec-rev, rem-member2-fin, rem-member1, rem-equal-inf, rem-equal-fin, mon-bd-or-unbound, lim-unique, lim-infsize-strong, lim-infsize, lim-finsize, lim-exists, lastoc-finrec-end, getfilter-sat-p, filter-rec-gen, filter-inf-finsize-strong, filter-inf-finsize, cntfin-eqlen, cnt-is-succ,
nat-basic1/trans-1 is used by rem-reminv-cnt-add, mon-bd-or-unbound, lastoc-less-size, lastoc-inf-ant, cntrem-is-inf, cnt-is-succ,
nat-basic1/zero is used by rem-rec-rev, filter-rec-gen, cnt-is-succ,
nat-basic1/zero-01 is used by rem-member1-fin, rem-equal-fin, rem-cntequal-fin, lastoc-empty, getfilter-sat-p, filter-ub, cntfin-eqlen, cnt-is-zero, cnt-is-succ,

Used from specification list-del

list-del/get-append-grt is used by rem-member2-fin, cnt-is-succ,
list-del/get-append-less is used by rem-cntequal-fin, lastoc-finrec-end, cntfin-eqlen, cnt-is-zero, cnt-is-succ,
list-del/get-append-grt is used by rem-cntequal-fin, lastoc-finrec-end, cntfin-eqlen, cnt-is-zero, cnt-is-succ,
list-del/get-append-less is used by cnt-is-succ,
list-del/get-butlast is used by rem-member2-fin, lastoc-finrec-end,
list-del/get-last is used by rem-member2-fin,
list-del/get-last-03 is used by lastoc-finrec-end,
list-del/get-succ is used by rem-member1-fin, rem-cntequal-fin, cntfin-eqlen, cnt-is-zero, cnt-is-succ,
list-del/get-zero-01 is used by rem-member1-fin, rem-cntequal-fin, cntfin-eqlen, cnt-is-zero, cnt-is-succ,
list-del/one-03 is used by rem-member2-fin, rem-cntequal-fin, lastoc-finrec-end, getfilter-sat-p, cntfin-eqlen, cnt-is-zero, cnt-is-succ,