Used simplifier rules/spec theorems by specification

Used from specification nat-basic

• nat-basic/a is used by diffone-nodupsget, diffone-nodupssize, le, diffgetn-nodupssize,
• nat-basic/c is used by diffone-nodupsget, diffone-nodupssize, le, diffgetn-nodupssize,
• nat-basic/eq-01 is used by diffone-nodupssize, diffgetn-nodupssize,
• nat-basic/f is used by diffone-nodupsget, le, diffgetn-nodupssize, size-le, sub-size-01, size-nls, sub-size, size-nls-01,
• nat-basic/l is used by diffone-nodupsget,
• nat-basic/less-zero is used by diffone-nodupsget,
• nat-basic/lf is used by diffone-nodupsget,
• nat-basic/lf-01 is used by size-nls-01,
• nat-basic/lf-02 is used by size-nls-01,
• nat-basic/ls-02 is used by size-nls-01,
• nat-basic/one-01 is used by diffone-nodupsget, diffone-nodupssize, le, diffgetn-nodupssize,
• nat-basic/oz is used by diffone-nodupsget, diffgetn-nodupssize,
• nat-basic/refl-nat is used by size-le, size-nls,
• nat-basic/s-04 is used by diffone-nodupsget, le, diffgetn-nodupssize,
• nat-basic/succ is used by diffone-nodupsget, diffone-nodupssize, diffgetn-nodupssize,
• nat-basic/trans-nat is used by diffone-nodupsget,
• nat-basic/zero is used by diffone-nodupsget,

Used from specification nat

• nat/elim-pred-c is used by diffone-nodupsget, diffone-nodupssize, diffgetn-nodupssize,
• nat/eq-02 is used by diffone-nodupssize, diffgetn-nodupssize,
• nat/fle is used by sub-size-01, size-nls, sub-size,
• nat/fle-01 is used by size-nls,
• nat/le-def is used by diffone-nodupssize, le, diffgetn-nodupssize, size-le, sub-size,
• nat/le-ls-simp is used by diffone-nodupsget, le,
• nat/lels is used by diffone-nodupsget, le, diffgetn-nodupssize,
• nat/ler is used by size-nle, sub-size-02, 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/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 diffone-nodupsget, diffone-nodupssize, le, diffgetn-nodupssize, size-le, sub-size-01, size-nls, sub-size, size-nls-01,
• list-data/size-nil is used by diffone-nodupssize, le, diffgetn-nodupssize,

Used from specification list

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

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-in is used by del1, del1-01,
• 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/get-zero-01 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,