Used simplifier rules/spec theorems by specification

Used from specification nat-basic

• nat-basic/neq-01 is used by union-sizele,
• nat-basic/a is used by size-del-leq, union-size-le, union-size-02, diff-sub-size, intersection-size, union-size-not-less-01, del-size-01, size-union, del-three, union-size-03, union-size-not-less-02, del-size, union-size-ls-in, union-size-insert,
• nat-basic/c is used by size-del-leq, union-size-le, union-size-02, diff-sub-size, intersection-size, union-size-not-less-01, del-size-01, size-union, del-three, union-size-03, union-size-not-less-02, del-size, union-size-ls-in, union-size-insert,
• nat-basic/eq-01 is used by diff-sub-size, size-union, union-size-03,
• nat-basic/eq-02 is used by union-size-02, diff-sub-size,
• nat-basic/eqs is used by union-size-03,
• nat-basic/f is used by union-size-le, diff-sub-size, intersection-size, union-size-not-less-01, union-size, union-sizele, del-three, union-size-03, union-size-not-less-02, union-size-not-less,
• nat-basic/l is used by union-size-le, intersection-size, union-size-not-less-01,
• nat-basic/l-01 is used by diff-sub-size,
• nat-basic/l-02 is used by union-size-not-less-02,
• nat-basic/l-04 is used by union-size-not-less-01,
• nat-basic/less-zero is used by intersection-size,
• nat-basic/lf-01 is used by diff-sub-size,
• nat-basic/nls-fst is used by union-size-le, intersection-size,
• nat-basic/one is used by del-ne, del-three,
• nat-basic/one-01 is used by size-del-leq, union-size-02, diff-sub-size, del-size-01,
• nat-basic/oz is used by del-three,
• nat-basic/refl-nat is used by size-del-leq, union-size-le, union-size-not-less-01, union-sizele,
• nat-basic/z-02 is used by union-size-le, diff-sub-size, intersection-size, size-union, union-size-03,

Used from specification nat

• nat/elim-sub is used by diff-sub-size,
• nat/fle is used by union-size-not-less-01,
• nat/add-01 is used by union-size-03,
• nat/anti is used by diff-sub-size,
• nat/cancel-01 is used by union-size-03,
• nat/elim-pred-c is used by del-three,
• nat/elim-sub is used by union-size-02, diff-sub-size, union-size-03,
• nat/eq-01 is used by del-size-01, del-size,
• nat/eq-02 is used by diff-sub-size, del-size-01,
• nat/fle is used by union-size-not-less-01, union-sizele, union-size-not-less-02,
• nat/fle-01 is used by union-sizele,
• nat/l-num-04 is used by del-three,
• nat/le-add is used by size-del-leq, union-size-ls-in,
• nat/le-def is used by size-del-leq, union-size-le, union-size-02, diff-sub-size, del-size-01, union-sizele, union-size-03, union-size-not-less-02, union-size-ls-in,
• nat/le-sum is used by union-size-not-less-01,
• nat/lels is used by diff-sub-size, union-size-not-less-01, union-size-ls-in,
• nat/lep-02 is used by union-size-ls-in,
• nat/ler is used by diff-sub-size, union-size-not-less-01,
• nat/lez is used by diff-sub-size,
• nat/ls-02 is used by size-del-leq, union-size-ls-in,
• nat/ls-le-simp is used by union-size-03, union-size-not-less,
• nat/sub-base is used by union-size-03,
• nat/succ-01 is used by diff-sub-size,

Used from specification set-basic

