Used simplifier rules/spec theorems by specification

Used from specification nat-basic

• nat-basic/a is used by dups-lesize, rm-size-05, dups-eqsize-02, dups-rmdup-size-equiv, k-dups, rm-size, rm-size-not, rm-allsize, dups-eqsize-01, rm-size-01,
• nat-basic/c is used by dups-lesize, rm-size-05, dups-eqsize-02, dups-rmdup-size-equiv, k-dups, rm-size, rm-size-not, rm-allsize, dups-eqsize-01, rm-size-01,
• nat-basic/eq-01 is used by dups-eqsize-02, dups-rmdup-size-equiv, rm-size, rm-allsize, dups-eqsize-01, rm-size-01,
• nat-basic/f is used by rm-size-04, dups-lesize, rm-size-05, dups-eqsize, rm-size-03,
• nat-basic/l is used by rm-size-05,
• nat-basic/l-02 is used by rm-size-05,
• nat-basic/ls-02 is used by rm-size-04, dups-eqsize, rm-size-03,
• nat-basic/one is used by k-dups,
• nat-basic/one-06 is used by k-dups,
• nat-basic/s-04 is used by dups-lesize,
• nat-basic/succ is used by dups-lesize, dups-eqsize-02, dups-eqsize-01,

Used from specification nat

• nat/add-num-01 is used by rm-size,
• nat/eq is used by rm-size-not,
• nat/fle is used by rm-size-05,
• nat/gr-def is used by k-dups,
• nat/le-def is used by dups-lesize, rm-size-le,
• nat/le-ls-simp is used by rm-size-05,
• nat/lels is used by dups-lesize, rm-size-05,
• nat/lels-02 is used by rm-size-04, dups-eqsize, rm-size-03,
• nat/succ-01 is used by dups-lesize,

Used from specification list-data

• list-data/elim-list-c is used by dups-rest, eq-01, k-dups, dups-in, rec, eq,
• list-data/l is used by rm-size-04, dups-lesize, rm-size-05, dups-eqsize-02, dups-eqsize, k-dups, rm-size-03, rm-allsize, dups-eqsize-01,
• list-data/size-nil is used by rm-size-05, dups-eqsize-02, dups-rmdup-size-equiv, rm-allsize, dups-eqsize-01,

Used from specification list

