Used simplifier rules/spec theorems by specification

Used from specification array-copy

• array-copy/size-subarray is used by ar-elems-extract1,
• array-copy/subarray-elim is used by ar-elems-extract1,

Used from specification bag-basic

• bag-basic/count-insert is used by ar-elems-in-h,
• bag-basic/bag-add2-eq-elim is used by ar-elems-update-h,
• bag-basic/count-other is used by ar-elems-in-exists-h,
• bag-basic/count-same is used by ar-elems-in-h,
• bag-basic/insert-inj is used by ar-elems-update-h0, ar-elems-update-h, ar-elems-extract1, ar-elems-append-not-lower-h, ar-elems-append-lower-h,

Used from specification bag-union

• bag-union/in is used by ar-elems-in-h, ar-elems-in-exists-h,
• bag-union/bag-rm-add-eq is used by ar-elems-update-h,
• bag-union/del-empty is used by ar-elems-update-h,
• bag-union/del-rec is used by ar-elems-update-h,
• bag-union/in-emp is used by ar-elems-in-exists-h,
• bag-union/size-empty is used by ar-elems-size-h,
• bag-union/size-rec is used by ar-elems-size-h,
• bag-union/union-ass is used by ar-elems-extract1, ar-elems-append-not-lower-h, ar-elems-append,
• bag-union/union-com is used by ar-elems-extract1, ar-elems-append-not-lower-h, ar-elems-append,
• bag-union/union-empty is used by ar-elems-extract1, ar-elems-append-not-lower-h, ar-elems-append,
• bag-union/union-inj is used by ar-elems-append,
• bag-union/union-rec is used by ar-elems-extract1, ar-elems-append-not-lower-h,

Used from specification nat-basic1

• nat-basic1/f is used by ar-elems-update-h0, ar-elems-update-h, ar-elems-update, ar-elems-size-h, ar-elems-in-h, ar-elems-in-exists-h, ar-elems-in-exists, ar-elems-in, ar-elems-id-size1, ar-elems-extract1, ar-elems-append-not-lower-h, ar-elems-append-lower-h,
• nat-basic1/lf is used by ar-elems-update-h0, ar-elems-update-h, ar-elems-in-exists-h,
• nat-basic1/lf-01 is used by ar-elems-id-size1, ar-elems-extract1,
• nat-basic1/lf-02 is used by ar-elems-in-h, ar-elems-id-size1, ar-elems-append-not-lower-h,
• nat-basic1/ls-02 is used by ar-elems-in-exists-h, ar-elems-id-size1, ar-elems-extract1, ar-elems-append-not-lower-h,
• nat-basic1/ref-1 is used by ar-elems-size, ar-elems-in-exists-h, ar-elems-extract1, ar-elems-append-not-lower-h, ar-elems-append,
• nat-basic1/trans-1 is used by ar-elems-update-h0, ar-elems-in-exists-h,
• nat-basic1/zero is used by ar-elems1, ar-elems-append-not-lower-h,
• nat-basic1/zero-01 is used by ar-elems-update-h, ar-elems-in-h,

Used from specification array-splice

• array-splice/subarray-split-at is used by ar-elems-extract1,
• array-splice/subarray-split-first is used by ar-elems-extract1,
• array-splice/append-a is used by ar-elems-extract1, ar-elems-append-not-lower-h, ar-elems-append-lower-h, ar-elems-append,
• array-splice/append-at1 is used by ar-elems-append-lower-h,
• array-splice/append-atp2 is used by ar-elems-append-not-lower-h,
• array-splice/append-len is used by ar-elems-extract1, ar-elems-append-not-lower-h, ar-elems-append-lower-h, ar-elems-append,

Used from specification array

• array/Put-other is used by ar-elems-update-h,
• array/Put-same is used by ar-elems-update-h,
• array/Size-mkarray is used by ar-elems-extract1,
• array/Size-put is used by ar-elems-update-h0, ar-elems-update-h, ar-elems-update, ar-elems-extract1,
• array/cgetput is used by ar-elems-extract1,
• array/cngetput is used by ar-elems-update-h0,

Used from specification nat