• set-basic/Extension is used by subseteq-rem-del, diff-supset-empty, add-inter-rem, size-eq-ext, subset-is-union, rem-inter-empty3, rem-union-ins, empty-intersection-diff, subseteq-inter-empty-empty, union-diff-union-same, add-rem-sub, union-sub-rem-inter-empty, sub-rem-inter-rem, union-rem-add,
• set-basic/Size-insert is used by intersection-size, size-union, union-size-03,
• set-basic/Subset is used by subseteq-rem-del, inter-empty-diff, subseteq-inter-empty-empty, union-sub-rem-inter-empty,
• set-basic/eq is used by union-size-le, intersection-size, subset-is-union, union-size-03,
• set-basic/indef is used by del-size,
• set-basic/size-exgr is used by diff-sub-size,
• set-basic/size-two-03 is used by del-ne,
• set-basic/sub-insert is used by subset-is-union,
• set-basic/sub-size is used by union-size,
• set-basic/subsize-eq is used by union-sizeeq,
• set-basic/Extension is used by del-in-03, k-delete-rec, int-inse, del-feq, del-neq-02, k-union-base, intersection-shift, union-size-le, int-c, del-e-02, une-01, intersection-insert, union-size-02, subsub-del, unidem, diff-sub-size, intersection-size, k-union-rec1, int-idem, unc, del-feq-01, sub-ade, union-subset-05, diff-del-minus-2, del-ne, diff-del, k-diff-rec1, unsub-union-01, union-rewone, int-empty-one, del-d-01, sub-union, del-addeq-01, one-min, diff-e-01, sub-union-01, delete-insert, diff-del-minus, del-in, undel-06, del-addeq-04, equal-add-in, insdel-sub, diff-empty, sub-ade-02, unsubdel, sub-del-03, union-inter-inter-union, del-size-01, size-union, una, del-del-one, intersect-add-rem, int-empty-01, delsw-01, k-diff-rec2, diff-idem, union-sizele, uneq, diff-add-del, union-sub, diff-int-01, del-three, unadd-01, k-intersect-base, diff-del-plus-1, diff-rc, union-size-03, unsubdel-01, del-d, diff-del-minus-3, int-inserte, del-feq-02, k-union-rec2, int-a, int-del-rew, delsw, int-ins, delsw-02, int-eq, diff-e, undel-01, k-intersect-rec1, union-subset-03, unall, del-addeq-02, delete-shift, int-notempty-01, del-neq-01, del-size, intdel-empty, union-size-ls-in, intu-empty, del-two, del-addeq-05, undel-04, sub-del-04, une, del-e-01, del-addeq, sub-ade-03, union-sub-01, del-size-02, int-empty-02, sub-del-01, int-empty, del-eq, intexin, diff-del-plus-2, union-sizeeq, union-difference, sub-del, union-subset-01, int-e, del-e, diff-int, int-notempty, undel-05, unadd, selsub-diff, del-addeq-06, undel-02, undel, unsubsub, diff-union-03, k-intersect-rec2, sub-ade-01,
• set-basic/In-empty is used by int-inse, diff-supset-empty, del-feq, intersection-shift, union-size-le, del-e-02, une-01, union-size-02, subsub-del, diff-sub-size, intersection-size, sub-ade, union-subset-05, del-ne, diff-del, k-diff-rec1, unsub-union-01, sub-union, diff-e-01, sub-union-01, rem-inter-empty3, insdel-sub, diff-empty, sub-ade-02, unsubdel, sub-del-03, del-size-01, size-union, int-empty-01, diff-idem, union-sizele, uneq, diff-int-01, del-three, diff-del-plus-1, union-size-03, int-inserte, int-ins, int-eq, diff-e, k-intersect-rec1, union-subset-03, unall, delete-shift, int-notempty-01, del-neq-01, del-size, subseteq-inter-empty-empty, intdel-empty, union-size-ls-in, intu-empty, del-two, sub-del-04, une, del-e-01, del-addeq, sub-ade-03, union-sub-01, del-size-02, int-empty-02, sub-del-01, int-empty, del-eq, intexin, union-sizeeq, sub-del, union-subset-01, int-e, del-e, union-sub-rem-inter-empty, diff-int, int-notempty, selsub-diff, unsubsub, sub-ade-01,
• set-basic/In-insert is used by sub-union-03, subseteq-rem-del, k-delete-rec, int-inse, del-feq, del-neq-02, add-inter-rem, diff-del-02, intersection-shift, intersection-insert, diff-sub-size, del-feq-01, sub-ade, union-subset-05, del-addin, union-subset-02, del-addeq-01, sub-union-01, delete-insert, del-addeq-04, equal-add-in, insdel-sub, sub-ade-02, sub-union-04, size-union, intersect-add-rem, diff-add-del, unadd-01, diff-del-plus-1, rem-union-ins, int-inserte, del-feq-02, delsw, int-ins, k-intersect-rec1, unsubins-01, del-addeq-02, delete-shift, sub-union-02, int-notempty-01, del-addin-01, del-neq-01, unsubins, del-two, del-addeq-05, del-addeq, union-one, sub-ade-03, union-subset-04, int-empty, sub-union-05, diff-del-plus-2, add-rem-sub, diff-one, del-e, int-notempty, unadd, del-addeq-06, delete-subset, union-rem-add, sub-ade-01, diff-subset-01,
• set-basic/Size-empty is used by union-size-le, diff-sub-size, intersection-size, size-union, union-size-03,
• set-basic/Size-insert is used by union-size-le, diff-sub-size, intersection-size, size-union, union-size-03, del-size,
• set-basic/Subset is used by sub-union-03, diff-del-02, sub-del-05, subsub-del, diff-sub-size, diff-subset, sub-del-02, sub-ade, union-subset-05, union-size, unsub-union-01, union-subset-02, sub-union, sub-union-01, insdel-sub, sub-ade-02, unsubdel, sub-del-03, sub-union-04, union-sizele, uneq, int-subs01, int-eq, unsub, unsubins-01, union-subset-03, sub-union-02, unsubins, diff-del-01, sub-del-04, union-size-01, sub-ade-03, union-sub-01, union-subset-04, sub-del-01, sub-union-05, union-sizeeq, union-difference, sub-del, diff-sub, union-subset-01, diff-one, selsub-diff, delete-subset, unsubsub, sub-ade-01, diff-subset-01,
• set-basic/eq is used by add-inter-rem, diff-sub-size, size-union, union-size-03,
• set-basic/eq-03 is used by uninsert, del-addeq-03,
• set-basic/in-02 is used by add-rem-sub, del-e,
• set-basic/in-03 is used by subset-is-union,
• set-basic/in-04 is used by del-e-02, subset-is-union, del-del-one, one-in, del-two, diff-one,
• set-basic/ne is used by subset-is-union,
• set-basic/ne-01 is used by subseteq-rem-del, int-inse, del-feq, add-inter-rem, size-del-leq, intersection-shift, union-size-le, del-e-02, une-01, union-size-02, subsub-del, diff-sub-size, intersection-size, sub-ade, union-subset-05, diff-del, k-diff-rec1, unsub-union-01, union-subset-02, sub-union, sub-union-01, subset-is-union, rem-inter-empty3, insdel-sub, diff-empty, sub-ade-02, uninsubdel, unsubdel, sub-del-03, del-size-01, size-union, int-empty-01, union-sizele, uneq, del-three, diff-del-plus-1, union-size-03, unsubdel-01, rem-union-ins, int-inserte, int-ins, int-eq, k-intersect-rec1, union-subset-03, unall, delete-shift, int-notempty-01, inter-empty-diff, del-size, subseteq-inter-empty-empty, intdel-empty, union-size-ls-in, intu-empty, del-two, sub-del-04, del-addeq, sub-ade-03, union-sub-01, del-size-02, union-subset-04, int-empty-02, sub-del-01, int-empty, del-eq, intexin, union-diff-union-same, union-sizeeq, sub-del, union-subset-01, add-rem-sub, del-e, union-sub-rem-inter-empty, int-notempty, selsub-diff, sub-rem-inter-rem, union-rem-add, unsubsub, diff-diff-right, sub-ade-01,
• set-basic/one-size is used by subset-is-union,
• set-basic/size-ins is used by union-size-insert,
• set-basic/size-one-01 is used by subset-is-union,
• set-basic/size-one-02 is used by del-three,
• set-basic/size-zero is used by diff-supset-empty, del-ne, subset-is-union, rem-inter-empty3, subseteq-inter-empty-empty,
• set-basic/size-zero-01 is used by subseteq-rem-del, diff-supset-empty, add-inter-rem, diff-sub-size, unsub-union-01, union-subset-02, subset-is-union, rem-inter-empty3, size-union, rem-union-ins, intersect-empty-rem, inter-empty-diff, subseteq-inter-empty-empty, intu-empty, union-subset-04, add-rem-sub, union-sub-rem-inter-empty, sub-rem-inter-rem, union-rem-add, diff-diff-right,
• set-basic/size-zero-02 is used by size-del-leq, union-size-02, diff-sub-size, del-size-01, del-three, union-size-ls-in,
• set-basic/sub-add-02 is used by union-sizele-01,
• set-basic/sub-add-03 is used by union-sizele-01,
• set-basic/sub-idem is used by subset-del,
• set-basic/sub-in is used by subseteq-rem-del, subset-is-union, uninsubdel, unsubdel-01,
• set-basic/subset-empty is used by subset-is-union,