[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, butlast-len,
nat/elim-pred-c is used by mk-rest-01, mk-rest, mk-rec, mk-last-02, mk-inj-01, mk-butlast-01, mk-butlast, lb, blastN-rec-01, blastN-rec, blastN-mklist, blastN-len,
nat/elim-sub is used by mklist-split-intro, blastN-len,
nat/eq-01 is used by blastn-len-0,
nat/eq-02 is used by nodups-butlastn, mk-inj,
nat/eqle-one is used by nodups-butlastn,
nat/le-add is used by prefix-app-03, prefix-app-02,
nat/lels is used by prefix-app-03, prefix-app-02, postfix-length,
nat/lels-01 is used by postfix-split-stronger, postfix-length, nodups-butlastn, mk-inj, lb-01, blastn-len-0,
nat/lep is used by prefix-intro, blastN-len,
nat/lep-02 is used by nodups-butlastn, blastN-rec-01,
nat/ler is used by blastN-all,
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-first-equal-last,
nat/pred-03 is used by mk-rest-01, mk-rest, mk-last-02, blastN-rec-01, blastN-rec, blastN-len,
nat/succ-01 is used by postfix-length,
nat/zero is used by blastN-all,

Used from specification list-data

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

Used from specification list

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

Used from specification nat-basic2

nat-basic2/a is used by rev-mklist, rev-length, prefix-size-eq, prefix-longer-01, prefix-intro, prefix-app-03, prefix-app-02, postfix-split-stronger, postfix-more, postfix-length, nodups-butlastn, mklist-split-intro, mklist-rmdup-01, mklist-one, mklist-last, mklist-append, mk-two-01, mk-two, mk-succ, mk-rest-01, mk-rest, mk-rec, mk-plus, mk-one-01, mk-last-02, mk-last-01, mk-last, mk-inj-01, mk-inj, mk-in, mk-empty, mk-butlast-01, mk-butlast, le-leq-one-empty-or-first-equal-last, lb-01, lb, last-one, butlast-len, blastn-len-0, blastN-rec-01, blastN-rec, blastN-mklist, blastN-len,
nat-basic2/add-base is used by mk-inj-01, butlast-len, blastN-len,
nat-basic2/c is used by rev-mklist, rev-length, prefix-size-eq, prefix-longer-01, prefix-intro, prefix-app-03, prefix-app-02, postfix-split-stronger, postfix-more, postfix-length, nodups-butlastn, mklist-split-intro, mklist-rmdup-01, mklist-one, mklist-last, mklist-append, mk-two-01, mk-two, mk-succ, mk-rest-01, mk-rest, mk-rec, mk-plus, mk-one-01, mk-last-02, mk-last-01, mk-last, mk-inj-01, mk-inj, mk-in, mk-empty, mk-butlast-01, mk-butlast, le-leq-one-empty-or-first-equal-last, lb-01, lb, last-one, butlast-len, blastn-len-0, blastN-rec-01, blastN-rec, blastN-mklist, blastN-len,
nat-basic2/eq is used by prefix-size-eq, postfix-more,
nat-basic2/eq-01 is used by rev-length, mk-succ, mk-inj-01, lb, blastN-len,
nat-basic2/l-02 is used by prefix-longer-01, postfix-length, blastn-len-0,
nat-basic2/one is used by mk-one-01,
nat-basic2/one-03 is used by le-leq-one-empty-or-first-equal-last, last-one,
nat-basic2/oz is used by rev-mklist, postfix-more, nodups-butlastn, mklist-rmdup-01, mk-rest-01, mk-rest, mk-rec, mk-last-02, mk-last-01, mk-inj-01, mk-inj, mk-in, mk-butlast-01, mk-butlast, blastN-rec-01, blastN-rec, blastN-mklist, blastN-len,
nat-basic2/pred is used by rev-mklist, mklist-rmdup-01, blastN-mklist,
nat-basic2/s is used by postfix-split-stronger, postfix-length, nodups-butlastn, lb-01, blastN-rec-01, blastN-len,
nat-basic2/succ is used by rev-mklist, rev-length, postfix-more, postfix-length, nodups-butlastn, mklist-rmdup-01, mk-two, mk-succ, mk-plus, mk-one-01, mk-last-01, mk-last, mk-inj-01, mk-inj, mk-in, mk-empty, mk-butlast-01, mk-butlast, le-leq-one-empty-or-first-equal-last, last-one, butlast-len, blastN-mklist,
nat-basic2/z is used by mk-plus,
nat-basic2/z-01 is used by rev-mklist, prefix-app-03, postfix-more, mklist-rmdup-01, mk-inj-01, blastN-len,

Used from specification nat-basic1

nat-basic1/f is used by prefix-longer-01, postfix-length, nodups-butlastn, blastn-len-0,
nat-basic1/lf-01 is used by nodups-butlastn,
nat-basic1/lf-02 is used by blastn-len-0,
nat-basic1/one is used by bnotempty,
nat-basic1/one-01 is used by postfix-split-stronger, nodups-butlastn, mk-inj, lb-01,
nat-basic1/ref-1 is used by postfix-split-stronger, nodups-butlastn, lb-01, blastN-rec-01, blastN-len,
nat-basic1/zero-01 is used by lb-01,