• nat/add-01 is used by ar-elems-extract1,
• nat/anti is used by ar-elems-in-h,
• nat/ax-02 is used by ar-elems-append-not-lower-h, ar-elems-append,
• nat/elim-pred-c is used by ar-elems-extract1,
• nat/elim-sub is used by ar-elems-extract1, ar-elems-append-not-lower-h,
• nat/eq is used by ar-elems-extract1,
• nat/eq-01 is used by ar-elems-append,
• nat/eqle-one is used by ar-elems-extract1,
• nat/fle is used by ar-elems-update-h0, ar-elems-update-h, ar-elems-in-h, ar-elems-append-not-lower-h,
• nat/fle-01 is used by ar-elems-update-h0, ar-elems-append-lower-h,
• nat/le-add is used by ar-elems-update-h0, ar-elems-append,
• nat/le-ls-simp is used by ar-elems-update-h0, ar-elems-update-h, ar-elems-size-h, ar-elems-in-exists-h, ar-elems-append-not-lower-h, ar-elems-append-lower-h,
• nat/lels is used by ar-elems-update-h0, ar-elems-update-h, ar-elems-size-h, ar-elems-in-h, ar-elems-in-exists-h, ar-elems-extract1, ar-elems-append-not-lower-h, ar-elems-append-lower-h, ar-elems-append,
• nat/lels-01 is used by ar-elems-size, ar-elems-extract1, ar-elems-append-not-lower-h, ar-elems-append,
• nat/lels-02 is used by ar-elems-update-h,
• nat/lels-03 is used by ar-elems-update-h0, ar-elems-update-h, ar-elems-size-h, ar-elems-in-h, ar-elems-in-exists-h, ar-elems-extract1, ar-elems-append-not-lower-h, ar-elems-append-lower-h,
• nat/lep-02 is used by ar-elems-append-not-lower-h, ar-elems-append,
• nat/ler is used by ar-elems-update, ar-elems-in-exists, ar-elems-in, ar-elems-extract1,
• nat/ls-le-simp is used by ar-elems-in-h,
• nat/succ-01 is used by ar-elems-update-h0, ar-elems-update-h, ar-elems-size-h, ar-elems-in-h, ar-elems-in-exists-h, ar-elems-extract1, ar-elems-append-not-lower-h, ar-elems-append-lower-h,
• nat/zero-01 is used by ar-elems-extract1,

Used from specification nat-basic2

• nat-basic2/a is used by ar-elems1, ar-elems-update-h0, ar-elems-update-h, ar-elems-size-h, ar-elems-in-h, ar-elems-in-exists-h, ar-elems-extract1, ar-elems-append-not-lower-h, ar-elems-append-lower-h, ar-elems-append,
• nat-basic2/ax-08 is used by ar-elems-extract1, ar-elems-append-not-lower-h, ar-elems-append,
• nat-basic2/c is used by ar-elems1, ar-elems-update-h0, ar-elems-update-h, ar-elems-size-h, ar-elems-in-h, ar-elems-in-exists-h, ar-elems-extract1, ar-elems-append-not-lower-h, ar-elems-append-lower-h, ar-elems-append,
• nat-basic2/eq-01 is used by ar-elems-size-h, ar-elems-extract1,
• nat-basic2/l is used by ar-elems-extract1, ar-elems-append-not-lower-h,
• nat-basic2/l-01 is used by ar-elems-extract1, ar-elems-append-not-lower-h,
• nat-basic2/l-02 is used by ar-elems-extract1, ar-elems-append-lower-h,
• nat-basic2/oz is used by ar-elems-in-h, ar-elems-extract1, ar-elems-append-not-lower-h,
• nat-basic2/s is used by ar-elems-update-h, ar-elems-in-h, ar-elems-in-exists-h, ar-elems-extract1,
• nat-basic2/succ is used by ar-elems-update-h0, ar-elems-update-h, ar-elems-size-h, ar-elems-in-h, ar-elems-in-exists-h, ar-elems-append-not-lower-h, ar-elems-append-lower-h,
• nat-basic2/z-01 is used by ar-elems-in-h,