• list/firsteq is used by eq-01, inapp-01, inapp, eq,
• list/firstoc is used by rm-allsize,
• list/firstoc-rew is used by dups-firstoc-rew,
• list/in-def is used by dups-lesize, dups-eqsize-02, rm-allsize, rec, dups-eqsize-01,
• list/lastdiv is used by in-09, inapp-01, inapp,
• list/lastoc-rew is used by lastoc,
• list/Nil is used by rm-in-05, f-01, app-02, eq-01, rm-rm-02, f, rm-size-02, app, app-01-02, dups-sw, inapp-01, inapp, rm-size, two-03, firstoc, d, dups-appex, rm-in-04, rmdup-last, rm-rm-01, rec, rm-in, rm-size-01, eq,
• list/a is used by cons-02, lastoc, rm-in-05, rm-size-04, first, app-05, aa, in-06, f-01, dups-rest, app-02, l-01, rm-in-02, two, eq-01, dups-lesize, rm-rm-02, rm-size-in, in-09, f, rm-size-05, l, two-02, last-01, dups-eqsize-02, rm-ifrec, c, rm-size-02, rm-in-03, rm-notin, rm-eq, dups-switch, app, in-01-02, dups-rmdup-size-equiv, dups-firstoc-rew, app-01-02, dups-sw, in-07, cons-03, in-06-01, in-02-01, inapp-01, app-03, l-02, k-dups, first-01, in-04-01, dups-01, a, inapp, rm-size, two-03, firstoc, c-01, d, e-01, dups-appex, a-01, cons-01, rm-size-03, rm-allsize, rm-in-04, rmdup-last, app-01, rm-in-01, dups-in, last, rm-nodups, rm-notin-01, one-03, cons, rm-size-in-01, in-08, rm-rm-01, sym, cons-04, rec, two-01, l-03, rm-in, dups-eqsize-01, rm-size-01, fin, eq, in-05-01, empty-01, rm-empty, n, in-03-01,
• list/app is used by two, in-09, rm-size-05, dups-sw, inapp-01, inapp, one-03, empty-01, rm-empty,
• list/app-01 is used by rm-rm-02, rm-ifrec, rmdup-last, rm-rm-01,
• list/app-02 is used by eq-01, c, e-01, eq, rm-empty,
• list/app-05 is used by rm-in-05, rm-in-04,
• list/app-06 is used by in-09, inapp-01, inapp,
• list/app-08 is used by eq-01, rm-eq, firstoc, rec,
• list/c is used by cons-02, lastoc, rm-in-05, app-05, in-06, f-01, dups-rest, app-02, rm-in-02, two, eq-01, dups-lesize, rm-rm-02, f, rm-size-05, l, dups-eqsize-02, rm-ifrec, c, rm-size-02, rm-in-03, rm-notin, rm-eq, app, dups-rmdup-size-equiv, dups-firstoc-rew, app-01-02, dups-sw, k-dups, dups-01, a, rm-size, two-03, firstoc, d, e-01, dups-appex, cons-01, rm-allsize, rm-in-04, rmdup-last, rm-in-01, dups-in, rm-nodups, one-03, in-08, rm-rm-01, sym, rec, rm-in, dups-eqsize-01, rm-size-01, eq, empty-01, rm-empty,
• list/c-04 is used by rmdup-last, empty-01,
• list/c-06 is used by eq-01, inapp-01, inapp, rec, eq,
• list/c-07 is used by eq-01, eq,
• list/c-08 is used by eq-01, eq,
• list/e is used by rm-in-05, c, e-01, rm-in-04, empty-01, rm-empty,
• list/e-01 is used by dups-rest, eq-01, dups-lesize, rm-size-05, k-dups, two-03, dups-in, eq, rm-empty,
• list/e-02 is used by eq-01, in-09, inapp-01, inapp, eq,
• list/eq-04 is used by c,
• list/first is used by eq,
• list/first-02 is used by eq-01, eq,
• list/first-app is used by eq-01, eq,
• list/in-01 is used by cons-02, f-01, eq-01, two-02, dups-eqsize-02, in-07, inapp-01, inapp, rm-size, rm-in-01, in-08, rec, rm-in, dups-eqsize-01, eq, n,
• list/in-06 is used by rm-in-05, app-02, eq-01, rm-in-03, rm-notin, in-02-01, rm-size, two-03, d, rmdup-last, rm-in-01, cons, in-08, rm-in, dups-eqsize-01, eq, in-03-01,
• list/in-08 is used by inapp, rm-allsize,
• list/in-10 is used by lastoc, dups-firstoc-rew, inapp, rm-allsize,
• list/in-11 is used by eq-01, inapp, rm-size-in-01, rm-in, eq,
• list/in-12 is used by dups-firstoc-rew, inapp-01, rm-in-04, rm-in,
• list/in-13 is used by in-09, inapp, rm-allsize, rm-notin-01,
• list/in-14 is used by eq-01, inapp-01, inapp, rec, eq,
• list/in-15 is used by in-09, inapp-01, inapp,
• list/in-17 is used by cons-02, lastoc, rm-in-05, first, l-01, rm-in-02, two, in-09, f, l, one-01, rm-size-02, rm-in-03, rm-notin, in-07, cons-03, in-06-01, inapp-01, first-01, inapp, dups-appex, a-01, cons-01, rm-allsize, rmdup-last, sym, two-01, one, rm-size-01, in-05-01, n,
• list/in-append is used by cons-02, lastoc, rm-in-05, rm-size-04, first, app-05, in-06, f-01, l-01, rm-in-02, eq-01, dups-lesize, rm-rm-02, in-09, f, l, dups-eqsize-02, rm-size-02, rm-in-03, dups-firstoc-rew, app-01-02, dups-sw, in-07, cons-03, in-06-01, inapp-01, first-01, a, inapp, rm-size, firstoc, d, dups-appex, a-01, cons-01, rm-allsize, rmdup-last, rm-size-in-01, rm-rm-01, sym, rec, rm-in, dups-eqsize-01, rm-size-01, eq, in-05-01, n,
• list/in-empty is used by cons-02, lastoc, rm-in-05, in-06, f-01, rm-in-02, eq-01, in-09, f, l, dups-eqsize-02, rm-in-03, rm-notin, inapp-01, k-dups, dis-empty, firstoc, dups-appex, cons-01, rm-allsize, rm-in-01, rm-in, rm-size-01, eq, empty-01, e,
• list/in-rec is used by in-06, f-01, eq-01, dups-lesize, l, dups-eqsize-02, dups-firstoc-rew, inapp-01, firstoc, d, rec, dups-eqsize-01, eq,
• list/inapp-02 is used by eq-01, inapp, rec, eq,
• list/inapp-04 is used by inapp-01,
• list/inapp-11 is used by inapp,
• list/inapp-14 is used by in-09,
• list/isin-01 is used by inapp,
• list/len is used by dups-lesize, rm-size-05, dups-eqsize-02, rm-size-02, dups-rmdup-size-equiv, k-dups, rm-size, rm-allsize, dups-eqsize-01, rm-size-01,
• list/len-02 is used by rm-size-05, rm-size-02, dups-rmdup-size-equiv, k-dups, rm-size, rm-allsize, rm-size-01,
• list/len-05 is used by dups-lesize, dups-eqsize-02, dups-eqsize-01,
• list/neq is used by rm-allsize, rm-notin-01, rec,
• list/neq-01 is used by eq-01,
• list/neq-02 is used by inapp-01,
• list/neq-09 is used by eq,
• list/ni is used by in-09, inapp-01,