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

nat-basic/a is used by postfix-split-stronger, mk-in, postfix-length, rev-length, blastn-len-0, blastN-rec, mk-empty, prefix-app-02, mk-one-01, nodups-butlastn, mk-one, mk-tail-01, mk-rec, mk-tail, mklist-append, butlast-len, lb, postfix-more, mklist-last, prefix-intro, le-leq-one-empty-or-head-equal-last, mk-butlast-01, prefix-app-03, blastN-rec-01, rev-mklist, mklist-split-intro, lb-01, mklist-rmdup-01, mk-last-02, mk-last, prefix-size-eq, prefix-longer-01, mk-two, blastN-mklist, last-sizeone, mk-inj-01, blastN-len, mk-butlast, mk-plus, mk-inj, mk-len,
nat-basic/add-base is used by mk-one-01, mk-tail-01, mk-tail, mk-two, mk-inj-01, mk-inj,
nat-basic/c is used by postfix-split-stronger, mk-in, postfix-length, rev-length, blastn-len-0, blastN-rec, mk-empty, prefix-app-02, mk-one-01, nodups-butlastn, mk-one, mk-tail-01, mk-rec, mk-tail, mklist-append, butlast-len, lb, postfix-more, mklist-last, prefix-intro, le-leq-one-empty-or-head-equal-last, mk-butlast-01, prefix-app-03, blastN-rec-01, rev-mklist, mklist-split-intro, lb-01, mklist-rmdup-01, mk-last-02, mk-last, prefix-size-eq, prefix-longer-01, mk-two, blastN-mklist, last-sizeone, mk-inj-01, blastN-len, mk-butlast, mk-plus, mk-inj, mk-len,
nat-basic/eq-01 is used by rev-length, lb, mk-inj-01, blastN-len, mk-inj, mk-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, nodups-butlastn, lb-01,
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-in, postfix-length, nodups-butlastn, mk-one, mk-tail-01, mk-rec, mk-tail, postfix-more, mk-butlast-01, blastN-rec-01, rev-mklist, mklist-rmdup-01, mk-last-02, mk-two, blastN-mklist, mk-inj-01, blastN-len, mk-butlast, mk-inj,
nat-basic/pred is used by mk-butlast-01, rev-mklist, mklist-rmdup-01, blastN-mklist, mk-butlast,
nat-basic/refl-nat is used by postfix-split-stronger, nodups-butlastn, blastN-rec-01, lb-01, blastN-len, blastN-all,
nat-basic/s-04 is used by postfix-split-stronger, postfix-length, nodups-butlastn, blastN-rec-01, lb-01, blastN-len,
nat-basic/succ is used by mk-in, mk-empty, mk-one-01, nodups-butlastn, mk-one, mk-elem, rev-mklist, mklist-rmdup-01, mk-last, blastN-mklist, mk-inj-01, mk-plus, mk-inj, mk-len,
nat-basic/z-01 is used by mk-one-01, mk-tail-01, mk-tail, mk-butlast-01, prefix-app-03, mk-two, blastN-mklist, blastN-len, mk-butlast, mk-inj,
nat-basic/z-02 is used by blastN-len, mk-plus,

Used from specification nat

nat/add-01 is used by mk-one-01, mk-tail-01, mk-tail, mk-two, mk-inj-01, mk-inj,
nat/add-num-03 is used by mk-two,
nat/elim-pred-c is used by blastN-rec, mk-tail-01, mk-rec, mk-tail, lb, mk-butlast-01, blastN-rec-01, mk-last-02, mk-inj-01, blastN-len, mk-butlast, mk-inj,
nat/elim-sub is used by mklist-split-intro, blastN-len,
nat/eq-01 is used by blastn-len-0, butlast-len,
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, postfix-length, blastn-len-0, nodups-butlastn, lb-01, blastN-all,
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 nodups-butlastn, blastN-rec-01,
nat/les is used by nodups-butlastn,
nat/lez-01 is used by nodups-butlastn, blastN-rec-01,
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 blastN-rec, mk-last-01, mk-tail-01, mk-tail, blastN-rec-01, mk-last-02, blastN-len,
nat/zero is used by blastN-all,

Used from specification list-data

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

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-01, rev-disjoint,
list-dup/e is used by rev-disjoint-01, rev-disjoint,
list-dup/e-01 is used by nodups-butlastn, rev-dups,
list-dup/first is used by rev-disjoint-01, rev-disjoint,
list-dup/last is used by rev-disjoint,
list-dup/one-01 is used by rev-disjoint-01, rev-disjoint,
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-01, rev-disjoint,