Used simplifier rules/spec theorems by specification

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 size-rm-eq,
• nat/elim-sub is used by union-size-03, union-size-02, diff-sub-size,
• nat/eq-01 is used by del-size, del-size-01,
• nat/eq-02 is used by diff-sub-size, del-size-01,
• nat/fle is used by union-size-not-less-01, union-size-not-less-02, union-sizele,
• nat/fle-01 is used by union-sizele,
• nat/l-num-04 is used by del-three,
• nat/le-add is used by union-size-ls-in, size-del-leq,
• nat/le-def is used by union-size-ls-in, union-size-not-less-02, union-size-03, union-size-02, diff-sub-size, size-del-leq, del-size-01, union-size-le, size-rm-less, del-size-le, union-sizele,
• nat/le-sum is used by union-size-not-less-01,
• nat/lels is used by union-size-ls-in, union-size-not-less-01, diff-sub-size,
• nat/lep-02 is used by union-size-ls-in,
• nat/ler is used by union-size-not-less-01, diff-sub-size,
• nat/lez is used by diff-sub-size,
• nat/ls is used by del-size-le,
• nat/ls-01 is used by size-rm-less,
• nat/ls-02 is used by union-size-ls-in, size-del-leq,
• nat/ls-le-simp is used by union-size-not-less, union-size-03,
• 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 filter-empty, rem-union-ins, filter-add, diff-union-04, union-rem-add, add-rem-sub, add-inter-rem, subseteq-rem-del, disjoint-all, union-diff-union-same, diff-supset-empty, disjoint-diff, size-eq-ext, filter-union, sub-rem-inter-rem, diff-diff-right-union,
• set-basic/Size-insert is used by union-size-03, size-union, intersection-size,
• set-basic/Subset is used by subseteq-rem-del, disjoint-diff-subset, diff-subset-02,
• set-basic/eq is used by union-size-03, union-size-le, intersection-size,
• set-basic/indef is used by del-size, del-three,
• set-basic/size-exgr is used by diff-sub-size,
• set-basic/size-two-03 is used by del-ne,
• set-basic/sub-size is used by union-size,
• set-basic/subsize-eq is used by union-sizeeq,
• set-basic/Extension is used by int-c, int-e, int-a, intersection-shift, undel-04, undel-02, undel-01, undel-06, intersect-add-rem, undel-05, del-two, unadd, del-eq, union-rewone, diff-e-01, diff-del-minus, unsub-union-01, del-neq-01, del-neq-02, delsw-01, k-union-rec1, k-union-rec2, union-size-ls-in, delete-insert, une-01, del-e-01, del-e-02, diff-union-03, diff-idem, int-del-rew, del-size, one-min, diff-empty, delsw-02, diff-int-01, uneq, intexin, del-d-01, del-in-03, k-intersect-base, del-addeq-02, del-addeq-04, del-addeq-05, union-size-03, union-size-02, del-addeq-01, del-addeq-06, unidem, diff-sub-size, une, unc, una, del-feq-02, del-feq-01, del-ne, diff-add-del, unall, del-size-01, del-addeq, int-idem, diff-del-plus-2, diff-del-plus-1, equal-add-in, union-difference, size-union, k-delete-rec, union-size-le, intersection-insert, union-sizeeq, del-d, diff-del-minus-3, unadd-01, diff-del-minus-2, k-diff-rec1, k-diff-rec2, del-feq, undel, diff-del, intersection-size, intdel-empty, k-intersect-rec1, k-union-base, k-intersect-rec2, union-inter-inter-union, union-sub, del-in, int-eq, delete-shift, delsw, selsub-diff, diff-rc, diff-int, diff-e,
• set-basic/In-empty is used by int-e, del-del-one, del-two, filter-empty, diff-e-01, unsub-union-01, disjoint-empty, del-neq-01, union-size-ls-in, une-01, disjoint-empty2, del-e-01, del-e-02, diff-idem, del-size, diff-empty, diff-int-01, intexin, exists-def, union-size-03, union-size-02, diff-sub-size, une, del-ne, disjoint-all, del-size-01, diff-supset-empty, size-union, union-size-le, union-sizeeq, intersection-size, intdel-empty, del-three, one-in, forall-def, diff-int, diff-e,
• set-basic/In-insert is used by del-del-one, intersection-shift, intersect-add-rem, del-two, unadd, rem-union-ins, filter-add, del-neq-01, del-neq-02, sub-union-05, sub-union-02, delete-insert, sub-union-01, sub-union-04, sub-union-03, delete-subset, del-e-02, del-addin, union-rem-add, exists-def, sub-ade-02, sub-ade-03, sub-ade-01, sub-ade, del-addeq-02, del-addeq-04, del-addeq-05, del-addeq-01, del-addeq-06, add-rem-sub, diff-sub-size, del-feq-02, del-feq-01, add-inter-rem, subseteq-rem-del, disjoint-rec2, diff-add-del, del-addeq, diff-del-plus-2, diff-del-plus-1, equal-add-in, diff-one, del-addin-01, size-union, k-delete-rec, intersection-insert, unadd-01, diff-del-02, del-feq, union-one, union-subset-02, k-intersect-rec1, one-in, unsubins-01, union-subset-04, union-subset-05, disjoint-rec, diff-subset-01, unsubins, forall-def, insdel-sub, delete-shift, delsw, disjoint-notempty-01,
• set-basic/Size-empty is used by union-size-03, diff-sub-size, size-union, union-size-le, intersection-size, del-three,
• set-basic/Size-insert is used by del-size, union-size-03, diff-sub-size, size-union, union-size-le, intersection-size, del-three,
• set-basic/Subset is used by int-subs01, subsub-del, unsub-union-01, unsub, sub-union-05, sub-union-02, sub-union-01, sub-union-04, sub-union-03, delete-subset, sub-union, union-sub-01, uneq, diff-subset, sub-ade-02, sub-ade-03, sub-ade-01, sub-ade, union-size-01, diff-sub-size, union-difference, diff-one, union-size, union-sizeeq, diff-del-01, diff-del-02, sub-del, unsubsub, sub-del-03, sub-del-04, sub-del-01, sub-del-02, sub-del-05, union-subset-02, diff-sub, union-subset-01, unsubins-01, union-subset-04, union-subset-03, union-subset-05, union-sizele, int-eq, diff-subset-01, unsubins, insdel-sub, selsub-diff,
• set-basic/add is used by filter-add,
• set-basic/eq is used by union-size-03, diff-sub-size, add-inter-rem, size-union,
• set-basic/eq-02 is used by del-three,
• set-basic/eq-03 is used by del-addeq-03, uninsert,
• set-basic/in-02 is used by filter-add, del-three,
• set-basic/in-04 is used by del-two, diff-one,
• set-basic/in-06 is used by del-three,
• set-basic/ne is used by filter-add, del-three,
• set-basic/ne-01 is used by del-two, rem-disjoint, unsub-union-01, disjointu-empty2, filter-add, union-size-ls-in, une-01, del-size, disjointu-empty, exists-def, union-size-03, union-size-02, subseteq-disjoint-empty, diff-sub-size, size-del-leq, add-inter-rem, subseteq-disjoint-empty-right, uninsubdel, disjoint-rec2, disjoint-all, del-size-01, size-rm-eq, disjoint-diff-subset, disjoint-diff, size-union, union-size-le, union-sizeeq, size-rm-less, intersection-size, intdel-empty, del-three, del-size-le, disjoint-rec, diff-subset-02, forall-def, disjoint-notempty-01, disjoint-01,
• set-basic/one-size is used by del-three,
• set-basic/size-ins is used by union-size-insert,
• set-basic/size-one-01 is used by del-three,
• set-basic/size-zero is used by filter-empty, filter-add, del-ne,
• set-basic/size-zero-01 is used by filter-empty, rem-disjoint, unsub-union-01, disjointu-empty2, filter-add, une-01, disjointu-empty, exists-def, subseteq-disjoint-empty, diff-sub-size, add-inter-rem, subseteq-disjoint-empty-right, disjoint-rec2, disjoint-all, size-rm-eq, disjoint-diff-subset, disjoint-diff, size-union, del-three, disjoint-rec, forall-def, disjoint-notempty-01, disjoint-01,
• set-basic/size-zero-02 is used by union-size-ls-in, union-size-02, diff-sub-size, size-del-leq, del-size-01, size-rm-less, del-three, del-size-le,
• 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-disjoint-empty, subseteq-disjoint-empty-right, uninsubdel, disjoint-diff-subset, diff-subset-02,
• set-basic/sub-ntrans is used by disjoint-diff-subset,

