[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Used simplifier rules/spec theorems by specification

Used from specification nat

nat/add-01 is used by mk-inj-01, mk-inj, mk-one-01, mk-two, mk-tail, mk-tail-01,
nat/add-num-03 is used by mk-two,
nat/elim-pred-c is used by mk-inj-01, mk-last-02, mk-inj, mk-butlast, blastN-rec-01, blastN-rec, lb, mk-butlast-01, mk-tail, mk-tail-01, mk-rec, blastN-len,
nat/elim-sub is used by mklist-split-intro, blastN-len,
nat/eq-01 is used by butlast-len, blastn-len-0,
nat/eq-02 is used by nodups-butlastn,
nat/eqle-one is used by nodups-butlastn,
nat/le-add is used by postfix-length, prefix-app-02, prefix-app-03,
nat/le-def is used by postfix-split-stronger, lb-01, blastN-all, postfix-length, blastn-len-0, nodups-butlastn,
nat/lels is used by postfix-length, prefix-app-02, prefix-app-03,
nat/lep is used by prefix-intro, blastN-len,
nat/lep-02 is used by blastN-rec-01, nodups-butlastn,
nat/les is used by nodups-butlastn,
nat/lez-01 is used by blastN-rec-01, nodups-butlastn,
nat/ls-01 is used by postfix-split-stronger, lb-01,
nat/not-zero is used by le-leq-one-empty-or-head-equal-last,
nat/pred-03 is used by mk-last-02, mk-last-01, blastN-rec-01, blastN-rec, mk-tail, mk-tail-01, blastN-len,
nat/zero is used by blastN-all,

Used from specification list-dup

list-dup/f is used by rev-dups,
list-dup/rm-ifrec is used by mklist-rmdup-01, mklist-rmdup,
list-dup/app-02 is used by rev-disjoint, rev-disjoint-01,
list-dup/e is used by rev-disjoint, rev-disjoint-01,
list-dup/e-01 is used by nodups-butlastn, rev-dups,
list-dup/first is used by rev-disjoint, rev-disjoint-01,
list-dup/last is used by rev-disjoint,
list-dup/one-01 is used by rev-disjoint, rev-disjoint-01,
list-dup/rec is used by nodups-butlastn, rev-dups,
list-dup/rm-one is used by mklist-rmdup-01,
list-dup/rmdup-e is used by mklist-rmdup,
list-dup/rmdup-n is used by mklist-rmdup,
list-dup/rmdup-y is used by mklist-rmdup,
list-dup/sym is used by rev-disjoint, rev-disjoint-01,

Used from specification list-data

list-data/elim-add is used by postfix-rec-right,
list-data/elim-list-c is used by mk-head, le-leq-one-empty-or-head-equal-last, prefix-rec, prefix-trans, prefix-ex, postfix-tail, blast-head, prefix-rec-01, lin, postfix-tail-01, b-01, mk-tail, l-06, l-03, l-04, l-01, mk-tail-01, last-sizeone, rev-tail, mk-head-01,
list-data/l is used by postfix-split-stronger, le-leq-one-empty-or-head-equal-last, bnotempty, lb-01, blastN-all, postfix-length, nodups-butlastn, prefix-longer-01, lb, prefix-size-eq, prefix-app-02, prefix-app-03, last-sizeone,
list-data/le-one is used by le-leq-one-empty-or-head-equal-last,
list-data/less-nil is used by postfix-is-lessOrEqual,
list-data/size-nil is used by blastN-rec-01, lb-01, mk-len, nodups-butlastn, rev-length, last-sizeone, blastN-len,

Used from specification nat-basic

nat-basic/a is used by mk-empty, mklist-split-intro, postfix-split-stronger, le-leq-one-empty-or-head-equal-last, mklist-last, mk-inj-01, postfix-more, butlast-len, mk-last-02, mk-inj, mk-butlast, mk-one-01, blastN-rec-01, prefix-intro, rev-mklist, lb-01, mk-len, blastN-rec, postfix-length, blastn-len-0, nodups-butlastn, mk-in, prefix-longer-01, blastN-mklist, lb, mk-two, prefix-size-eq, mk-butlast-01, rev-length, mk-tail, mk-one, mk-last, prefix-app-02, prefix-app-03, mk-tail-01, mk-plus, last-sizeone, mklist-rmdup-01, mk-rec, blastN-len, mklist-append,
nat-basic/add-base is used by mk-inj-01, mk-inj, mk-one-01, mk-two, mk-tail, mk-tail-01,
nat-basic/c is used by mk-empty, mklist-split-intro, postfix-split-stronger, le-leq-one-empty-or-head-equal-last, mklist-last, mk-inj-01, postfix-more, butlast-len, mk-last-02, mk-inj, mk-butlast, mk-one-01, blastN-rec-01, prefix-intro, rev-mklist, lb-01, mk-len, blastN-rec, postfix-length, blastn-len-0, nodups-butlastn, mk-in, prefix-longer-01, blastN-mklist, lb, mk-two, prefix-size-eq, mk-butlast-01, rev-length, mk-tail, mk-one, mk-last, prefix-app-02, prefix-app-03, mk-tail-01, mk-plus, last-sizeone, mklist-rmdup-01, mk-rec, blastN-len, mklist-append,
nat-basic/eq-01 is used by mk-inj-01, mk-inj, mk-len, lb, rev-length, blastN-len,
nat-basic/eq-02 is used by postfix-more, prefix-size-eq,
nat-basic/f is used by postfix-length, blastn-len-0, nodups-butlastn, prefix-longer-01,
nat-basic/l-02 is used by blastn-len-0, prefix-longer-01,
nat-basic/less-zero is used by lb-01,
nat-basic/lf-01 is used by nodups-butlastn,
nat-basic/one is used by bnotempty,
nat-basic/one-01 is used by postfix-split-stronger, lb-01, nodups-butlastn,
nat-basic/one-03 is used by mk-one-01, mk-one,
nat-basic/one-06 is used by le-leq-one-empty-or-head-equal-last, last-sizeone,
nat-basic/oz is used by mk-inj-01, postfix-more, mk-last-02, mk-inj, mk-butlast, blastN-rec-01, rev-mklist, postfix-length, nodups-butlastn, mk-in, blastN-mklist, mk-two, mk-butlast-01, mk-tail, mk-one, mk-tail-01, mklist-rmdup-01, mk-rec, blastN-len,
nat-basic/pred is used by mk-butlast, rev-mklist, blastN-mklist, mk-butlast-01, mklist-rmdup-01,
nat-basic/refl-Nat is used by postfix-split-stronger, blastN-rec-01, lb-01, blastN-all, nodups-butlastn, blastN-len,
nat-basic/s-04 is used by postfix-split-stronger, blastN-rec-01, lb-01, postfix-length, nodups-butlastn, blastN-len,
nat-basic/succ is used by mk-empty, mk-inj-01, mk-inj, mk-one-01, rev-mklist, mk-len, nodups-butlastn, mk-in, blastN-mklist, mk-one, mk-last, mk-plus, mklist-rmdup-01, mk-elem,
nat-basic/z-01 is used by mk-inj, mk-butlast, mk-one-01, blastN-mklist, mk-two, mk-butlast-01, mk-tail, prefix-app-03, mk-tail-01, blastN-len,
nat-basic/z-02 is used by mk-plus, blastN-len,

Used from specification list

list/c-06 is used by last-elim,
list/in-def is used by last-ex,
list/lastdiv is used by blastN-rec-01, blastN-len,
list/less-append is used by postfix-is-lessOrEqual,
list/split-first is used by prefix-intro,
list/Last is used by rev-mklist, last, rev-app, rev-length, rev-one, rev-dups,
list/Nil is used by prefix-empty, postfix-split-stronger, last-elim, prefix-ex, prefix-one-01, blast-head, bnotempty, lapp-05, lapp-04, rev-app, b-01, prefix-nil, bl, rev-one, prefix-split-stronger, prefix-app-01, mk-last, prefix-app-02, prefix-app-03, mklist-rmdup,
list/a is used by postfix-in-03, prefix-self, postfix-split, mk-empty, lin-01, mklist-split-intro, prefix-empty, prefix-more, mk-head, prefix-butlast, postfix-split-stronger, le-leq-one-empty-or-head-equal-last, butlast-def, mklist-last, prefix-eq, prefix-rec, mk-inj-01, last-elim, prefix-trans, prefix-ex, postfix-tail, postfix-more, butlast-len, mk-last-02, mk-last-01, mk-inj, prefix-one-01, postfix-same, blast-head, prefix-attach, rev-in, bnotempty, consmklist-last, last-def, bin-02, mk-butlast, mk-one-01, prefix-rec-03, prefix-rec-02, bin-01, prefix-rec-01, blastN-rec-01, prefix-intro, last-01, rev-mklist, last, prefix-one, lapp-03, lapp-02, lapp-01, prefix-same, mk-len, lapp-05, lapp-04, blastN-rec, postfix-length, lin, nodups-butlastn, postfix-app, revert-last, mk-in, rev-app, postfix-empty, prefix-longer-01, blastN-mklist, postfix-rec, last-ex, postfix-tail-01, rev-rev-identity, butlast-last-01, prefix-split, prefix-in-01, lb, prefix-in-02, postfix-more-01, lthree, prefix-app, postfix-one-less, prefix-in-03, mk-two, prefix-size-eq, b-01, b-02, splitlasteq-01, rev-empty, prefix-nil, prefix-longer, prefix-in, mklist-one, rev-length, mk-tail, bapp, postfix-empty-02, postfix-empty-03, mk-one, postfix-empty-01, prefix-app-size-eq, bl, prefix-empty-03, rev-one, postfix-one, rev-disjoint, bc, butlast-eq, postfix-reflexivity, l-06, prefix-split-stronger, l-03, l-04, l-01, l-02, prefix-app-01, mk-last, prefix-app-02, postfix-rec-right, prefix-app-03, prefix-app-04, prefix-app-05, mk-tail-01, postfix-in, mk-plus, last-sizeone, splitlasteq, mklist-rmdup-01, rev-dups, rev-tail, postfix-trans, mk-elem, l-in, mklist-rmdup, blastN-len, postfix-app-06, postfix-app-05, prefix-same-01, postfix-app-04, lapp, bin, prefix-butlast-append, mk-head-01, mklist-append, postfix-app-03, postfix-app-02, postfix-app-01, rev-disjoint-01, blapp,
list/app is used by lin-01, postfix-split-stronger, le-leq-one-empty-or-head-equal-last, last-elim, prefix-attach, consmklist-last, blastN-rec-01, nodups-butlastn, rev-app, postfix-empty, blastN-mklist, b-02, mklist-one, postfix-empty-03, mk-one, bl, rev-one, postfix-one, l-06, l-01, prefix-app-01, mk-last, prefix-app-03, mk-plus, last-sizeone, l-in, bin,
list/app-01 is used by mklist-split-intro, mklist-last, mk-inj-01, prefix-ex, mk-last-02, prefix-attach, mk-butlast, prefix-rec-03, prefix-rec-02, blastN-rec-01, rev-mklist, prefix-same, revert-last, rev-rev-identity, prefix-split, bapp, bl, bc, butlast-eq, mk-last, prefix-app-04, prefix-app-05, mk-plus, mklist-rmdup, mklist-append, postfix-app-03,
list/app-02 is used by mk-empty, prefix-empty, prefix-more, mk-head, postfix-split-stronger, butlast-def, butlast-len, prefix-one-01, blast-head, last-def, prefix-rec-01, lapp-01, lapp-05, postfix-more-01, b-02, rev-empty, prefix-longer, postfix-empty-02, postfix-empty-03, mk-one, postfix-empty-01, prefix-empty-03, mk-tail-01, rev-tail,
list/app-03 is used by postfix-split, postfix-split-stronger, postfix-same, rev-app, bl, postfix-rec-right, postfix-trans, postfix-app-06, postfix-app-05, postfix-app-04, postfix-app-02, postfix-app-01, blapp,
list/app-04 is used by prefix-self, prefix-more, prefix-eq, prefix-size-eq, prefix-longer, l-04,
list/app-05 is used by postfix-more-01, postfix-reflexivity, postfix-rec-right,
list/app-06 is used by butlast-def, last-def, postfix-app-06,
list/app-08 is used by mk-inj, mk-two,
list/c is used by lin-01, mk-head, le-leq-one-empty-or-head-equal-last, prefix-rec, mk-inj-01, last-elim, prefix-trans, prefix-ex, postfix-tail, mk-inj, prefix-one-01, blast-head, rev-in, mk-one-01, prefix-rec-01, lapp-05, lapp-04, postfix-length, lin, nodups-butlastn, rev-app, last-ex, postfix-tail-01, rev-rev-identity, lthree, mk-two, b-01, rev-empty, rev-length, mk-tail, bapp, bl, postfix-one, rev-disjoint, l-06, prefix-split-stronger, l-03, l-04, l-01, prefix-app-01, postfix-rec-right, mk-tail-01, last-sizeone, rev-dups, rev-tail, mk-rec, postfix-is-lessOrEqual, l-in, mklist-rmdup, lapp, bin, mk-head-01, rev-disjoint-01,
list/c-03 is used by last-elim, prefix-one-01, blast-head, mk-one-01, lapp-05, lapp-04, b-01, mk-one, postfix-one, l-06,
list/c-04 is used by last-elim, mk-one-01, blastN-rec-01, mk-one, bl, butlast-eq, mk-last, mklist-rmdup-01, mklist-rmdup, prefix-butlast-append,
list/c-05 is used by last-elim,
list/c-06 is used by mk-head, last-elim, blast-head, prefix-rec-03, lapp-05, lapp-04, mk-tail, prefix-split-stronger, postfix-rec-right, mk-tail-01, rev-tail,
list/e is used by mk-empty, prefix-more, butlast-def, butlast-len, blast-head, prefix-attach, last-def, mk-one-01, prefix-rec-01, prefix-one, lapp-01, lapp-05, postfix-more-01, b-02, rev-empty, prefix-longer, postfix-empty-02, postfix-empty-01, prefix-empty-03, l-06, postfix-rec-right, prefix-butlast-append,
list/e-01 is used by lin-01, mk-head, le-leq-one-empty-or-head-equal-last, prefix-rec, last-elim, prefix-trans, prefix-ex, postfix-tail, prefix-one-01, blast-head, lapp-01, postfix-length, lin, postfix-tail-01, b-01, postfix-one, l-06, prefix-split-stronger, l-04, postfix-rec-right, mk-tail-01, last-sizeone, rev-tail,
list/e-02 is used by prefix-butlast, bin-02, bin-01, blastN-rec-01, postfix-rec, last-ex, blastN-len, prefix-butlast-append,
list/eq-04 is used by postfix-one,
list/first is used by prefix-one,
list/first-01 is used by prefix-ex,
list/in-01 is used by lapp-04, nodups-butlastn, mk-elem,
list/in-06 is used by lin-01, nodups-butlastn, mk-in, prefix-in-03, mklist-rmdup,
list/in-11 is used by bin-01, lapp-04, prefix-in-02,
list/in-12 is used by postfix-in,
list/in-13 is used by postfix-more, lapp-05,
list/in-14 is used by mk-head, mk-inj-01, last-elim, mk-inj, blast-head, lapp-01, lapp-05, lapp-04, mk-tail, postfix-rec-right, mk-tail-01, rev-tail, mk-head-01,
list/in-15 is used by postfix-split-stronger, last-elim, blast-head, blastN-rec-01, lapp-01, lapp-05, lapp-04, butlast-eq, rev-tail, blastN-len, blapp,
list/in-17 is used by postfix-in-03, last-elim, blast-head, rev-in, bin-02, blastN-rec-01, lapp-05, lapp-04, last-ex, prefix-in-01, prefix-in, rev-tail, blastN-len,
list/in-append is used by postfix-in-03, mk-head, postfix-split-stronger, last-elim, blast-head, rev-in, bin-02, blastN-rec-01, lapp-05, lapp-04, last-ex, prefix-in-01, prefix-in, postfix-rec-right, mk-tail-01, rev-tail, mklist-rmdup, blastN-len,
list/in-empty is used by lin-01, last-elim, blast-head, rev-in, bin-02, nodups-butlastn, mk-in, last-ex, mk-elem, l-in,
list/in-rec is used by last-elim, mk-tail,
list/inapp-10 is used by lapp-04,
list/len is used by le-leq-one-empty-or-head-equal-last, postfix-more, butlast-len, blastN-rec-01, prefix-intro, postfix-length, prefix-longer-01, lb, prefix-size-eq, rev-length, prefix-app-02, prefix-app-03, last-sizeone, blastN-len,
list/len-01 is used by prefix-intro, prefix-app-size-eq,
list/len-02 is used by le-leq-one-empty-or-head-equal-last, postfix-more, butlast-len, bnotempty, blastN-rec-01, postfix-length, lb, rev-length, last-sizeone, blastN-len,
list/len-05 is used by mk-len, nodups-butlastn,
list/rest-01 is used by prefix-ex,