Used simplifier rules/spec theorems by specification

Used from specification set-union

• set-union/subdef is used by subseteq-rem-del, subseteq-inter-empty-empty, subdef,
• set-union/subdef is used by unsubsub, unsubins-01, unsubins, unsubdel, unsub-union-01, unsub, union-subset-05, union-subset-04, union-subset-03, union-subset-02, union-subset-01, union-sizele, union-sizeeq, union-difference, uneq, subsub-del, sub-union-05, sub-union-02, sub-del-04, sub-del-02, sub-del, sub-ade-03, sub-ade-02, sub-ade-01, sub-ade, selsub-diff, int-subs01, int-eq, insdel-sub, diff-subset-01, diff-subset, diff-sub-size, diff-sub, diff-one, diff-del-02, delete-subset,

Used from specification nat

• nat/elim-sub is used by diff-sub-size,
• nat/add-01 is used by union-size-03, del-size-01, del-size,
• 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-03, diff-sub-size,
• nat/eq-02 is used by union-size-02, diff-sub-size, del-size-01,
• nat/fle is used by union-sizele, union-size-not-less-02, union-size-not-less-01,
• 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,
• nat/lels is used by union-size-ls-in, diff-sub-size,
• nat/lels-01 is used by union-sizele, union-size-not-less-02, union-size-ls-in, union-size-le, union-size-03, union-size-02, size-del-leq, diff-sub-size, del-size-01,
• nat/lep-02 is used by union-size-ls-in,
• nat/ler is used by size-del-leq, diff-sub-size,
• nat/lez is used by diff-sub-size,
• nat/ls-02 is used by union-size-ls-in, size-del-leq,
• nat/ls-add-not-01 is used by union-size-not-less-01,
• nat/ls-le-simp is used by union-size-not-less,
• nat/sub-base is used by union-size-03,
• nat/succ-01 is used by size-del-leq, diff-sub-size,

Used from specification set-basic

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

Used from specification nat-basic2

• nat-basic2/a is used by union-size-not-less-02, union-size-not-less-01, union-size-ls-in, union-size-le, union-size-insert, union-size-03, union-size-02, size-union, size-del-leq, intersection-size, diff-sub-size, del-three, del-size-01, del-size,
• nat-basic2/add-base is used by union-size-le, union-size-03, del-size-01, del-size,
• nat-basic2/c is used by union-size-not-less-02, union-size-not-less-01, union-size-ls-in, union-size-le, union-size-insert, union-size-03, union-size-02, size-union, size-del-leq, intersection-size, diff-sub-size, del-three, del-size-01, del-size,
• nat-basic2/eq is used by union-size-02, diff-sub-size,
• nat-basic2/eq-01 is used by union-size-03, size-union, diff-sub-size,
• nat-basic2/eqs is used by union-size-03,
• nat-basic2/l is used by union-size-le, intersection-size,
• nat-basic2/l-01 is used by diff-sub-size,
• nat-basic2/l-02 is used by union-size-not-less-02,
• nat-basic2/nls-fst is used by union-size-le, intersection-size,
• nat-basic2/oz is used by union-size-le, intersection-size, del-three,
• nat-basic2/z is used by size-union, diff-sub-size,

Used from specification nat-basic1

• nat-basic1/neq-01 is used by union-sizele,
• nat-basic1/f is used by union-sizele, union-size-not-less-02, union-size-not-less-01, union-size-not-less, union-size-le, union-size, intersection-size, diff-sub-size, del-three,
• nat-basic1/lf-01 is used by diff-sub-size, del-three,
• nat-basic1/one is used by del-three, del-ne,
• nat-basic1/one-01 is used by union-size-02, size-del-leq, diff-sub-size, del-size-01,
• nat-basic1/ref-1 is used by union-sizele, union-size-le, size-del-leq,