Used from specification nat-basic

• nat-basic/neq-01 is used by union-sizele,
• nat-basic/a is used by union-size-ls-in, union-size-not-less-01, union-size-not-less-02, del-size, union-size-03, union-size-02, diff-sub-size, size-del-leq, del-size-01, size-rm-eq, size-union, union-size-le, size-rm-less, intersection-size, del-three, del-size-le, union-size-insert,
• nat-basic/c is used by union-size-ls-in, union-size-not-less-01, union-size-not-less-02, del-size, union-size-03, union-size-02, diff-sub-size, size-del-leq, del-size-01, size-rm-eq, size-union, union-size-le, size-rm-less, intersection-size, del-three, del-size-le, union-size-insert,
• nat-basic/eq-01 is used by union-size-03, diff-sub-size, size-union,
• nat-basic/eq-02 is used by union-size-02, diff-sub-size, size-rm-eq,
• nat-basic/eqs is used by union-size-03,
• nat-basic/f is used by union-size-not-less, union-size-not-less-01, union-size-not-less-02, union-size-03, diff-sub-size, union-size, union-size-le, intersection-size, del-three, union-sizele,
• nat-basic/l is used by union-size-not-less-01, union-size-le, intersection-size,
• nat-basic/l-01 is used by diff-sub-size,
• nat-basic/l-02 is used by union-size-not-less-02, del-size-le,
• 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 union-size-02, diff-sub-size, size-del-leq, del-size-01, size-rm-less, del-size-le,
• nat-basic/refl-Nat is used by union-size-not-less-01, size-del-leq, union-size-le, size-rm-less, del-size-le, union-sizele,
• nat-basic/s-04 is used by size-rm-less,
• nat-basic/z-02 is used by union-size-03, diff-sub-size, size-union, union-size-le, intersection-size,