Used simplifier rules/spec theorems by specification

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/lels is used by rm-size-05, dups-lesize,
• nat/lels-01 is used by rm-size-le, dups-lesize,
• nat/lels-02 is used by rm-size-04, rm-size-03, dups-eqsize,
• nat/ls-add-not-01 is used by rm-size-05,
• nat/ls-le-simp is used by rm-size-04, rm-size-03, dups-eqsize,
• nat/succ-01 is used by dups-lesize,

Used from specification list-data

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

Used from specification list

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

Used from specification nat-basic2

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

Used from specification nat-basic1

• nat-basic1/f is used by rm-size-05, rm-size-04, rm-size-03, dups-lesize, dups-eqsize,
• nat-basic1/one is used by k-dups,