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

Used from specification stream

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

Used from specification nat-inf

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

Used from specification list-data

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

Used from specification nat-basic

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

Used from specification mon-lim-filter-count

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

Used from specification list

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

Used from specification list-del

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