[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/fin-inject-embed is used by leninv-less, inv-get-lslen,
nat-inf-basic/notinf-fin is used by stutf-maxinf-is-fin, leninv-zero, leninv-succ, leninv-inf, inv-ls-succ, inv-inverts, inv-get-lslen,
nat-inf-basic/disj is used by rem-preserves-monls, monlsinf-notsmall, monls-to, monls-mon-implies-monls, monls-from, mininv-stays-if-not-taken, mininv-inverts-weak, mininv-inverts-inner-succ, mininv-inverts-inner, min-stutters, min-skolemf, maxinf-skolemf, maxinf-inf, maxinf-fin, lsleninv-1, leq-leninv, leninv-succ, leninv-invlast, inv-ls-succ, inv-inverts-leq, inv-inverts-last, inv-inverts, inv-get-lslen, inv-get-inverse-succ-inf, inv-get-inverse-succ, inv-get-inverse-last, inv-get-inverse-between, inv-get-inverse, eq-leninv,
nat-inf-basic/elim is used by mininv-stays-if-not-taken, mininv-inverts-weak, mininv-inverts-inner-succ, mininv-inverts-inner, min-stutters, maxinf-inf, maxinf-fin, lsleninv-1, leq-leninv, inv-ls-succ, inv-inverts-leq, inv-inverts-last, inv-inverts, inv-get-lslen, inv-get-inverse-succ, inv-get-inverse-last, inv-get-inverse-between, inv-get-inverse, eq-leninv,
nat-inf-basic/fin-inject-embed is used by leninv-is-len-inv, inv-inverts-leq, inv-get-inverse-last,
nat-inf-basic/inj is used by maxinf-fin, inv-inverts,
nat-inf-basic/sel is used by rem-preserves-monls, monls-mon-implies-monls, mininv-inverts-inner-succ, min-stutters, min-skolemf, maxinf-skolemf, leninv-succ, leninv-invlast, inv-ls-succ, inv-inverts,

Used from specification nat

nat/le-def is used by inv-ls-notleq,
nat/add-01 is used by mininv-inverts-inner-succ, mininv-inverts, min-stutters, min-skolemf, leninv-zero, leninv-succ, leninv-invlast-inv, leninv-invlast, leninv-inf,
nat/add-num-03 is used by monls-mon-implies-monls, inv-ls-succ,
nat/anti is used by monls-exists-maxleq, mininv-stays-if-not-taken, mininv-inverts-inner-succ, mininv-inverts-inner, min-stutters, min-skolemf, leninv-succ, inv-inverts, inv-get-inverse-last, inv-get-inverse-between,
nat/cancel-01 is used by rem-preserves-monls, monls-mon-implies-monls, leninv-succ,
nat/elim-pred-c is used by mininv-stays-if-not-taken, mininv-inverts-inner-succ, mininv-inverts-inner, min-stutters, maxinf-skolemf, lsleninv-1, leq-leninv, leninv-succ, leninv-inf, inv-ls-succ, inv-inverts-leq, inv-inverts, inv-get-lslen, inv-get-inverse-succ, inv-get-inverse-last, inv-get-inverse-between, inv-get-inverse, eq-leninv,
nat/elim-sub is used by monls-ls, monle-leq, maxinf-skolemf, leninv-succ,
nat/eq is used by mininv-stays-if-not-taken, maxinf-skolemf, leninv-succ, leninv-inf, inv-ls-succ, inv-inverts-leq, inv-get-inverse-succ, inv-get-inverse-between, inv-get-inverse, eq-leninv,
nat/eq-01 is used by monls-ls, monle-leq, leninv-succ,
nat/eqle-one is used by stutf-alltakenmax, stutf-alltaken, maxinf-skolemf, lsleninv-1, less-leninv, leninv-succ, leninv-inf-strong, leninv-inf, inv-ls-succ, inv-get-inverse-succ, inv-get-inverse-between, inv-get-inverse, eq-leninv,
nat/fle is used by stutf-slowincrease, stutf-notbig, stutf-maxinf-is-fin, stutf-alltaken, monls-to, monls-mon-implies-monls, monls-exists-maxls, monls-exists-maxleq, monls-append1, monle-leq, maxinf-skolemf, lsleninv-1, leq-leninv, leninv-succ, inv-ls-succ, inv-inverts-leq, inv-get-inverse-last, inv-get-inverse-between, eq-leninv,
nat/fle-01 is used by stutf-maxinf-is-fin, monls-ls, monls-exists-maxls, monls-exists-maxleq, mininv-stays-if-not-taken, min-stutters, lsleninv-1, leninv-succ, inv-ls-succ, inv-get-lslen, inv-get-inverse-between,
nat/l-num-06 is used by leninv-inf, inv-ls-succ,
nat/le-add is used by monls-mon-implies-monls, maxinf-skolemf, inv-inverts-last,
nat/le-ls-simp is used by stutf-slowincrease, stutf-maxinf-is-fin, stutf-alltaken, rem-preserves-monls, monlsinf-notsmall, monls-notsmall, monls-ls, monls-exists-maxleq, monls-append2, mininv-stays-if-not-taken, mininv-inverts-inner-succ, mininv-inverts-inner, min-stutters, min-skolemf, leninv-succ, inv-ls-succ, inv-inverts-leq, inv-inverts, inv-get-lslen, inv-get-inverse-succ, inv-get-inverse-last, inv-get-inverse-between, inv-get-inverse,
nat/le-one is used by stutf-alltaken, monls-notsmall, maxinf-skolemf, inv-ls-succ,
nat/lels is used by stutf-slowincrease, stutf-notbig, stutf-maxinf-is-fin, stutf-invmonls, rem-preserves-monls, monlsinf-notsmall, monls-to, monls-notsmall, monls-mon-implies-monls, monls-ls, monls-from, monls-exists-maxleq, monls-append2, monls-append1, monle-leq, mininv-stays-if-not-taken, mininv-inverts-inner-succ, mininv-inverts-inner, mininv-inverts, min-stutters, min-skolemf, maxinf-skolemf, lsleninv-1, less-leninv, leq-leninv, leninv-succ, leninv-inf-strong, leninv-inf, inv-ls-succ, inv-ls-notleq, inv-inverts-leq, inv-inverts-last, inv-inverts, inv-get-lslen, inv-get-inverse-succ, inv-get-inverse-last, inv-get-inverse-between, inv-get-inverse, eq-leninv,
nat/lels-01 is used by stutf-slowincrease, stutf-monle, stutf-alltaken, monls-ls, monls-exists-maxls, monle-leq, mininv-inverts-weak2, min-skolemf, maxinf-skolemf, lsleninv-1, less-leninv, leninv-succ, leninv-inf, inv-ls-succ, inv-get-inverse-between,
nat/lels-02 is used by stutf-maxinf-is-fin, monls-exists-maxleq, mininv-stays-if-not-taken, mininv-inverts-inner-succ, mininv-inverts-inner, mininv-inverts, min-stutters, min-skolemf, leninv-succ, inv-get-inverse-between, eq-leninv,
nat/lels-03 is used by stutf-maxinf-is-fin, monls-ls, monls-exists-maxleq, mininv-stays-if-not-taken, min-stutters, min-skolemf, lsleninv-1, leninv-succ, inv-ls-succ, inv-inverts-leq, inv-inverts, inv-get-inverse-succ, inv-get-inverse-between, inv-get-inverse, eq-leninv,
nat/lep is used by monls-exists-maxls, monls-exists-maxleq, monle-leq, maxinf-skolemf, leninv-succ, inv-ls-succ, inv-get-inverse-between,
nat/lep-02 is used by stutf-alltaken, inv-get-inverse-between,
nat/leprf is used by maxinf-skolemf,
nat/ler is used by stutf-alltaken, monls-exists-maxleq, mininv-stays-if-not-taken, mininv-inverts-inner-succ, mininv-inverts-inner, min-stutters, min-skolemf, maxinf-skolemf, less-leninv, leninv-succ, inv-ls-succ, inv-get-inverse-last, inv-get-inverse-between, eq-leninv,
nat/les is used by stutf-alltaken, min-stutters, maxinf-skolemf, leninv-inf-strong, inv-ls-succ, inv-get-inverse-between,
nat/let is used by mininv-stays-if-not-taken, min-stutters, lsleninv-1, inv-ls-succ, inv-inverts-leq, inv-get-inverse-between,
nat/lez is used by monls-exists-maxleq, min-zero, min-skolemf, maxinf-skolemf, lsleninv-1, less-leninv, inv-inverts-last,
nat/lez-01 is used by stutf-alltaken, min-zero, eq-leninv,
nat/ls-01 is used by maxinf-skolemf,
nat/ls-02 is used by maxinf-skolemf,
nat/ls-03 is used by inv-get-inverse-between,
nat/ls-add-not-01 is used by stutf-notbig,
nat/ls-le-simp is used by stutf-maxinf-is-fin, monls-to, monls-from, monls-exists-maxls, monle-leq, mininv-stays-if-not-taken, mininv-inverts-weak, min-skolemf, maxinf-skolemf, lsleninv-1, less-leninv, leninv-succ, leninv-inf, inv-ls-succ, inv-inverts-leq, inv-get-lslen, inv-get-inverse-succ, inv-get-inverse-between, inv-get-inverse, eq-leninv,
nat/not-zero is used by inv-ls-succ,
nat/pred-03 is used by inv-get-inverse-between,
nat/succ-01 is used by stutf-alltakenmax, monls-exists-maxleq, mininv-stays-if-not-taken, mininv-inverts-inner-succ, mininv-inverts, min-stutters, min-skolemf, maxinf-skolemf, lsleninv-1, less-leninv, leninv-succ, leninv-inf, inv-ls-succ, inv-inverts-leq, inv-inverts, inv-get-lslen, inv-get-inverse-succ, inv-get-inverse-between, inv-get-inverse, eq-leninv,
nat/zero is used by rem-preserves-monls,
nat/zero-01 is used by monls-ls, leninv-succ,
nat/zero-02 is used by monle-leq,

Used from specification mon-lim-filter-count

mon-lim-filter-count/natstream/lim-def is used by monls-mon-implies-monls,
mon-lim-filter-count/natstream/mon-remfun is used by rem-preserves-monls,
mon-lim-filter-count/natstream/prefix-def is used by monls-mon-implies-monls,
mon-lim-filter-count/natstream/rem-inf is used by rem-preserves-monls,
mon-lim-filter-count/natstream/rem-member1-fin is used by rem-preserves-monls,
mon-lim-filter-count/natstream/rem-base is used by rem-preserves-monls,
mon-lim-filter-count/natstream/rem-rec is used by rem-preserves-monls,

Used from specification list-data

list-data/natstream/l is used by rem-preserves-monls, monls-append2, monls-append1,

Used from specification stream

stream/natstream/extensionality is used by leninv-zero, eq-leninv,
stream/natstream/get-append-ls is used by rem-preserves-monls, monls-mon-implies-monls,
stream/natstream/get-infto is used by inv-inverts-last,
stream/natstream/append-assoc is used by rem-preserves-monls, monls-mon-implies-monls, monls-append2, monls-append1,
stream/natstream/append-empty is used by rem-preserves-monls,
stream/natstream/append-finfin is used by rem-preserves-monls,
stream/natstream/empty is used by rem-preserves-monls,
stream/natstream/get-append-ls is used by rem-preserves-monls,
stream/natstream/get-append-notls is used by rem-preserves-monls, monls-mon-implies-monls,
stream/natstream/get-append2-fin is used by rem-preserves-monls, monls-append2, monls-append1,
stream/natstream/get-from-inf is used by monls-from,
stream/natstream/get-infto is used by monls-to, inv-ls-succ, inv-inverts-leq, inv-inverts-last, inv-inverts, inv-get-lslen, inv-get-inverse-succ, inv-get-inverse-last, inv-get-inverse-between, inv-get-inverse,
stream/natstream/get-to is used by monls-mon-implies-monls,
stream/natstream/inf-size-to is used by monls-to, leninv-is-len-inv,
stream/natstream/sel-fin is used by rem-preserves-monls, monls-to, monls-append2, monls-append1, inv-ls-succ, inv-inverts-leq, inv-inverts-last, inv-inverts, inv-get-lslen, inv-get-inverse-succ, inv-get-inverse-last, inv-get-inverse-between, inv-get-inverse,
stream/natstream/sel-inf is used by monlsinf-notsmall, monls-to, monls-from, lsleninv-1, less-leninv, leq-leninv, leninv-zero, inv-ls-succ, inv-inverts-leq, inv-inverts-last, inv-inverts, inv-get-lslen, inv-get-inverse-succ, inv-get-inverse-between, inv-get-inverse, eq-leninv,
stream/natstream/size-append is used by rem-preserves-monls, monls-mon-implies-monls, monls-append2, monls-append1,
stream/natstream/size-empty is used by mininv-inverts-weak, mininv-inverts-inner-succ, mininv-inverts-inner, min-empty,
stream/natstream/size-empty-equiv is used by monls-notsmall, lsleninv-1, leninv-zero, leninv-succ, leninv-inf, inv-inverts-leq, inv-get-lslen, inv-get-inverse-last, inv-get-inverse-between, inv-get-inverse,
stream/natstream/size-fin is used by rem-preserves-monls, monls-append2, monls-append1,
stream/natstream/size-inf is used by monlsinf-notsmall, monls-to, monls-from, lsleninv-1, leninv-zero, leninv-is-len-inv, inv-inverts-last, eq-leninv,
stream/natstream/size-to is used by monls-mon-implies-monls,
stream/natstream/to-inf is used by leninv-is-len-inv, inv-ls-succ, inv-inverts-leq, inv-inverts-last, inv-inverts, inv-get-lslen, inv-get-inverse-succ, inv-get-inverse-last, inv-get-inverse-between, inv-get-inverse,
stream/natstream/to-zero-nf is used by inv-inverts-last, inv-inverts,
stream/natstream/zero-len is used by stutf-alltaken, monls-exists-maxleq, min-zero, min-skolemf,

Used from specification list

list/natstream/lastdiv-rew is used by rem-preserves-monls,
list/natstream/a is used by rem-preserves-monls, monls-append2, monls-append1,
list/natstream/len is used by rem-preserves-monls,
list/natstream/len-02 is used by rem-preserves-monls,

Used from specification nat-basic2

nat-basic2/a is used by succlessleninv-invsize, stutf-slowincrease, stutf-notbig, stutf-monle, stutf-maxinf-is-fin, stutf-invmonls, stutf-alltakenmax, stutf-alltaken, rem-preserves-monls, monlsinf-notsmall, monls-to, monls-notsmall, monls-mon-implies-monls, monls-ls, monls-from, monls-exists-maxls, monls-exists-maxleq, monls-append2, monls-append1, monle-leq, mininv-stays-if-not-taken, mininv-inverts-inner-succ, mininv-inverts-inner, mininv-inverts, min-stutters, min-skolemf, maxinf-skolemf, lsleninv-2, lsleninv-1, less-leninv, leq-leninv, leninv-zero, leninv-succ, leninv-invlast-inv, leninv-invlast, leninv-inf-strong, leninv-inf, inv-ls-succ, inv-inverts-leq, inv-inverts-last, inv-inverts, inv-get-lslen, inv-get-inverse-succ, inv-get-inverse-last, inv-get-inverse-between, inv-get-inverse, eq-leninv,
nat-basic2/add-base is used by stutf-slowincrease, mininv-inverts-inner-succ, mininv-inverts, min-skolemf, leninv-zero, leninv-succ, leninv-invlast, leninv-inf,
nat-basic2/c is used by succlessleninv-invsize, stutf-slowincrease, stutf-notbig, stutf-monle, stutf-maxinf-is-fin, stutf-invmonls, stutf-alltakenmax, stutf-alltaken, rem-preserves-monls, monlsinf-notsmall, monls-to, monls-notsmall, monls-mon-implies-monls, monls-ls, monls-from, monls-exists-maxls, monls-exists-maxleq, monls-append2, monls-append1, monle-leq, mininv-stays-if-not-taken, mininv-inverts-inner-succ, mininv-inverts-inner, mininv-inverts, min-stutters, min-skolemf, maxinf-skolemf, lsleninv-2, lsleninv-1, less-leninv, leq-leninv, leninv-zero, leninv-succ, leninv-invlast-inv, leninv-invlast, leninv-inf-strong, leninv-inf, inv-ls-succ, inv-inverts-leq, inv-inverts-last, inv-inverts, inv-get-lslen, inv-get-inverse-succ, inv-get-inverse-last, inv-get-inverse-between, inv-get-inverse, eq-leninv,
nat-basic2/eq is used by stutf-slowincrease, stutf-notbig, stutf-alltakenmax, stutf-alltaken, mininv-inverts-inner-succ, mininv-inverts-inner, mininv-inverts, less-leninv, leninv-succ, leninv-inf, inv-inverts, inv-get-inverse-succ, inv-get-inverse-last, inv-get-inverse-between,
nat-basic2/eq-01 is used by mininv-inverts-inner-succ, min-stutters, leninv-succ, inv-inverts,
nat-basic2/eqs is used by less-leninv, inv-inverts, inv-get-inverse-between,
nat-basic2/l is used by succlessleninv-invsize, stutf-slowincrease, monls-mon-implies-monls, monls-append2, mininv-inverts-inner-succ, min-stutters, leninv-succ, leninv-inf, inv-ls-succ, inv-inverts-leq, inv-inverts, inv-get-inverse-succ, inv-get-inverse-last, inv-get-inverse-between,
nat-basic2/l-01 is used by monls-mon-implies-monls, monls-ls, leninv-succ,
nat-basic2/l-02 is used by stutf-slowincrease, stutf-notbig, stutf-monle, stutf-maxinf-is-fin, stutf-alltakenmax, stutf-alltaken, monls-to, monls-notsmall, monls-ls, monls-exists-maxls, monle-leq, leq-leninv, leninv-succ, inv-ls-succ, inv-inverts, inv-get-inverse-last, inv-get-inverse-between, eq-leninv,
nat-basic2/l-06 is used by min-stutters,
nat-basic2/l-08 is used by monls-append1,
nat-basic2/neq-01 is used by stutf-alltakenmax, mininv-inverts-inner-succ, min-stutters, inv-get-inverse-between,
nat-basic2/nls-fst is used by monls-append1, inv-inverts-leq, inv-inverts, inv-get-inverse-succ, inv-get-inverse-last, inv-get-inverse-between,
nat-basic2/one-03 is used by leninv-succ,
nat-basic2/oz is used by succlessleninv-invsize, stutf-alltakenmax, stutf-alltaken, mininv-stays-if-not-taken, mininv-inverts-inner-succ, mininv-inverts-inner, min-stutters, maxinf-skolemf, lsleninv-1, leq-leninv, leninv-zero, leninv-succ, leninv-inf-strong, leninv-inf, inv-ls-succ, inv-inverts-leq, inv-inverts, inv-get-lslen, inv-get-inverse-succ, inv-get-inverse-last, inv-get-inverse-between, inv-get-inverse, eq-leninv,
nat-basic2/s is used by succlessleninv-invsize, stutf-maxinf-is-fin, stutf-alltakenmax, stutf-alltaken, rem-preserves-monls, monls-ls, monls-exists-maxleq, mininv-stays-if-not-taken, mininv-inverts-inner-succ, mininv-inverts-inner, mininv-inverts, min-stutters, min-skolemf, lsleninv-2, lsleninv-1, less-leninv, leq-leninv, leninv-zero, leninv-succ, leninv-inf-strong, leninv-inf, inv-ls-succ, inv-inverts-leq, inv-inverts-last, inv-inverts, inv-get-lslen, inv-get-inverse-succ, inv-get-inverse-last, inv-get-inverse-between, inv-get-inverse, eq-leninv,
nat-basic2/succ is used by succlessleninv-invsize, stutf-slowincrease, stutf-notbig, stutf-maxinf-is-fin, stutf-alltakenmax, stutf-alltaken, monls-notsmall, monls-mon-implies-monls, monls-ls, monls-exists-maxls, monls-exists-maxleq, monle-leq, mininv-inverts-inner-succ, min-skolemf, lsleninv-1, less-leninv, leq-leninv, leninv-zero, leninv-succ, leninv-inf-strong, leninv-inf, inv-ls-succ, inv-inverts-leq, inv-inverts-last, inv-inverts, inv-get-lslen, inv-get-inverse-succ, inv-get-inverse-between, inv-get-inverse, eq-leninv,
nat-basic2/succ-03 is used by mininv-inverts-inner-succ, min-stutters, inv-ls-succ, inv-get-inverse-between,
nat-basic2/z is used by min-stutters, leninv-invlast-inv,
nat-basic2/z-01 is used by maxinf-skolemf,

Used from specification nat-inf

nat-inf/add-comm is used by inv-get-inverse-last,
nat-inf/add-fin is used by leninv-succ, eq-leninv,
nat-inf/lele-refl is used by not-ls-leninv,
nat-inf/add-all-zero is used by rem-preserves-monls, monls-ls, inv-get-inverse-between,
nat-inf/add-assoc is used by succlessleninv-invsize, stutf-slowincrease, stutf-notbig, stutf-invmonls, stutf-alltakenmax, stutf-alltaken, rem-preserves-monls, monlsinf-notsmall, monls-to, monls-notsmall, monls-mon-implies-monls, monls-ls, monls-from, monls-exists-maxls, monls-exists-maxleq, monls-append2, monls-append1, monle-leq, mininv-inverts-inner-succ, mininv-inverts-inner, min-stutters, min-skolemf, min-empty, lsleninv-2, lsleninv-1, leq-leninv, leninv-succ, leninv-invlast-inv, leninv-invlast, leninv-inf, inv-ls-succ, inv-inverts-last, inv-inverts, inv-get-lslen, inv-get-inverse-succ-inf, inv-get-inverse-succ, inv-get-inverse-last, inv-get-inverse-between, inv-get-inverse, eq-leninv,
nat-inf/add-comm is used by succlessleninv-invsize, stutf-slowincrease, stutf-notbig, stutf-invmonls, stutf-alltakenmax, stutf-alltaken, rem-preserves-monls, monlsinf-notsmall, monls-to, monls-notsmall, monls-mon-implies-monls, monls-ls, monls-from, monls-exists-maxls, monls-exists-maxleq, monls-append2, monls-append1, monle-leq, mininv-inverts-inner-succ, mininv-inverts-inner, min-stutters, min-skolemf, min-empty, lsleninv-2, lsleninv-1, leq-leninv, leninv-succ, leninv-invlast-inv, leninv-invlast, leninv-inf, inv-ls-succ, inv-inverts-last, inv-inverts, inv-get-lslen, inv-get-inverse-succ-inf, inv-get-inverse-succ, inv-get-inverse-last, inv-get-inverse-between, inv-get-inverse, eq-leninv,
nat-inf/add-fin is used by succlessleninv-invsize, stutf-slowincrease, stutf-notbig, stutf-alltakenmax, stutf-alltaken, rem-preserves-monls, monlsinf-notsmall, monls-notsmall, monls-mon-implies-monls, monls-ls, monls-exists-maxls, monls-exists-maxleq, monle-leq, mininv-stays-if-not-taken, mininv-inverts-inner-succ, mininv-inverts-inner, mininv-inverts, min-stutters, min-skolemf, lsleninv-1, less-leninv, leq-leninv, leninv-zero, leninv-succ, leninv-inf, inv-inverts-leq, inv-inverts-last, inv-inverts, inv-get-lslen, inv-get-inverse-succ, inv-get-inverse-last, inv-get-inverse-between, inv-get-inverse, eq-leninv,
nat-inf/add-inf-02 is used by inv-ls-succ, inv-inverts-last, inv-get-inverse-last,
nat-inf/add-ls-cancel-01 is used by stutf-slowincrease, monls-ls, monle-leq,
nat-inf/add-ls-cancel-num-02 is used by monls-notsmall,
nat-inf/add-ls-cancel-num-04 is used by rem-preserves-monls, monls-mon-implies-monls, inv-get-inverse-between,
nat-inf/add-not-less is used by monls-mon-implies-monls,
nat-inf/addeqinf-cancel is used by monlsinf-notsmall, monls-to, monls-from, leninv-succ, inv-inverts, inv-get-inverse-succ-inf, inv-get-inverse-succ, inv-get-inverse-between,
nat-inf/eq-natinf-to-nat-2-1 is used by inv-get-inverse-last,
nat-inf/eqls-succ is used by rem-preserves-monls, mininv-inverts-inner-succ, inv-get-inverse-succ, inv-get-inverse-between,
nat-inf/eqsucc-ls is used by min-stutters,
nat-inf/inf-inseq-reduce is used by succlessleninv-invsize, rem-preserves-monls, mininv-inverts-inner-succ, mininv-inverts-inner, min-skolemf, lsleninv-2, lsleninv-1, leq-leninv, leninv-succ, leninv-inf, inv-inverts-last, inv-inverts, inv-get-lslen, inv-get-inverse-succ, inv-get-inverse-between, inv-get-inverse, eq-leninv,
nat-inf/inf-less is used by monlsinf-notsmall, monls-to, monls-from, leninv-succ, inv-ls-succ, inv-inverts, inv-get-inverse-succ-inf, inv-get-inverse-succ, inv-get-inverse-last, inv-get-inverse-between,
nat-inf/lels-trans is used by monls-mon-implies-monls, leninv-less,
nat-inf/leq-notgradd is used by inv-get-inverse-between,
nat-inf/less-fin is used by stutf-maxinf-is-fin, rem-preserves-monls, not-ls-leninv, monls-mon-implies-monls, monls-exists-maxleq, mininv-stays-if-not-taken, mininv-inverts-weak, mininv-inverts-inner-succ, mininv-inverts-inner, min-stutters, maxinf-skolemf, maxinf-inf, maxinf-fin, lsleninv-1, less-leninv, leq-leninv, leninv-zero, leninv-succ, inv-ls-succ, inv-inverts-leq, inv-inverts, inv-get-lslen, inv-get-inverse-succ, inv-get-inverse-last, inv-get-inverse-between, inv-get-inverse, eq-leninv,
nat-inf/less-inf1 is used by monls-mon-implies-monls, leninv-less,
nat-inf/less-inf2 is used by stutf-maxinf-is-fin, lsleninv-1, less-leninv, leq-leninv, leninv-zero, leninv-succ, leninv-inf, inv-ls-succ, inv-inverts-leq, inv-inverts, inv-get-lslen, inv-get-inverse-succ, inv-get-inverse-last, inv-get-inverse-between, inv-get-inverse, eq-leninv,
nat-inf/less-notgeqinf is used by min-empty,
nat-inf/less-succ-leq is used by rem-preserves-monls, monls-mon-implies-monls, monls-exists-maxleq, inv-get-inverse-between,
nat-inf/ls-natinf-to-nat-1-2 is used by monls-mon-implies-monls, min-stutters,
nat-inf/ls-natinf-to-nat-2-1 is used by succlessleninv-invsize, stutf-slowincrease, stutf-notbig, stutf-alltakenmax, stutf-alltaken, monls-to, monls-notsmall, monls-mon-implies-monls, monls-ls, monls-exists-maxls, monls-append2, monls-append1, monle-leq, inv-ls-succ, inv-inverts, inv-get-inverse-succ, inv-get-inverse-between,
nat-inf/ls-natinf-to-nat-2-2 is used by monls-append2, monls-append1,
nat-inf/ls-natinf-to-nat-3-1 is used by inv-get-inverse-last,
nat-inf/ls-notlssucc is used by rem-preserves-monls, mininv-inverts-inner-succ, min-stutters, min-skolemf,
nat-inf/ls-trans is used by monls-mon-implies-monls,
nat-inf/lsle-trans is used by stutf-slowincrease, stutf-notbig, stutf-maxinf-is-fin, stutf-alltakenmax, stutf-alltaken, monls-notsmall, monls-ls, monls-exists-maxls, monls-exists-maxleq, monle-leq, leninv-less, inv-ls-succ, inv-inverts,
nat-inf/num-add is used by monls-notsmall, inv-get-inverse-between,
nat-inf/onels-neqzero is used by monls-notsmall,
nat-inf/prime-add-fin is used by rem-preserves-monls, monls-mon-implies-monls, mininv-inverts-inner-succ, min-stutters, min-skolemf, leninv-invlast,
nat-inf/rem-seln-on-add is used by leninv-invlast-inv,
nat-inf/sum-notinf is used by succlessleninv-invsize, mininv-inverts-inner-succ, min-stutters, min-skolemf, leninv-invlast-inv, leninv-invlast, inv-get-inverse-last,
nat-inf/zerols-neqzero is used by mininv-inverts-weak,

Used from specification nat-basic1

nat-basic1/f is used by succlessleninv-invsize, stutf-slowincrease, stutf-notbig, stutf-monle, stutf-maxinf-is-fin, stutf-alltakenmax, stutf-alltaken, rem-preserves-monls, monls-to, monls-notsmall, monls-mon-implies-monls, monls-ls, monls-exists-maxls, monls-exists-maxleq, monls-append2, monls-append1, monle-leq, mon-eq, mininv-stays-if-not-taken, mininv-inverts-weak, mininv-inverts-inner-succ, mininv-inverts-inner, mininv-inverts, min-stutters, min-skolemf, maxinf-skolemf, maxinf-inf, maxinf-fin, lsleninv-3, lsleninv-2, lsleninv-1, less-leninv, leq-leninv, leninv-succ, leninv-inf-strong, leninv-inf, inv-ls-succ, inv-inverts-leq, inv-inverts-last, inv-inverts, inv-get-lslen, inv-get-inverse-succ, inv-get-inverse-last, inv-get-inverse-between, inv-get-inverse, eq-leninv,
nat-basic1/lf is used by stutf-maxinf-is-fin, monls-mon-implies-monls, monls-exists-maxleq, mininv-inverts-inner-succ, maxinf-skolemf, lsleninv-1, leninv-succ, inv-ls-succ, inv-inverts-leq, inv-get-inverse-succ, inv-get-inverse-between, inv-get-inverse, eq-leninv,
nat-basic1/lf-01 is used by stutf-slowincrease, stutf-notbig, stutf-monle, stutf-alltakenmax, stutf-alltaken, monls-notsmall, monls-exists-maxleq, mon-eq, mininv-stays-if-not-taken, mininv-inverts-inner-succ, mininv-inverts-inner, min-stutters, maxinf-skolemf, lsleninv-1, less-leninv, leq-leninv, leninv-succ, leninv-inf-strong, inv-ls-succ, inv-get-inverse-between, eq-leninv,
nat-basic1/lf-02 is used by stutf-monle, stutf-maxinf-is-fin, stutf-alltakenmax, stutf-alltaken, monls-notsmall, monls-exists-maxleq, mon-eq, mininv-stays-if-not-taken, maxinf-skolemf, lsleninv-1, less-leninv, leq-leninv, leninv-succ, leninv-inf-strong, inv-ls-succ, inv-inverts-leq, inv-inverts-last, inv-get-inverse-succ, inv-get-inverse-between, inv-get-inverse, eq-leninv,
nat-basic1/ls-02 is used by stutf-maxinf-is-fin, stutf-alltakenmax, monls-ls, mon-eq, mininv-stays-if-not-taken, mininv-inverts-inner-succ, mininv-inverts-inner, mininv-inverts, min-stutters, min-skolemf, less-leninv, leninv-succ, inv-ls-succ, inv-inverts-leq, inv-inverts, inv-get-inverse-succ, inv-get-inverse-between,
nat-basic1/neq-01 is used by mon-eq, maxinf-fin, leninv-succ, inv-inverts-last, inv-inverts,
nat-basic1/one is used by leninv-succ,
nat-basic1/one-01 is used by inv-ls-succ, inv-get-inverse-between,
nat-basic1/ref-1 is used by succlessleninv-invsize, stutf-slowincrease, stutf-monle, stutf-maxinf-is-fin, stutf-alltakenmax, stutf-alltaken, rem-preserves-monls, not-ls-leninv, monls-mon-implies-monls, monls-exists-maxleq, monls-append1, monle-leq, mon-eq, mininv-inverts-weak, mininv-inverts-inner-succ, mininv-inverts-inner, mininv-inverts, min-stutters, min-skolemf, lsleninv-2, lsleninv-1, less-leninv, leq-leninv, leninv-zero, leninv-succ, leninv-inf-strong, leninv-inf, inv-ls-succ, inv-inverts-leq, inv-inverts-last, inv-inverts, inv-get-lslen, inv-get-inverse-succ, inv-get-inverse-last, inv-get-inverse-between, inv-get-inverse, eq-leninv,
nat-basic1/trans-1 is used by stutf-maxinf-is-fin, monls-mon-implies-monls, monls-exists-maxleq, mininv-inverts-inner-succ, maxinf-skolemf, lsleninv-1, leninv-succ, inv-ls-succ, inv-inverts-leq, inv-get-inverse-succ, inv-get-inverse-between, inv-get-inverse, eq-leninv,
nat-basic1/zero is used by monls-notsmall, lsleninv-1, leq-leninv, leninv-zero, leninv-inf-strong, inv-ls-succ, inv-get-inverse-succ, inv-get-inverse,
nat-basic1/zero-01 is used by mininv-inverts-inner-succ, mininv-inverts-inner, min-zero, min-skolemf, lsleninv-1, inv-inverts-leq, inv-get-inverse-last, inv-get-inverse,

Used from specification list-del

list-del/natstream/get-append-less is used by monls-append1,
list-del/natstream/get-append-grt is used by monls-append1,
list-del/natstream/get-append-grt-02 is used by monls-append2,
list-del/natstream/get-butlast is used by rem-preserves-monls,
list-del/natstream/get-last-03 is used by rem-preserves-monls,
list-del/natstream/one-03 is used by rem-preserves-monls,