[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/elim-pred-c is used by diffone-nodupssize, diffone-nodupsget, diffgetn-nodupssize,
nat/eq-02 is used by diffone-nodupssize, diffgetn-nodupssize,
nat/fle is used by sub-size-01,
nat/le-ls-simp is used by le, diffone-nodupsget, diffgetn-nodupssize,
nat/lels is used by le, diffone-nodupsget, diffgetn-nodupssize,
nat/lels-01 is used by sub-size, size-le, le, diffone-nodupssize, diffgetn-nodupssize,
nat/ler is used by sub-size-02, size-nle, size-le,
nat/lez-01 is used by le, diffgetn-nodupssize,
nat/ls-01 is used by le,
nat/ls-02 is used by diffgetn-nodupssize,
nat/ls-le-simp is used by size-nls,
nat/pred-03 is used by le,
nat/succ-01 is used by diffone-nodupsget, diffgetn-nodupssize,

Used from specification list-last

list-last/rev-in is used by filter-rev-empty,

Used from specification list-data

list-data/elim-list-c is used by filter-rest,
list-data/l is used by sub-size-01, size-nls-01, size-nls, size-le, le, diffone-nodupssize, diffone-nodupsget, diffgetn-nodupssize,
list-data/size-01 is used by le, diffone-nodupssize, diffgetn-nodupssize,

Used from specification list

list/Nil is used by subset-rmdup, filter-empty, empty-01, dups-app, diff-firstofapp, diff-consbothsame, diff-append, diff-app-02, diff-app,
list/a is used by subsub-01, subsub, subset-rmdup, subset-rec, subset-perm, subset-diff-union, subset-append-02, subset-append-01, subset-append, subset-app-04, subset-app-03, subset-app-02, subset-app-01, subset-app, subset-01-01, subset-01, subonein, suband, sub-size-02, sub-07, sub-06, sub-05, sub-04, sub-03, sub-02, sub-01, sub, size-nls-01, size-nls, size-nle, size-le, rotsize, rmdup-01, rmdup, rax-01, onenotin-diff, notin-02, notin-01, notin, le, k-union-rec-y, k-union-rec-n, insub-01, insub, in-04, in-03, in-02, in-01-01, in-01, in, firstsub, firstinsub, firstin, filter-rest, filter-one-02, filter-one-01, filter-notin, filter-notempty, filter-empty-in-01, filter-empty-in, filter-empty-def, filter-empty-cons-01, filter-empty-cons, filter-empty-append, filter-empty-app-04, filter-empty-app-03, filter-empty-app-02, filter-empty-app-01, filter-empty-app, filter-empty, filter-dups, filter-all, filt-dups, f-rm, emptyunion, empty-01, empty, dups-app, diffone-nodupssize, diffone-nodupsget, diffgetn-nodupssize, diff-wfrec, diff-union, diff-unchanged, diff-twice-union, diff-twice-append-rev, diff-twice-append, diff-same, diff-onenonmember, diff-in, diff-firstofapp, diff-empty-all, diff-empty, diff-dups, diff-consnotin2, diff-consbothsame, diff-append, diff-app-02, diff-app-01, diff-app, del1-01, del1, commsize, assoc, appsize, app, Noassoc,
list/app is used by filter-one-02, filter-one-01, empty, diffgetn-nodupssize, diff-same, diff-app-01,
list/app-01 is used by k-union-rec-n, f-rm,
list/app-02-ant is used by emptyunion,
list/app-05 is used by k-union-rec-n,
list/app-08 is used by rax-01, notin, filter-notin, diff-wfrec, diff-union, diff-unchanged, diff-twice-union, diff-twice-append-rev, diff-twice-append, diff-onenonmember, diff-empty, diff-consnotin2, diff-append, del1-01, del1,
list/c is used by subset-rmdup, rmdup-01, rmdup, rax-01, onenotin-diff, notin-02, notin-01, notin, le, k-union-rec-y, k-union-rec-n, in-01-01, filter-rest, filter-notin, filter-notempty, filter-empty-def, filter-empty, filter-dups, filter-all, filt-dups, f-rm, dups-app, diffone-nodupssize, diffone-nodupsget, diffgetn-nodupssize, diff-wfrec, diff-union, diff-unchanged, diff-twice-union, diff-twice-append-rev, diff-twice-append, diff-onenonmember, diff-in, diff-empty-all, diff-empty, diff-dups, diff-consnotin2, diff-append, diff-app-02, diff-app-01, del1-01, del1,
list/c-04 is used by onenotin-diff,
list/e is used by k-union-rec-n, filter-one,
list/e-01 is used by le, filter-empty-def, filter-empty, filter-all, dups-app, diffone-nodupssize, diffone-nodupsget, diffgetn-nodupssize, diff-empty-all,
list/in-01 is used by rmdup-01, in-02, filter-notin, diff-consnotin2,
list/in-06 is used by rmdup-01, onenotin-diff, filter-notin, diff-wfrec, diff-onenonmember, diff-consnotin2, del1-01, del1,
list/in-08 is used by subset-empty-01,
list/in-11 is used by subset-app-02, subset-app, insub, diff-twice-union, diff-twice-append-rev, diff-twice-append,
list/in-12 is used by subset-app-01, insub-01, in-01, firstinsub, diff-twice-append-rev, diff-twice-append,
list/in-14 is used by diff-unchanged,
list/in-17 is used by subset-one, rmdup-01, rmdup, onenotin-diff, in-02, filter-empty-one, diffone-nodupssize, diffone-nodupsget, diffgetn-nodupssize, diff-onenonmember, diff-in-one,
list/in-append is used by subset-perm, subset-diff-union, subset-append-02, subset-append-01, subset-append, subset-app-04, subset-app-03, subset-app-02, suband, sub-07, sub-06, sub-05, sub-04, size-nls-01, size-nls, size-nle, rotsize, rmdup, k-union-rec-n, in-04, in-03, in, filter-empty-in, filter-empty-app-03, filter-empty-app, filter-dups, dups-app, diff-union, diff-twice-append-rev, diff-twice-append, diff-app-01, commsize,
list/in-empty is used by subset-empty-01, subset-empty, rmdup-01, rmdup, notin-02, notin-01, le, in-01-01, filter-notempty, filter-empty-01, diffone-nodupssize, diffgetn-nodupssize, diff-unchanged, diff-in, diff-empty-all, diff-empty,
list/in-rec is used by subset-rec, notin-02, notin-01, in-01-01, filter-notempty, filter-empty-def, filter-empty-cons, filter-all, diffone-nodupssize, diffone-nodupsget, diff-wfrec, diff-unchanged, diff-in, diff-empty-all, diff-app-01,
list/len-02 is used by diffone-nodupsget, diffgetn-nodupssize,
list/len-05 is used by le, diffone-nodupssize, diffone-nodupsget, diffgetn-nodupssize,

Used from specification nat-basic2

nat-basic2/a is used by le, diffone-nodupssize, diffone-nodupsget, diffgetn-nodupssize,
nat-basic2/c is used by le, diffone-nodupssize, diffone-nodupsget, diffgetn-nodupssize,
nat-basic2/eq-01 is used by diffone-nodupssize, diffgetn-nodupssize,
nat-basic2/l is used by diffone-nodupsget,
nat-basic2/oz is used by diffone-nodupsget, diffgetn-nodupssize,
nat-basic2/s is used by le, diffone-nodupsget, diffgetn-nodupssize,
nat-basic2/succ is used by le, diffone-nodupssize, diffone-nodupsget, diffgetn-nodupssize,

Used from specification list-dup

list-dup/dups-eqsize is used by size,
list-dup/dups-lesize is used by sub-size-01, size-nls,
list-dup/rm-allsize is used by size-nls-01, rotsize, commsize,
list-dup/rm-ifrec is used by diff-union, del1-01,
list-dup/rmdup-n is used by k-union-rec-n, diff-union,
list-dup/rmdup-y is used by le, f-rm,
list-dup/a is used by filter-dups,
list-dup/c-02 is used by filter-dups,
list-dup/e-01 is used by filt-dups, dups-app, diffgetn-nodupssize, diff-dups,
list-dup/in-08 is used by subset-insert,
list-dup/rec is used by filter-dups, filt-dups, dups-app, diffone-nodupssize, diffone-nodupsget, diffgetn-nodupssize, diff-dups,
list-dup/rm-empty is used by size-nls-01, size-nls, size-le, emptyunion,
list-dup/rm-in is used by rmdup-01, in-04, in-02, in-01, in, diff-twice-union,
list-dup/rm-in-01 is used by rmdup,
list-dup/rm-in-02 is used by sub-size-01, size-nls, in-06, in-04, in-03, in-02, in-01, in, diff-twice-union,
list-dup/rm-in-03 is used by rmdup,
list-dup/rm-in-04 is used by subset-rmdup, k-union-rec-y,
list-dup/rm-in-05 is used by k-union-rec-y,
list-dup/rm-nodups is used by sub-size-01, size-nls, nodups,
list-dup/rm-rm is used by rmdup-size, rmdup-02,
list-dup/rm-rm-01 is used by sub-05, sub-04, sub-03, sub-02, size-nls-01, size-nls, size-nle, rotsize, k-union-rec-y, in-03, diff-union, assoc, appsize, app, Noassoc,
list-dup/rm-rm-02 is used by assoc,
list-dup/rm-size-03 is used by sub-size-02, size-le,
list-dup/rm-size-04 is used by size-nle,
list-dup/rm-size-05 is used by sub-size-01,
list-dup/rm-size-in is used by sub-size-02, size-le,
list-dup/rm-size-in-01 is used by size-nle,
list-dup/rmdup-e is used by rmdup-01, le, f-rm, emptyunion, diff-union, del1-01,
list-dup/rmdup-n is used by notin, le, f-rm,
list-dup/rmdup-y is used by k-union-rec-n, firstin, f-rm, diff-union,

Used from specification nat-basic1

nat-basic1/f is used by sub-size-01, size-nls-01, size-nls, size-le, le, diffone-nodupsget, diffgetn-nodupssize,
nat-basic1/lf is used by diffone-nodupsget,
nat-basic1/lf-01 is used by size-nls-01, diffgetn-nodupssize,
nat-basic1/lf-02 is used by size-nls-01,
nat-basic1/ls-02 is used by size-nls-01,
nat-basic1/one-01 is used by le, diffone-nodupssize, diffone-nodupsget, diffgetn-nodupssize,
nat-basic1/ref-1 is used by size-le,
nat-basic1/trans-1 is used by diffone-nodupsget,
nat-basic1/zero-01 is used by diffone-nodupsget,

Used from specification list-del

list-del/del-n is used by diff-wfrec,
list-del/get-append-grt is used by diffone-nodupsget, diffgetn-nodupssize,
list-del/del-e is used by diff-wfrec,
list-del/del-y is used by diff-wfrec,
list-del/del1-e is used by le,
list-del/del1-in is used by del1-01, del1,
list-del/get-append-grt is used by diffone-nodupsget,
list-del/get-append-less is used by diffone-nodupsget, diffgetn-nodupssize,
list-del/get-nodups is used by diffone-nodupsget,
list-del/get-succ is used by diffone-nodupsget,
list-del/in-02 is used by subset-del,
list-del/in-del-new is used by subset-del,
list-del/inl is used by diffone-nodupsget,
list-del/l is used by le,
list-del/one-03 is used by diffgetn-nodupssize,
list-del/pos-n is used by diffone-nodupsget,
list-del/pos-y is used by diffone-nodupsget,