Used simplifier rules/spec theorems by specification

Used from specification int-basic1

• int-basic1/l is used by short-2bytes,
• int-basic1/lsrec is used by int2bytes-first-zerobyte-01,
• int-basic1/trans is used by short-2bytes, no-leading-zero-01,
• int-basic1/forward-pos is used by short-2bytes-03, short-2bytes-01, short-2bytes, rightshift-8-01, no-leading-zero-01, no-leading-zero, int2bytes-rec-pos-any, int2bytes-rec-pos-04, int2bytes-rec-pos-03, int2bytes-rec-pos-02, int2bytes-rec-pos-01, int2bytes-rec-case, int2bytes-one-01, int2bytes-minus-one, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-ls-01, int2bytes-leading-zeros, int2bytes-last-01, int2bytes-index-rightshift, int2bytes-first-zerobyte-01, int2bytes-first-zerobyte, int2bytes-butlast, getInt-theorem, bytes2int-int2bytes-len-eq, bytes2int-2-le-32767, bits2int-pos, band-65535-pos,
• int-basic1/irref is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-len-neg-01,
• int-basic1/lf-01 is used by int2bytes-rec-pos, int2bytes-le255,
• int-basic1/ls-01 is used by rightshift-8-01-01, rightshift-8-01, no-leading-zero-04, int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-04, int2bytes-rec-neg-03, int2bytes-rec-neg-02, int2bytes-rec-neg-01, int2bytes-rec-case, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-ls-01, int2bytes-le255, int2bytes-last-01, int2bytes-index-rightshift-02, int2bytes-index-rightshift, int2bytes-first-zerobyte-01, int2bytes-first-zerobyte, int2bytes-byte-neg, int2bytes-butlast, bytes2int-len-one-02, bytes2int-len-one-01, bytes2int-int2bytes-len-eq, bytes2int-first-pos,
• int-basic1/lst is used by no-leading-zero-01, int2bytes-one, int2bytes-minus-one, int2bytes-leading-zeros, int2bytes-first-zerobyte, int2bytes-first-neg-01, int2bytes-first-neg, bytes2int-int2bytes-len-eq,
• int-basic1/lst-01 is used by rightshift-8-01-01, rightshift-8-01, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-03, int2bytes-rec-neg-02, int2bytes-minus-one,
• int-basic1/minus-one is used by rightshift-8-01, no-leading-zero-01,
• int-basic1/numlsf is used by short-2bytes, setInt-theorem, no-leading-zero-04, no-leading-zero-01, int2bytes-zero, int2bytes-rec255-neg, int2bytes-rec-pos-any, int2bytes-rec-pos-04, int2bytes-rec-neg-256-01, int2bytes-rec-neg-256, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-03, int2bytes-rec-neg-02, int2bytes-rec-case, int2bytes-one-02, int2bytes-minus-one, int2bytes-len-one-01, int2bytes-len-one, int2bytes-len-neg256, int2bytes-len-le-neg-03, int2bytes-len-le-neg-01, int2bytes-last-01, int2bytes-first-neg-01, int2bytes-first-neg, int2bytes-fillsgn-rec, int2bytes-byte-neg, int2bytes-butlast, bytes2int-int2bytes-len-eq, bits2int-pos,
• int-basic1/numlslsdel is used by setInt-theorem, rightshift-8-02, rightshift-8-01, rightshift-8, no-leading-zero-04, no-leading-zero-01, int2bytes-rec255-neg, int2bytes-rec-case, int2bytes-len-one-01, int2bytes-len-one, int2bytes-last-01, int2bytes-first-neg-01, int2bytes-first-neg, int2bytes-fillsgn-rec, int2bytes-byte-neg, int2bytes-byte, int2bytes-butlast, bytes2int-int2bytes-len-eq,
• int-basic1/numlslsdel-01 is used by short-2bytes-03, short-2bytes-01, short-2bytes, rightshift-8-01, no-leading-zero-01, no-leading-zero, int2bytes-rec-pos-any, int2bytes-rec-pos-04, int2bytes-rec-pos-03, int2bytes-rec-pos-02, int2bytes-rec-pos-01, int2bytes-one-01, int2bytes-one, int2bytes-leading-zeros, int2bytes-last-01, int2bytes-first-zerobyte, bytes2int-int2bytes-len-eq, bytes2int-2-le-32767, bits2int-pos,
• int-basic1/trans is used by int2bytes-rec-pos,
• int-basic1/two-ls is used by rightshift-8-01, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-first-zerobyte-01,

Used from specification int-mult

• int-mult/commutativity is used by int2bytes-first-neg, bytes2int-neg, bytes2int-int2bytes-len-eq,
• int-mult/dist-rsplit is used by no-leading-zero-01, bytes2int-size-06, bytes2int-size-03, bytes2int-100x-03, bytes2int-011x-02, bytes2int-011x,
• int-mult/ls-add is used by no-leading-zero,
• int-mult/modeqp-01 is used by bytes2int-int2bytes-len-eq,
• int-mult/modeqp-copied is used by int2bytes-first-zerobyte-01, bytes2int-int2bytes-len-eq, bytes2int-diff,
• int-mult/modlep is used by bytes2int-size-07, bytes2int-size-06, bytes2int-size-02,
• int-mult/modlep-01 is used by bytes2int-size, bytes2int-2-le-32767,
• int-mult/modlsp is used by int2bytes-len-pos-01, int2bytes-len-neg-01, int2bytes-first-zerobyte-01,
• int-mult/modlsp-02 is used by int2bytes-len-le-neg-02, int2bytes-len-le-neg, int2bytes-len-le, bytes2int-size-05, bytes2int-size-04, bytes2int-size-03, bytes2int-size-01,
• int-mult/modlsp-03 is used by int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-first-zerobyte-01,
• int-mult/modzero is used by bytes2int-int2bytes-len-eq,
• int-mult/modzero-01 is used by bytes2int-zero-03,
• int-mult/modzero-03 is used by int2bytes-first-neg, bytes2int-neg, bytes2int-len-one-01, bytes2int-int2bytes-len-eq,
• int-mult/numls-12 is used by no-leading-zero-01,
• int-mult/zero-ge is used by rightshift-8-01-01,
• int-mult/zero-ls is used by rightshift-8-01-01, int2bytes-rec-neg-03,
• int-mult/Mult-zero is used by rightshift-8-01-01, no-leading-zeros, int2bytes-rec-neg-06, int2bytes-rec-neg-04, int2bytes-rec-neg-03, int2bytes-len-pos-01, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-le-neg-02, int2bytes-len-le-neg, int2bytes-len-le, int2bytes-first-zerobyte-01, bytes2int-size-03, bytes2int-size-01, byte2bits-val,
• int-mult/abs-eqall is used by rightshift-8-01-01, rightshift-8-01, int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-len-pos,
• int-mult/add-mult-two is used by int2bytes-rec-neg-06, int2bytes-rec-neg-03,
• int-mult/associativity is used by short-2bytes-03, short-2bytes, rightshift-8-01-01, rightshift-8-01, rightshift-8, no-leading-zeros, no-leading-zero-04, no-leading-zero-01, no-leading-zero, int2bytes-rec-pos-any, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-04, int2bytes-rec-neg-03, int2bytes-rec-neg-02, int2bytes-rec-neg-01, int2bytes-not-neg, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-le-neg, int2bytes-len-le-01, int2bytes-len-le, int2bytes-len-eq-pos, int2bytes-leading-zeros, int2bytes-last-01, int2bytes-index-rightshift-02, int2bytes-first-zerobyte-01, int2bytes-first-zerobyte, int2bytes-first-neg-01, int2bytes-first-neg, getInt-theorem, bytes2int-zero-03, bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-04, bytes2int-size-03, bytes2int-size-02, bytes2int-size-01, bytes2int-size, bytes2int-rec-first-zero, bytes2int-rec, bytes2int-neg, bytes2int-mklist-zeros-01, bytes2int-mklist-zeros, bytes2int-mklist-mones-01, bytes2int-len-one-02, bytes2int-len-one-01, bytes2int-int2bytes-len-eq, bytes2int-i2b, bytes2int-first-pos, bytes2int-diff, bytes2int-append, bytes2int-1011x, bytes2int-100x-03, bytes2int-100x-02, bytes2int-100x-01, bytes2int-100x, bytes2int-011x-02, bytes2int-011x-01, bytes2int-011x, byte2bits-val,
• int-mult/commutativity is used by short-2bytes-03, short-2bytes, rightshift-8-01-01, rightshift-8-01, rightshift-8, no-leading-zeros, no-leading-zero-04, no-leading-zero-01, no-leading-zero, int2bytes-rec-pos-any, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-04, int2bytes-rec-neg-03, int2bytes-rec-neg-02, int2bytes-rec-neg-01, int2bytes-not-neg, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-upper, int2bytes-len-ls-neg-03, int2bytes-len-ls-neg-02, int2bytes-len-ls-neg-01, int2bytes-len-ls-neg, int2bytes-len-ls-01, int2bytes-len-ls, int2bytes-len-le-upper, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-le-neg, int2bytes-len-le-01, int2bytes-len-le, int2bytes-len-eq-pos, int2bytes-len-eq-neg-01, int2bytes-len-eq-neg, int2bytes-leading-zeros, int2bytes-last-01, int2bytes-index-rightshift-02, int2bytes-index-rightshift-01, int2bytes-first-zerobyte-01, int2bytes-first-zerobyte, int2bytes-first-neg-01, int2bytes-first-neg, getInt-theorem, bytes2int-zero-03, bytes2int-size-val-07, bytes2int-size-val-06, bytes2int-size-val-05, bytes2int-size-val-04, bytes2int-size-val-03, bytes2int-size-val-02, bytes2int-size-val-01, bytes2int-size-val, bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-04, bytes2int-size-03, bytes2int-size-02, bytes2int-size-01, bytes2int-size, bytes2int-rec-first-zero, bytes2int-rec-bor, bytes2int-rec-01, bytes2int-rec, bytes2int-neg, bytes2int-mklist-zeros-01, bytes2int-mklist-zeros, bytes2int-mklist-mones-01, bytes2int-len-one-02, bytes2int-len-one-01, bytes2int-int2bytes-len-eq, bytes2int-i2b, bytes2int-first-pos, bytes2int-diff, bytes2int-append, bytes2int-2-le-32767, bytes2int-1011x, bytes2int-100x-03, bytes2int-100x-02, bytes2int-100x-01, bytes2int-100x, bytes2int-011x-02, bytes2int-011x-01, bytes2int-011x, bytes2bits-nls, bytes2bits-nle, byte2bits-val,
• int-mult/dist-rmerge is used by bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-04, bytes2int-rec-first-zero, bytes2int-1011x, bytes2int-100x-03, bytes2int-100x-02, bytes2int-011x-02,
• int-mult/eq-dist is used by getInt-theorem, bytes2int-rec-first-zero, bytes2int-rec, bytes2int-append,
• int-mult/eq-pos is used by getInt-theorem, bytes2int-size-07, bytes2int-size-05, bytes2int-size-04, bytes2int-size-02, bytes2int-size-01, bytes2int-size, bytes2int-rec-first-zero, bytes2int-mklist-zeros-01, bytes2int-mklist-mones-01, bytes2int-diff, bytes2int-1011x, bytes2int-100x-02, bytes2int-011x-01, bytes2int-011x,
• int-mult/eq-succ is used by bytes2int-int2bytes-len-eq,
• int-mult/le-dist-01 is used by int2bytes-len-pos,
• int-mult/le-one is used by int2bytes-rec-neg-06, int2bytes-rec-neg-03,
• int-mult/le-pos is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-len-le-neg-03, int2bytes-len-le-neg-01, int2bytes-len-eq-pos,
• int-mult/le-same is used by int2bytes-not-neg, int2bytes-leading-zeros, int2bytes-first-zerobyte,
• int-mult/ls-add-03 is used by int2bytes-len-pos,
• int-mult/ls-dist is used by no-leading-zero-01, int2bytes-len-pos-01, int2bytes-len-neg,
• int-mult/ls-pos is used by int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-le-neg, int2bytes-len-le-01, int2bytes-len-le, int2bytes-len-eq-pos,
• int-mult/ls-same-01 is used by int2bytes-leading-zeros,
• int-mult/minus-left is used by rightshift-8-01, bytes2int-rec, bytes2int-append,
• int-mult/minus-one-01 is used by int2bytes-rec-neg-06, int2bytes-rec-neg-03,
• int-mult/modzero-01 is used by int2bytes-first-zerobyte-01, bytes2int-int2bytes-len-eq,
• int-mult/numabs is used by int2bytes-rec-pos-any,
• int-mult/numeq-04 is used by no-leading-zero-04,
• int-mult/numle-12 is used by int2bytes-first-neg-01, int2bytes-first-neg,
• int-mult/numls-01 is used by int2bytes-len-pos-01, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-first-zerobyte-01,
• int-mult/numls-02 is used by rightshift-8-01-01, int2bytes-len-le-neg-02, int2bytes-len-le-neg, int2bytes-len-le, bytes2int-size-03, bytes2int-size-01,
• int-mult/numls-03 is used by bytes2int-size-05, bytes2int-int2bytes-len-eq,
• int-mult/numls-04 is used by bytes2int-size-07, bytes2int-size-06,
• int-mult/numls-12 is used by bytes2int-size-07, bytes2int-size-06,
• int-mult/one is used by rightshift-8, int2bytes-rec-neg-03, bytes2int-append,
• int-mult/one-01 is used by int2bytes-rec-pos-any, bytes2int-int2bytes-len-eq,
• int-mult/pred-rmerge is used by rightshift-8-01,
• int-mult/succ-rmerge is used by rightshift-8-01-01, no-leading-zero-01, int2bytes-rec-neg-03, int2bytes-first-neg-01, int2bytes-first-neg, getInt-theorem, bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-04, bytes2int-size-03, bytes2int-size-02, bytes2int-size-01, bytes2int-size, bytes2int-mklist-mones-01, bytes2int-int2bytes-len-eq, bytes2int-1011x, bytes2int-100x-03, bytes2int-100x-02, bytes2int-100x-01, bytes2int-100x, bytes2int-011x-02, bytes2int-011x-01, bytes2int-011x, byte2bits-val,
• int-mult/zero-eq is used by rightshift-8-01-01, int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-04, int2bytes-rec-neg-02, int2bytes-rec-neg-01, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-first-zerobyte-01, bytes2int-mklist-zeros, bytes2int-mklist-mones-01, bytes2int-100x-03, bytes2int-100x-02,
• int-mult/zero-ge is used by rightshift-8-01-01, int2bytes-rec-pos-any, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-04, int2bytes-rec-neg-03, int2bytes-rec-neg-02, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-le-neg, int2bytes-len-le, int2bytes-len-eq-pos, int2bytes-index-rightshift-02, int2bytes-first-zerobyte-01, int2bytes-first-neg-01, getInt-theorem, bytes2int-size-06, bytes2int-size-05, bytes2int-size-03, bytes2int-size, bytes2int-neg, bytes2int-int2bytes-len-eq, bytes2int-append, bytes2int-100x-03, bytes2int-100x-01, bytes2int-011x-02, bytes2int-011x,
• int-mult/zero-ge-01 is used by rightshift-8-01-01,
• int-mult/zero-ge-add is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-len-ls-01, int2bytes-first-zerobyte-01, getInt-theorem,
• int-mult/zero-gr is used by rightshift-8-01-01, no-leading-zero-04, int2bytes-rec-pos-any, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-03, int2bytes-rec-neg-02, int2bytes-rec-neg-01, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-len-le-neg-03, int2bytes-len-le-neg-01, int2bytes-len-le-01, int2bytes-len-le, int2bytes-len-eq-pos, int2bytes-first-zerobyte-01, getInt-theorem, bytes2int-zero-03, bytes2int-size-07, bytes2int-size-04, bytes2int-size-02, bytes2int-size-01, bytes2int-int2bytes-len-eq, bytes2int-1011x, bytes2int-100x-02, bytes2int-100x, bytes2int-011x-01,
• int-mult/zero-ls is used by short-2bytes, rightshift-8, no-leading-zero-01, int2bytes-rec-pos-any, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-03, int2bytes-len-pos, int2bytes-len-neg, int2bytes-first-zerobyte-01, int2bytes-first-neg-01, getInt-theorem, bytes2int-int2bytes-len-eq, bytes2int-first-pos,
• int-mult/zero-ls-03 is used by rightshift-8-01-01,
• int-mult/zero-neq-01 is used by no-leading-zero-04, int2bytes-rec-pos-any, int2bytes-rec-neg-04, int2bytes-rec-neg-01, bytes2int-zero-03,

Used from specification nat

• nat/add-01 is used by fix-bits2bytes-01,
• nat/add-03 is used by int2bytes-len-def, bits2bytes-len-02, bits2bytes-app,
• nat/l-num-05 is used by band-65535-pos,
• nat/le-num-06 is used by bits2bytes-app,
• nat/lels is used by int2bytes-len-ls-neg-03, int2bytes-len-ls-neg-02, int2bytes-len-ls-neg-01, int2bytes-len-ls-neg,
• nat/lels-01 is used by int2bytes-len-ls-upper, int2bytes-len-le-upper,
• nat/num-02 is used by int2bytes-rec-pos-any, int2bytes-len-ls-01,
• nat/prop is used by int2bytes-rec-pos-any, fix-bits2bytes-01,
• nat/prop-01 is used by rightshift-8-01-01, int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02,
• nat/prop-07 is used by int2bytes-rec-neg-05, int2bytes-rec-neg-02,
• nat/shift is used by int2bytes-rec-neg-05, int2bytes-rec-neg-02, bits2bytes-len,
• nat/shift-01 is used by fix-bits2bytes-01, fix-bits2bytes,
• nat/sub-add is used by fix-bits2bytes-01, bits2bytes-fill,
• nat/sub-same is used by int2bytes-index-rightshift,
• nat/sub-succ is used by rightshift-8-01, int2bytes-rec-pos-any, bits2bytes-fill,
• nat/zero-02 is used by int2bytes-rec-pos-any, fix-bits2bytes-01,
• nat/add-01 is used by rightshift-8-01-01, rightshift-8-01, int2bytes-rec-pos-any, int2bytes-rec-pos, int2bytes-rec-neg-05, int2bytes-rec-neg-04, int2bytes-rec-neg-02, int2bytes-rec-neg-01, int2bytes-len-pos, int2bytes-len-neg, int2bytes-len-def, int2bytes-index-rightshift, fix-bits2bytes, fillsgn-rec, fillsgn-butlast, bytes2int-size-val, bytes2bytes-zero, bytes2bytes-other, bytes2bytes-mone, bytes2bytes-fix, bits2bytes-rec-02, bits2bytes-2pot,
• nat/add-num-01 is used by int2bytes-rec-neg-05, int2bytes-len-pos-01, int2bytes-len-neg-01, bits2bytes-len-01, bits2bytes-2pot,
• nat/add-num-03 is used by no-leading-zero-03, int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-len-neg-01, int2bytes-byte, fix-bits2bytes, bytes2int-size-07, bytes2int-size-05, bytes2int-size-01, bytes2int-size, bytes2int-rec-first-zero, bytes2int-len-one-02, bytes2bytes-fix, bits2bytes-rec-02, bits2bytes-fill, bits2bytes-app,
• nat/add-num-04 is used by setShort-theorem-01, setInt-theorem, int2bytes-rec255-neg, fix2rest-last, bytes2int-int2bytes-len-eq,
• nat/anti is used by setInt-theorem, int2bytes-rec-pos, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-len-le-neg-02, fix-value, fix-pos-le, fix-neg-le, fix-bits2bytes-01, fillsgn-short, fillsgn-length-02, bytes2int-fillsgn-zero, bytes2bytes-identity-01, bits2bytes-mklist-03, bits2bytes-app,
• nat/cancel-01 is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-fillsgn-rec, fix-rec-pos, fix-rec-neg, fix-bits2bytes-01, fillsgn-rec,
• nat/elim-pred-c is used by int2bytes-rec-pos-any, int2bytes-fillsgn-rec, fix-rec-pos, fix-rec-neg, fix-bits2bytes, fillsgn-rec, bytes2int-fillsgn-zero,
• nat/elim-sub is used by int2bytes-index-rightshift-02, int2bytes-index-rightshift, int2bytes-byte, fix2rest-last, fix-value, fix-rec-pos, fix-rec-neg, fix-bits2bytes-01, fix-bits2bytes, fillsgn-rec, fillsgn-fix, byte2bits-val, bits2bytes-rec-02,
• nat/eq is used by int2bytes-rec-neg-05, bytes2int-fillsgn-zero,
• nat/eq-01 is used by rightshift-8-01-01, fillsgn-rec, fillsgn-fix, bits2bytes-rec-01, bits2bytes-mklist-03,
• nat/eq-02 is used by int2bytes-rec-pos-any, int2bytes-rec-pos, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-len-def, fix-bits2bytes-01, fix-bits2bytes, fillsgn-butlast, bits2bytes-len-01, bits2bytes-fill,
• nat/eq-03 is used by fix-bits2bytes-01,
• nat/eqle-one is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-len-ls-01, int2bytes-len-le-neg, int2bytes-len-le, int2bytes-fillsgn-rec, fix-bits2bytes-01, fix-bits2bytes,
• nat/fle is used by int2bytes-rec-pos-any, int2bytes-rec-pos, int2bytes-len-pos, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-len-le-neg-03, int2bytes-len-le, int2bytes-index-rightshift, fix-bits2bytes, fillsgn-short, fillsgn-butlast, bytes2bytes-length, band-65535-pos,
• nat/fle-01 is used by int2bytes-rec-pos, int2bytes-len-le-neg-01, int2bytes-len-le-neg, int2bytes-len-le, int2bytes-len-def, bits2int-pos, bits2bytes-len-02, bits2bytes-fill, bits2bytes-app,
• nat/ge is used by setShort-theorem, setInt-theorem, rightshift-8-02, rightshift-8-01-01, int2int-fillsgn, int2bytes-rec255-neg, int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-fillsgn-rec, fix2rest-last, fix-value, fix-pos-le, fix-one-01, fix-neg-le, fix-length-01, fix-length, fix-last, fix-empty, fix-butlast, fix-bits2bytes-01, fillsgn-short, fillsgn-rec, fillsgn-not-empty, fillsgn-length-03, fillsgn-length, fillsgn-empty, fillsgn-butlast, bytes2bytes-fillsgn,
• nat/l-num-01 is used by int2bytes-rec-pos-any, bits2bytes-fill,
• nat/l-num-03 is used by bits2bytes-2pot,
• nat/l-num-04 is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, bytes2bytes-zero, bits2int-pos, bits2bytes-rec-02,
• nat/l-num-05 is used by fix2rest-last, bits2bytes-rec-01,
• nat/l-num-06 is used by fix-rec-pos, fix-rec-neg,
• nat/le is used by int2bytes-rec-pos-any, int2bytes-rec-pos, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-len-eq-pos, bits2bytes-fill,
• nat/le-add is used by rightshift-8-01-01, rightshift-8-01, int2bytes-len-neg-01, int2bytes-len-le-01, int2bytes-index-rightshift-02, int2bytes-index-rightshift, fillsgn-rec, bytes2int-fillsgn-zero,
• nat/le-ls-simp is used by rightshift-8-01-01, rightshift-8-01, int2int-fillsgn, int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-len-ls-01, int2bytes-len-le-neg-03, int2bytes-len-le-neg-01, int2bytes-len-le-neg, int2bytes-len-le-01, int2bytes-len-eq-pos, int2bytes-index-rightshift-02, int2bytes-index-rightshift, fix2rest-last, fix-butlast, fix-bits2bytes, fillsgn-rec, fillsgn-butlast, bytes2int-fillsgn-zero, bytes2bytes-fillsgn, bits2int-pos, bits2bytes-mklist-03, bits2bytes-mklist-02, bits2bytes-mklist, bits2bytes-app, band-65535-pos, band-65535-neg,
• nat/le-num-01 is used by int2bytes-len-neg-01, bits2bytes-rec-02,
• nat/le-num-02 is used by bytes2bytes-identity, bytes2bytes-fix,
• nat/le-num-03 is used by bits2bytes-2pot,
• nat/le-num-04 is used by no-leading-zero-03, int2bytes-rec-pos,
• nat/le-num-05 is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, fix2rest-last, bits2int-pos, bits2bytes-rec-02,
• nat/lels is used by setInt-theorem, rightshift-8-02, rightshift-8-01-01, rightshift-8-01, int2int-fillsgn, int2bytes-rec255-neg, int2bytes-rec-pos-any, int2bytes-rec-pos, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-upper, int2bytes-len-ls-01, int2bytes-len-ls, int2bytes-len-le-upper, int2bytes-len-le-neg, int2bytes-len-le-01, int2bytes-len-le, int2bytes-len-eq-neg-01, int2bytes-len-eq-neg, int2bytes-len-def, int2bytes-le255, int2bytes-index-rightshift-02, int2bytes-index-rightshift-01, int2bytes-index-rightshift, int2bytes-first-zerobyte, int2bytes-fillsgn-rec, int2bytes-empty, int2bytes-bytes2int-length-01, fix-rec-pos, fix-rec-neg, fix-length, fix-butlast-longer, fix-butlast, fix-bits2bytes-01, fix-bits2bytes, fillsgn-short, fillsgn-rec, fillsgn-length-02, fillsgn-length, fillsgn-fix, fillsgn-empty, fillsgn-butlast, bytes2int-fillsgn-zero, bytes2bytes-zero, bytes2bytes-other, bytes2bytes-mone, bytes2bytes-length, bytes2bytes-fix, bits2int-pos, bits2bytes-rec-02, bits2bytes-mklist-03, bits2bytes-mklist-02, bits2bytes-mklist, bits2bytes-len-02, bits2bytes-len, bits2bytes-fill, bits2bytes-app, bits2bits-sgn, bits2bits-inj, bits2bits-in, band-65535-pos,
• nat/lels-01 is used by setShort-theorem-01, setShort-theorem, setInt-theorem, rightshift-8-02, rightshift-8-01-01, rightshift-8-01, int2int-fillsgn, int2bytes-rec255-neg, int2bytes-rec-pos-any, int2bytes-rec-pos, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-minus-one, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-neg-02, int2bytes-len-ls-neg, int2bytes-len-ls-04, int2bytes-len-ls-03, int2bytes-len-ls-01, int2bytes-len-ls, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-le-neg, int2bytes-len-le-01, int2bytes-len-le, int2bytes-len-eq-pos, int2bytes-len-eq-neg-01, int2bytes-len-eq-neg, int2bytes-len-def, int2bytes-le127, int2bytes-index-rightshift-02, int2bytes-index-rightshift, int2bytes-first-zerobyte, int2bytes-fillsgn-rec, int2bytes-byte-neg, int2bytes-byte, fix2rest-last, fix-value, fix-rec-pos, fix-rec-neg, fix-one-01, fix-length-01, fix-length, fix-last, fix-empty, fix-butlast-longer, fix-butlast, fix-bits2bytes-01, fix-bits2bytes, fillsgn-short, fillsgn-rec, fillsgn-not-empty, fillsgn-length-03, fillsgn-length, fillsgn-len-short, fillsgn-fix, fillsgn-empty, fillsgn-butlast, bytes2int-zero-06, bytes2int-len-one-01, bytes2int-first-pos, bytes2bytes-zero, bytes2bytes-other, bytes2bytes-mone, bytes2bytes-length, bytes2bytes-fillsgn, byte2bits-val, byte2bits-length, bits2int-pos, bits2bytes-rec-02, bits2bytes-rec-01, bits2bytes-mklist-03, bits2bytes-mklist-02, bits2bytes-mklist-01, bits2bytes-mklist, bits2bytes-len-02, bits2bytes-len-01, bits2bytes-len, bits2bytes-fill, bits2bytes-empty, bits2bytes-app, bits2bits-sgn, bits2bits-inj, bits2bits-in, band-65535-neg,
• nat/lels-02 is used by setInt-theorem, int2bytes-rec255-neg, int2bytes-rec-pos-any, int2bytes-rec-pos, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-len-neg-01, int2bytes-len-le-neg-03, int2bytes-len-le-neg-01, int2bytes-len-le-01, int2bytes-len-eq-pos, int2bytes-byte-neg, fix2rest-last, fix-value, fix-pos-le, fix-neg-le, fix-butlast-longer, fix-butlast, fix-bits2bytes-01, fix-bits2bytes, fillsgn-butlast, bits2bytes-app, bits2bits-sgn, bits2bits-inj, bits2bits-in,
• nat/lels-03 is used by setShort-theorem, setInt-theorem, rightshift-8-01-01, int2bytes-rec-pos-any, int2bytes-rec-pos, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-index-rightshift, int2bytes-byte, fix2rest-last, fix-value, fix-rec-pos, fix-rec-neg, fix-bits2bytes-01, fix-bits2bytes, fillsgn-short, fillsgn-fix, bits2bytes-rec-02, bits2bytes-mklist-02, bits2bytes-mklist-01, bits2bytes-mklist, bits2bytes-fill, bits2bytes-app,
• nat/lep is used by no-leading-zero-03, int2bytes-rec-pos-any, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-le-neg-02, int2bytes-index-rightshift-02, int2bytes-index-rightshift, fillsgn-rec, bits2bytes-rec-02, bits2bytes-mklist-02, bits2bytes-mklist, bits2bytes-fill,
• nat/lep-01 is used by int2bytes-rec-pos-any, int2bytes-rec-pos, int2bytes-rec-neg-05, int2bytes-rec-neg-02, fix-bits2bytes-01, fix-bits2bytes, fillsgn-fix, bytes2bytes-zero, bytes2bytes-other, bytes2bytes-mone, bytes2bytes-identity, bytes2bytes-fix, bits2bytes-rec-02, bits2bytes-mklist, bits2bytes-len, bits2bytes-fill, bits2bytes-app, bits2bits-sgn, bits2bits-inj, bits2bits-in,
• nat/lep-02 is used by int2bytes-rec-pos-any, int2bytes-rec-pos, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-len-le-neg, int2bytes-len-le, int2bytes-len-eq-pos, int2bytes-fillsgn-rec, fix-bits2bytes-01, fix-bits2bytes, fillsgn-rec, bits2bytes-fill,
• nat/leprf is used by int2bytes-len-eq-pos,
• nat/ler is used by int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-ls-01, int2bytes-len-le-neg, int2bytes-len-le, int2bytes-len-eq-neg-01, int2bytes-len-eq-neg, int2bytes-fillsgn-rec, fix-length-01, fix-bits2bytes-01, fix-bits2bytes, fillsgn-short, fillsgn-rec, bytes2bytes-identity-01,
• nat/les is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-len-pos, int2bytes-len-ls-01, int2bytes-len-le-neg, int2bytes-len-le, int2bytes-fillsgn-rec, fix-bits2bytes-01, fix-bits2bytes,
• nat/let is used by rightshift-8-01, int2bytes-rec-pos-any, int2bytes-rec-pos, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-eq-pos, int2bytes-index-rightshift-02, fix-bits2bytes, fillsgn-short, bytes2int-fillsgn-zero, bytes2bytes-fix, bits2bytes-len,
• nat/lez is used by int2bytes-len-le-01, int2bytes-index-rightshift-02, int2bytes-index-rightshift-01, fix-empty, bytes2int-zero-05,
• nat/lez-01 is used by rightshift-8-01-01, int2bytes-len-ls-01, int2bytes-len-le-neg-03, fillsgn-not-empty, fillsgn-empty,
• nat/ls is used by int2bytes-len-neg, int2bytes-fillsgn-rec, fix-rec-pos, fix-rec-neg, fix-bits2bytes-01, fix-bits2bytes, bits2bytes-rec-02,
• nat/ls-01 is used by rightshift-8-01, int2bytes-rec-pos-any, int2bytes-len-ls-01, int2bytes-len-le-01, int2bytes-len-def, fix-butlast-longer, fix-butlast, fix-bits2bytes-01, fix-bits2bytes, fillsgn-butlast, bytes2int-zero-06, bytes2int-first-pos, bits2bytes-mklist-02, bits2bytes-mklist, bits2bytes-len-02, bits2bytes-len, bits2bytes-app, bits2bits-sgn, bits2bits-inj, bits2bits-in,
• nat/ls-02 is used by rightshift-8-01, int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-len-ls-01, int2bytes-len-le-neg-03, int2bytes-len-le-neg-01, int2bytes-len-le-01, int2bytes-len-eq-pos, fix-butlast, fix-bits2bytes-01, fix-bits2bytes, fillsgn-butlast, bits2bytes-len,
• nat/ls-03 is used by int2bytes-rec-pos-any, int2bytes-index-rightshift, int2bytes-fillsgn-rec, int2bytes-byte-neg, fix-bits2bytes-01, fillsgn-butlast, bits2bytes-rec-02, bits2bytes-mklist-02, bits2bytes-mklist, bits2bytes-fill,
• nat/ls-le-simp is used by int2bytes-rec255-neg, int2bytes-rec-pos-any, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-le127, int2bytes-index-rightshift-01, int2bytes-fillsgn-rec, int2bytes-bytes2int-length-01, fix-rec-pos, fix-rec-neg, fix-length, fix-butlast-longer, fix-butlast, fix-bits2bytes-01, fix-bits2bytes, fillsgn-short, fillsgn-length, fillsgn-fix, fillsgn-empty, fillsgn-butlast, bits2int-pos,
• nat/not-zero is used by setShort-theorem-01, setInt-theorem, rightshift-8-02, rightshift-8-01, no-leading-zero-03, int2bytes-rec255-neg, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-le-neg, int2bytes-len-le, int2bytes-len-eq-pos, int2bytes-len-def, int2bytes-first-zerobyte, fix2rest-last, fix-bits2bytes-01, fillsgn-short, bits2bytes-rec-02, bits2bytes-len-02, bits2bytes-len-01, bits2bytes-len, bits2bytes-app, bits2bits-sgn,
• nat/one-02 is used by int2bytes-len-le-neg-01, bits2bytes-rec-02, bits2bytes-mklist-02, bits2bytes-mklist,
• nat/pred-03 is used by int2bytes-rec-pos-any, int2bytes-rec-pos, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-le-neg, int2bytes-len-le-01, int2bytes-len-le, int2bytes-len-eq-pos, int2bytes-len-def, int2bytes-index-rightshift, int2bytes-first-zerobyte, int2bytes-fillsgn-rec, fix2rest-last, fix-rec-pos, fix-rec-neg, fix-last, fillsgn-rec, bytes2bytes-fix,
• nat/prop-07 is used by int2bytes-rec-pos-any, fix-length, fix-bits2bytes-01, fix-bits2bytes, fillsgn-length, bits2bytes-fill,
• nat/sub-base is used by rightshift-8-01-01, rightshift-8-01, int2bytes-index-rightshift-02, fillsgn-empty,
• nat/sub-ls is used by int2bytes-len-le-01, int2bytes-len-le, int2bytes-len-eq-pos, fix-bits2bytes-01,
• nat/succ-01 is used by rightshift-8-01, int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-len-ls, int2bytes-len-le-neg-03, int2bytes-len-eq-pos, int2bytes-index-rightshift, int2bytes-fillsgn-rec, fix-rec-pos, fix-rec-neg, fix-butlast, fix-bits2bytes-01, fix-bits2bytes, fillsgn-butlast,
• nat/zero is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, fix-bits2bytes-01, bytes2int-fillsgn-zero,
• nat/zero-01 is used by rightshift-8-01-01, int2bytes-rec-pos-any, int2bytes-index-rightshift, fix-butlast-longer, fix-bits2bytes-01, fix-bits2bytes, bits2bytes-mklist-02, bits2bytes-mklist, bits2bytes-len, bits2bytes-fill, bits2bytes-app, bits2bits-sgn, bits2bits-inj, bits2bits-in,
• nat/zero-02 is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, fix2rest-last, fix-pos-le, fix-neg-le, fix-bits2bytes-01, fix-bits2bytes, bits2bits-sgn, bits2bits-in,

Used from specification int-pot

• int-pot/lemon2pot-02 is used by band-65535-neg,
• int-pot/ls-pos is used by band-65535-pos,
• int-pot/ls-pos-2pot is used by int2bytes-len-neg-01, int2bytes-len-le-neg-03, int2bytes-len-le-neg-01, int2bytes-first-zerobyte-01, int2bytes-byte,
• int-pot/ls-pos-2pot-01 is used by int2bytes-byte,
• int-pot/mod2-2pot-05 is used by int2bytes-rec-pos-any,
• int-pot/mod2-pos is used by int2bytes-rec-pos-any,
• int-pot/pot-dist-pos is used by bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-04, bytes2int-size-03, bytes2int-size-02, bytes2int-size-01, bytes2int-size, bytes2int-1011x, bytes2int-100x-03, bytes2int-100x-02, bytes2int-100x-01, bytes2int-100x, bytes2int-011x-02, bytes2int-011x-01, bytes2int-011x, byte2bits-val,
• int-pot/pot-pot is used by bytes2int-append,
• int-pot/succ is used by bytes2int-rec-first-zero,
• int-pot/two-le is used by int2bytes-len-neg,
• int-pot/two-zero is used by rightshift-8-01-01, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-04, int2bytes-rec-neg-03, int2bytes-rec-neg-02,
• int-pot/zero is used by int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-03, int2bytes-rec-neg-02,
• int-pot/2pot-leone is used by int2bytes-rec-neg-06, int2bytes-rec-neg-03, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-le-neg-03, int2bytes-len-eq-pos, int2bytes-first-zerobyte-01,
• int-pot/abs-2pot is used by rightshift-8-01-01, int2bytes-rec-neg-06, int2bytes-rec-neg-03,
• int-pot/eq-one is used by int2bytes-len-neg-01, int2bytes-len-neg,
• int-pot/ls-pos-2pot-01 is used by rightshift-8-01-01, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-le-neg, int2bytes-len-le-01, int2bytes-len-le, int2bytes-len-eq-pos, int2bytes-first-zerobyte-01, int2bytes-byte,
• int-pot/pot2-ls-pred is used by rightshift-8-01-01, int2bytes-rec-neg-05, int2bytes-len-pos-01, int2bytes-len-neg-01, int2bytes-len-ls-01, int2bytes-len-le-neg-03, int2bytes-len-le-neg-01, int2bytes-len-eq-pos, int2bytes-first-zerobyte-01,
• int-pot/pot2-pos is used by rightshift-8-01-01, int2bytes-rec-pos-any, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-03, int2bytes-rec-neg-02, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-len-le-neg-01, int2bytes-len-le-01, int2bytes-len-le, int2bytes-len-eq-pos, int2bytes-first-zerobyte-01, int2bytes-byte, bytes2int-append, band-65535-pos,
• int-pot/pot2-pos-01 is used by int2bytes-rec-neg-06, int2bytes-rec-neg-03, int2bytes-len-pos, int2bytes-len-ls-01, band-65535-pos,
• int-pot/two-lez-01 is used by int2bytes-rec-pos-any, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-03, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg, int2bytes-first-zerobyte-01,
• int-pot/two-lsz is used by rightshift-8-01-01, int2bytes-rec-pos-any, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-04, int2bytes-rec-neg-03, int2bytes-rec-neg-02, int2bytes-len-pos-01, int2bytes-len-neg-01,
• int-pot/two-zero is used by int2bytes-rec-neg-04,

Used from specification int-abs

• int-abs/Abs-neg is used by no-leading-zero-04, no-leading-zero-01, int2bytes-rec-neg-06, int2bytes-rec-neg-03, int2bytes-first-neg-01, int2bytes-first-neg,
• int-abs/Abs-pos is used by rightshift-8-01, bytes2int-size, bytes2int-int2bytes-len-eq, bytes2int-2-le-32767,
• int-abs/add-rew is used by rightshift-8-01-01,
• int-abs/add-shift is used by int2bytes-len-neg,
• int-abs/discard-add2-lels-left is used by bytes2int-len-one-02,
• int-abs/elim-sub is used by bytes2int-int2bytes-len-eq,
• int-abs/forward-lsle is used by int2bytes-len-neg-01, bytes2bytes-first-pos,
• int-abs/le-rew-succ is used by no-leading-zero-01, no-leading-zero,
• int-abs/lels-02 is used by int2bytes-len-le,
• int-abs/les is used by no-leading-zero-04,
• int-abs/mone-07 is used by int2bytes-rec-neg-06, int2bytes-rec-neg-03,
• int-abs/mone-08 is used by int2bytes-rec-neg-05, int2bytes-rec-neg-02,
• int-abs/neg-08 is used by int2bytes-byte,
• int-abs/ple-02 is used by bytes2int-len-one-01,
• int-abs/sub-ls is used by bytes2int-int2bytes-len-eq,
• int-abs/sub-ls-01 is used by int2bytes-rec255-neg,
• int-abs/zero-ge-01 is used by int2bytes-first-neg-01,
• int-abs/zero-gs is used by bytes2int-neg,
• int-abs/Abs-pos is used by rightshift-8-01, no-leading-zero-04, no-leading-zero-01, int2bytes-rec-neg-06, int2bytes-rec-neg-03, int2bytes-first-neg-01, int2bytes-first-neg,
• int-abs/Sub-def is used by rightshift-8, int2bytes-rec-pos, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-03, int2bytes-len-pos-01, int2bytes-len-neg-01, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-le-neg, int2bytes-len-le-01, int2bytes-len-le, int2bytes-len-eq-pos, int2bytes-le255, int2bytes-last-01, int2bytes-first-zerobyte-01, bytes2int-size-val-02, bytes2int-size-val, bytes2int-size-07, bytes2int-size-04, bytes2int-size-02, bytes2int-size-01, bytes2int-rec, bytes2int-int2bytes-len-eq, bytes2int-1011x, bytes2int-100x-02, bytes2int-011x-01,
• int-abs/abs-03 is used by rightshift-8-01-01, bytes2int-size, bytes2int-int2bytes-len-eq, bytes2int-2-le-32767,
• int-abs/abs-05 is used by int2bytes-rec-neg-06, int2bytes-rec-neg-03, bytes2int-append, band-65535-neg,
• int-abs/abs-06 is used by rightshift-8-01-01, rightshift-8-01, bytes2int-size, bytes2int-int2bytes-len-eq, bytes2int-2-le-32767,
• int-abs/abs-08 is used by rightshift-8-02, rightshift-8-01-01, rightshift-8-01, rightshift-8, no-leading-zero-04, no-leading-zero-01, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-03, int2bytes-last-01, int2bytes-first-neg-01, int2bytes-first-neg, int2bytes-butlast, bytes2int-int2bytes-len-eq, bytes2int-append, band-65535-neg,
• int-abs/abs-10 is used by rightshift-8-01,
• int-abs/abs-16 is used by no-leading-zero-01, int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-not-neg, int2bytes-len-ls-01, int2bytes-leading-zeros, int2bytes-first-zerobyte,
• int-abs/absle is used by rightshift-8-02, rightshift-8-01-01, rightshift-8-01, int2bytes-len-pos, int2bytes-len-neg-01, bytes2int-int2bytes-len-eq, bytes2int-append, band-65535-pos,
• int-abs/absls-06 is used by bytes2int-int2bytes-len-eq,
• int-abs/abssub is used by rightshift-8-01,
• int-abs/anti is used by rightshift-8-02, rightshift-8-01-01, rightshift-8-01, rightshift-8, no-leading-zero-04, no-leading-zero, int2bytes-rec-neg-06, int2bytes-rec-neg-03, int2bytes-rec-case, int2bytes-one, int2bytes-len-pos, int2bytes-len-one-01, int2bytes-len-one, int2bytes-last-01, int2bytes-index-rightshift-02, int2bytes-first-zerobyte-01, int2bytes-first-neg-01, int2bytes-first-neg, int2bytes-butlast, bytes2int-zero-03, bytes2int-size-05, bytes2int-size-04, bytes2int-size-03, bytes2int-size-01, bytes2int-int2bytes-len-eq,
• int-abs/bet-01 is used by int2bytes-first-zerobyte-01,
• int-abs/elim-sub is used by no-leading-zero-01, int2bytes-leading-zeros, int2bytes-last-01, int2bytes-first-neg-01, int2bytes-first-neg, bytes2int-int2bytes-len-eq, byte2bits-val,
• int-abs/forward-le is used by short-2bytes-01, setInt-theorem, rightshift-8-02, rightshift-8, no-leading-zero-04, int2bytes-rec255-neg, int2bytes-rec-pos-any, int2bytes-rec-pos-04, int2bytes-rec-pos-03, int2bytes-rec-case, int2bytes-one, int2bytes-not-neg, int2bytes-len-pos, int2bytes-len-one-01, int2bytes-len-one, int2bytes-len-neg-01, int2bytes-last-01, int2bytes-index-rightshift-02, int2bytes-fillsgn-rec, int2bytes-butlast, getInt-theorem, bytes2int-size, bytes2int-int2bytes-len-eq, bytes2int-first-pos, bytes2int-2-le-32767, band-65535-pos,
• int-abs/forward-le-01 is used by short-2bytes-02, short-2bytes-01, setShort-theorem, setInt-theorem, rightshift-8-02, rightshift-8-01-01, rightshift-8-01, rightshift-8, no-leading-zero-04, no-leading-zero-01, no-leading-zero, int2bytes-rec255-neg, int2bytes-rec-pos-any, int2bytes-rec-pos-04, int2bytes-rec-pos-03, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-03, int2bytes-rec-neg-02, int2bytes-rec-case, int2bytes-one, int2bytes-not-neg-01, int2bytes-not-neg, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-one-01, int2bytes-len-one, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-upper, int2bytes-len-ls-04, int2bytes-len-ls-03, int2bytes-len-ls-01, int2bytes-len-ls, int2bytes-len-le-upper, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-le-neg, int2bytes-len-le-01, int2bytes-len-le, int2bytes-len-eq-pos, int2bytes-leading-zeros, int2bytes-le127, int2bytes-last-01, int2bytes-index-rightshift-02, int2bytes-index-rightshift, int2bytes-first-zerobyte-01, int2bytes-first-zerobyte, int2bytes-first-neg-01, int2bytes-first-neg, int2bytes-first, int2bytes-fillsgn-rec, int2bytes-byte, int2bytes-butlast, getInt-theorem, fix2rest-last, fix-value, fix-rec-pos, fix-rec-neg, fix-pos-le, fix-length, fix-last, fix-butlast-longer, fillsgn-short, fillsgn-rec, fillsgn-length, fillsgn-len-short, fillsgn-fix, fillsgn-butlast, bytes2int-zero-04, bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-04, bytes2int-size, bytes2int-rec, bytes2int-neg-01, bytes2int-neg, bytes2int-mklist-zeros-01, bytes2int-len-one-02, bytes2int-len-one-01, bytes2int-leading-zero, bytes2int-int2bytes-len-eq, bytes2int-ge-zero, bytes2int-first-pos-01, bytes2int-first-pos, bytes2int-first-neq, bytes2int-first-lez, bytes2int-first-gez, bytes2int-diff, bytes2int-append, bytes2int-2-le-32767, bytes2bytes-mone, bytes2bytes-length, bytes2bytes-identity, bytes2bytes-fix, bytes2bytes-first-pos, bytes2bytes-first-neg, bits2int-pos, bits2bits-sgn, band-65535-pos, band-65535-neg,
• int-abs/forward-le-02 is used by setInt-theorem, rightshift-8-02, rightshift-8-01-01, rightshift-8-01, rightshift-8, no-leading-zero-04, no-leading-zero-03, no-leading-zero-01, no-leading-zero, int2bytes-rec255-neg, int2bytes-rec-pos-any, int2bytes-rec-pos-04, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-04, int2bytes-rec-neg-03, int2bytes-rec-neg-02, int2bytes-rec-neg-01, int2bytes-one, int2bytes-not-neg, int2bytes-len-pos-01, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-neg, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-le-neg, int2bytes-len-eq-neg, int2bytes-leading-zeros, int2bytes-first-zerobyte-01, int2bytes-first-neg-01, int2bytes-first-neg, int2bytes-fillsgn-rec, int2bytes-byte, fix2rest-last, fix-value, fix-rec-pos, fix-rec-neg, fix-neg-le, fix-butlast-longer, fillsgn-rec, fillsgn-len-short, fillsgn-fix, fillsgn-empty, fillsgn-butlast, bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-04, bytes2int-size-01, bytes2int-size, bytes2int-pos, bytes2int-neg-01, bytes2int-neg, bytes2int-mone, bytes2int-mklist-mones-01, bytes2int-len-one-02, bytes2int-len-one-01, bytes2int-le-zero, bytes2int-int2bytes-len-eq, bytes2int-ge-zero, bytes2int-first-pos-01, bytes2int-first-pos, bytes2int-first-neq, bytes2int-first-lez, bytes2int-first-gez, bytes2int-diff, bytes2int-append, bytes2bytes-zero, bytes2bytes-mone, bytes2bytes-length, bytes2bytes-identity, bytes2bytes-fix, bytes2bytes-first-pos, bytes2bytes-first-neg, bytes2bits-nls, bits2int-pos, bits2int-neg, bits2bits-sgn, band-65535-neg,
• int-abs/forward-le-03 is used by int2bytes-rec-case, int2bytes-last-01, int2bytes-butlast, bytes2bytes-mone,
• int-abs/forward-le-04 is used by rightshift-8-01-01, rightshift-8, no-leading-zero-04, no-leading-zero-01, no-leading-zero, int2bytes-rec-pos-any, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-03, int2bytes-rec-case, int2bytes-one, int2bytes-minus-one, int2bytes-len-pos, int2bytes-len-one-01, int2bytes-len-one, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-le, int2bytes-last-01, int2bytes-first-neg-01, int2bytes-first-neg, int2bytes-butlast, bytes2int-zero-03, bytes2int-size-05, bytes2int-size-04, bytes2int-int2bytes-len-eq, bytes2int-first-pos, bytes2bytes-mone, band-65535-neg,
• int-abs/forward-le-05 is used by short-2bytes-03, short-2bytes-01, short-2bytes, setInt-theorem, rightshift-8-01-01, rightshift-8-01, no-leading-zero-01, no-leading-zero, int2bytes-rec-pos-any, int2bytes-rec-pos-03, int2bytes-rec-pos-02, int2bytes-rec-pos-01, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-04, int2bytes-rec-neg-03, int2bytes-rec-neg-02, int2bytes-rec-neg-01, int2bytes-one-01, int2bytes-not-neg, int2bytes-minus-one, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-len-le-01, int2bytes-len-le, int2bytes-len-eq-pos, int2bytes-leading-zeros, int2bytes-last-01, int2bytes-index-rightshift-02, int2bytes-index-rightshift, int2bytes-first-zerobyte-01, int2bytes-first-zerobyte, int2bytes-first, int2bytes-byte, getInt-theorem, bytes2int-zero-03, bytes2int-size-07, bytes2int-size-06, bytes2int-size-03, bytes2int-size-02, bytes2int-len-one-02, bytes2int-le-zero, bytes2int-int2bytes-len-eq, bytes2int-first-pos, bytes2int-append, bytes2int-2-le-32767, bytes2bytes-zero, bytes2bytes-first-neg, bits2int-pos,
• int-abs/forward-lele is used by rightshift-8-02, no-leading-zero-04, no-leading-zero-01, no-leading-zero, int2bytes-zero, int2bytes-rec-pos-any, int2bytes-rec-pos-04, int2bytes-rec-pos, int2bytes-rec-neg-05, int2bytes-rec-case, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-le, int2bytes-le255, int2bytes-first-neg-01, int2bytes-first-neg, bytes2int-len-one-01, bits2int-pos, bits2bits-sgn, bits2bits-in, band-65535-neg,
• int-abs/forward-lels is used by setInt-theorem, rightshift-8-02, rightshift-8-01-01, rightshift-8-01, no-leading-zero-04, no-leading-zero-01, int2bytes-rec255-neg, int2bytes-rec-pos-any, int2bytes-rec-pos, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-03, int2bytes-rec-case, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-one, int2bytes-len-neg256, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-len-le-neg-03, int2bytes-len-le-neg-01, int2bytes-len-le-01, int2bytes-len-le, int2bytes-len-eq-pos, int2bytes-leading-zeros, int2bytes-last-01, int2bytes-first-zerobyte-01, int2bytes-first-neg-01, int2bytes-first-neg, int2bytes-fillsgn-rec, int2bytes-byte, int2bytes-butlast, getInt-theorem, bytes2int-zero-03, bytes2int-len-one-02, bytes2int-len-one-01, bytes2int-int2bytes-len-eq, bits2bits-sgn, band-65535-pos, band-65535-neg,
• int-abs/forward-lsle is used by setInt-theorem, rightshift-8-01-01, rightshift-8-01, no-leading-zero-04, no-leading-zero-01, no-leading-zero, int2bytes-rec255-neg, int2bytes-rec-pos-any, int2bytes-rec-pos-04, int2bytes-rec-pos, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-03, int2bytes-rec-neg-02, int2bytes-not-neg, int2bytes-minus-one, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-le-neg, int2bytes-le255, int2bytes-last-01, int2bytes-index-rightshift-02, int2bytes-first-zerobyte-01, int2bytes-first-neg-01, int2bytes-first-neg, int2bytes-first, int2bytes-fillsgn-rec, int2bytes-byte, fix-rec-pos, fix-rec-neg, fillsgn-butlast, bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-04, bytes2int-neg-01, bytes2int-neg, bytes2int-len-one-02, bytes2int-len-one-01, bytes2int-int2bytes-len-eq, bytes2int-ge-zero, bytes2int-first-pos-01, bytes2int-first-pos, bytes2int-first-neq, bytes2int-first-lez, bytes2int-first-gez, bytes2int-diff, bytes2int-append, bytes2bytes-mone, bytes2bytes-first-pos, bytes2bytes-first-neg, bits2int-pos, bits2bits-sgn, band-65535-neg,
• int-abs/gr-def is used by int2bytes-first-zerobyte-01,
• int-abs/le-add is used by int2bytes-rec-pos-any, int2bytes-len-neg-01, int2bytes-len-neg,
• int-abs/le-add-02 is used by int2bytes-len-pos,
• int-abs/le-add-03 is used by no-leading-zero-04,
• int-abs/lels is used by short-2bytes, setShort-theorem, setInt-theorem, rightshift-8-02, rightshift-8-01-01, rightshift-8-01, rightshift-8, no-leading-zero-04, no-leading-zero-03, no-leading-zero-01, no-leading-zero, int2bytes-zero, int2bytes-rec255-neg, int2bytes-rec-shift, int2bytes-rec-pos-any, int2bytes-rec-pos-04, int2bytes-rec-pos, int2bytes-rec-neg-256-01, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-03, int2bytes-rec-neg-02, int2bytes-rec-case, int2bytes-one, int2bytes-not-neg, int2bytes-minus-one, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-one-01, int2bytes-len-one, int2bytes-len-neg256, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-upper, int2bytes-len-ls-neg-03, int2bytes-len-ls-neg-02, int2bytes-len-ls-neg-01, int2bytes-len-ls-neg, int2bytes-len-ls-04, int2bytes-len-ls-03, int2bytes-len-ls-01, int2bytes-len-le-upper, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-le-neg, int2bytes-len-le-01, int2bytes-len-le, int2bytes-len-eq-pos, int2bytes-len-eq-neg-01, int2bytes-len-eq-neg, int2bytes-leading-zeros, int2bytes-le255, int2bytes-last-01, int2bytes-index-rightshift-02, int2bytes-index-rightshift, int2bytes-first-zerobyte-01, int2bytes-first-zerobyte, int2bytes-first-neg-01, int2bytes-first-neg, int2bytes-fillsgn-rec, int2bytes-byte-neg, int2bytes-byte-01, int2bytes-byte, int2bytes-butlast, getInt-theorem, fix2rest-last, fix-value, fix-rec-neg, fix-neg-le, fix-length, fix-last, fix-butlast-longer, fillsgn-short, fillsgn-rec, fillsgn-length, fillsgn-len-short, fillsgn-fix, fillsgn-empty, fillsgn-butlast, bytes2int-zero-03, bytes2int-size-val-04, bytes2int-size-val-03, bytes2int-size-val-01, bytes2int-size-val, bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-04, bytes2int-size-03, bytes2int-size-02, bytes2int-size-01, bytes2int-size, bytes2int-rec-bor, bytes2int-rec, bytes2int-range, bytes2int-pos, bytes2int-neg-01, bytes2int-neg, bytes2int-mone, bytes2int-len-one-02, bytes2int-len-one-01, bytes2int-int2bytes-len-eq, bytes2int-ge-zero, bytes2int-first-pos, bytes2int-first-neq, bytes2int-first-lez, bytes2int-diff, bytes2int-append, bytes2int-2-le-32767, bytes2bytes-zero, bytes2bytes-mone, bytes2bytes-length, bytes2bytes-identity, bytes2bytes-fix, bytes2bytes-first-neg, bytes2bits-nls, byte2bits-val, byte2bits-first, bits2int-zero-ls, bits2int-pos, bits2int-neg, bits2bits-sgn, band-65535-pos, band-65535-neg,
• int-abs/lels-01 is used by short-2bytes-01, short-2bytes, setShort-theorem, setInt-theorem, rightshift-8-02, rightshift-8-01-01, rightshift-8-01, rightshift-8, no-leading-zero-04, no-leading-zero-01, no-leading-zero, int2bytes-zero, int2bytes-rec255-neg, int2bytes-rec-shift, int2bytes-rec-pos-any, int2bytes-rec-pos-04, int2bytes-rec-pos-03, int2bytes-rec-pos-02, int2bytes-rec-pos, int2bytes-rec-neg-05, int2bytes-rec-neg-04, int2bytes-rec-neg-02, int2bytes-rec-neg-01, int2bytes-rec-case, int2bytes-one-02, int2bytes-one-01, int2bytes-one, int2bytes-not-neg-01, int2bytes-minus-one, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-one-01, int2bytes-len-one, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-upper, int2bytes-len-ls-neg-03, int2bytes-len-ls-neg-02, int2bytes-len-ls-neg-01, int2bytes-len-ls-neg, int2bytes-len-ls-04, int2bytes-len-ls-03, int2bytes-len-ls-01, int2bytes-len-ls, int2bytes-len-le-upper, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-le-neg, int2bytes-len-le-01, int2bytes-len-le, int2bytes-len-eq-pos, int2bytes-len-eq-neg-01, int2bytes-len-eq-neg, int2bytes-leading-zeros, int2bytes-le255, int2bytes-last-01, int2bytes-last, int2bytes-index-rightshift-02, int2bytes-index-rightshift, int2bytes-first-zerobyte-01, int2bytes-first-zerobyte, int2bytes-first-neg-01, int2bytes-first-neg, int2bytes-first, int2bytes-fillsgn-rec, int2bytes-byte-neg, int2bytes-byte-01, int2bytes-byte, int2bytes-butlast, getInt-theorem, fix2rest-last, fix-value, fix-rec-pos, fix-pos-le, fix-length, fix-last, fix-butlast-longer, fillsgn-short, fillsgn-rec, fillsgn-length, fillsgn-len-short, fillsgn-fix, fillsgn-empty, fillsgn-butlast, bytes2int-size-val-05, bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-04, bytes2int-size-03, bytes2int-size-02, bytes2int-size-01, bytes2int-size, bytes2int-rec-bor, bytes2int-range, bytes2int-pos, bytes2int-neg, bytes2int-len-one-02, bytes2int-len-one-01, bytes2int-le-zero, bytes2int-int2bytes-len-eq, bytes2int-ge-zero, bytes2int-first-pos-01, bytes2int-first-pos, bytes2int-first-lez, bytes2int-first-gez, bytes2int-diff, bytes2int-append, bytes2int-2-le-32767, bytes2bytes-mone, bytes2bytes-length, bytes2bytes-identity, bytes2bytes-fix, bytes2bytes-first-pos, bytes2bytes-first-neg, bytes2bits-nle, byte2bits8, byte2bits-first, bits2int-zero-ls, bits2int-pos, bits2bits-sgn, bits2bits-in, band-65535-neg,
• int-abs/lels-02 is used by rightshift-8-01-01, rightshift-8-01, no-leading-zero-04, int2bytes-rec-pos-any, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-04, int2bytes-rec-neg-03, int2bytes-rec-neg-02, int2bytes-rec-neg-01, int2bytes-rec-case, int2bytes-one, int2bytes-len-pos, int2bytes-len-one-01, int2bytes-len-one, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-last-01, int2bytes-index-rightshift-02, int2bytes-index-rightshift, int2bytes-first-zerobyte-01, int2bytes-first-zerobyte, int2bytes-first-neg-01, int2bytes-first-neg, int2bytes-first, int2bytes-butlast, bytes2int-len-one-01, bytes2int-le-zero, bytes2int-int2bytes-len-eq, bytes2int-first-pos,
• int-abs/lels-03 is used by short-2bytes, rightshift-8-02, rightshift-8-01-01, rightshift-8-01, rightshift-8, no-leading-zero-04, no-leading-zero-03, no-leading-zero-01, no-leading-zero, int2bytes-rec255-neg, int2bytes-rec-shift, int2bytes-rec-pos-any, int2bytes-rec-neg-256-01, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-03, int2bytes-rec-case, int2bytes-one-02, int2bytes-one-01, int2bytes-one, int2bytes-not-neg, int2bytes-minus-one, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-one-01, int2bytes-len-one, int2bytes-len-neg256, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-neg-02, int2bytes-len-ls-neg-01, int2bytes-len-ls-neg, int2bytes-len-ls-01, int2bytes-len-ls, int2bytes-len-le-upper, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg, int2bytes-len-le-01, int2bytes-len-eq-neg-01, int2bytes-len-eq-neg, int2bytes-le255, int2bytes-last-01, int2bytes-index-rightshift, int2bytes-first-zerobyte-01, int2bytes-first-neg-01, int2bytes-first-neg, int2bytes-byte-neg, int2bytes-butlast, fix2rest-last, fix-rec-neg, fix-neg-le, fix-butlast-longer, fillsgn-rec, fillsgn-len-short, fillsgn-fix, fillsgn-empty, fillsgn-butlast, bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-04, bytes2int-size-03, bytes2int-size-02, bytes2int-size-01, bytes2int-size, bytes2int-range, bytes2int-pos, bytes2int-neg-01, bytes2int-neg, bytes2int-mone, bytes2int-len-one-02, bytes2int-int2bytes-len-eq, bytes2int-ge-zero, bytes2int-first-neq, bytes2int-first-lez, bytes2int-first-gez, bytes2int-append, bytes2bytes-zero, bytes2bytes-fix, bytes2bytes-first-neg, bytes2bits-nls, bits2int-zero-ls, bits2int-neg, bits2bits-sgn,
• int-abs/lels-04 is used by short-2bytes-02, setShort-theorem, rightshift-8-02, rightshift-8-01-01, rightshift-8-01, rightshift-8, no-leading-zero-04, no-leading-zero-01, no-leading-zero, int2bytes-rec-shift, int2bytes-rec-pos-any, int2bytes-rec-pos, int2bytes-rec-case, int2bytes-one, int2bytes-not-neg-01, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-one-01, int2bytes-len-one, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-upper, int2bytes-len-ls-neg-03, int2bytes-len-ls-neg-02, int2bytes-len-ls-neg, int2bytes-len-ls-04, int2bytes-len-ls-03, int2bytes-len-ls-01, int2bytes-len-ls, int2bytes-len-le-upper, int2bytes-len-le-neg-03, int2bytes-len-le-neg-01, int2bytes-len-le-01, int2bytes-len-le, int2bytes-len-eq-pos, int2bytes-len-eq-neg-01, int2bytes-len-eq-neg, int2bytes-leading-zeros, int2bytes-le255, int2bytes-last-01, int2bytes-last, int2bytes-index-rightshift-02, int2bytes-first-zerobyte-01, int2bytes-first-zerobyte, int2bytes-first-neg, int2bytes-first, int2bytes-butlast, fix2rest-last, fix-value, fix-rec-pos, fix-pos-le, fix-length, fix-last, fix-butlast-longer, fillsgn-short, fillsgn-rec, fillsgn-length, fillsgn-len-short, fillsgn-fix, fillsgn-butlast, bytes2int-zero-04, bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-02, bytes2int-size, bytes2int-rec, bytes2int-range, bytes2int-pos, bytes2int-neg-01, bytes2int-neg, bytes2int-len-one-01, bytes2int-int2bytes-len-eq, bytes2int-ge-zero, bytes2int-first-pos-01, bytes2int-first-pos, bytes2int-first-neq, bytes2int-first-lez, bytes2int-first-gez, bytes2bytes-mone, bytes2bytes-fix, bytes2bytes-first-pos, bytes2bytes-first-neg, bytes2bits-nle, byte2bits-first, bits2int-zero-ls, bits2bits-sgn, band-65535-neg,
• int-abs/lenls is used by int2bytes-byte,
• int-abs/leone is used by rightshift-8-01-01, rightshift-8-01, no-leading-zero-04, int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-le-neg, int2bytes-len-le-01, int2bytes-len-le, int2bytes-len-eq-pos, int2bytes-index-rightshift-02, int2bytes-first-zerobyte-01, bytes2int-size-07, bytes2int-size-04, bytes2int-size-02, bytes2int-size-01, bytes2int-1011x, bytes2int-100x-02, bytes2int-100x, bytes2int-011x-01,
• int-abs/lep is used by int2bytes-index-rightshift-02, int2bytes-index-rightshift,
• int-abs/lep-01 is used by rightshift-8-01, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-03, int2bytes-len-neg,
• int-abs/ler is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-len-pos-01, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-first-zerobyte-01,
• int-abs/les is used by int2bytes-len-pos-01, int2bytes-len-neg,
• int-abs/lsone is used by no-leading-zero-04, int2bytes-rec-neg-06, int2bytes-first-zerobyte-01, bytes2int-size-03, bytes2int-len-one-02, bytes2int-len-one-01, bytes2int-int2bytes-len-eq,
• int-abs/minus-02 is used by rightshift-8-01, no-leading-zero-04,
• int-abs/minus-add is used by short-2bytes, no-leading-zero-04, int2bytes-rec-neg-06, int2bytes-rec-neg-03, int2bytes-len-pos-01, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-len-le-neg-03, int2bytes-len-le-neg-01, int2bytes-first-zerobyte-01, int2bytes-first-neg, int2bytes-byte, bytes2int-size-07, bytes2int-rec, bits2int-pos,
• int-abs/minus-ass is used by bytes2int-rec, bytes2int-append,
• int-abs/minus-sub is used by int2bytes-rec-neg-06, int2bytes-rec-neg-03,
• int-abs/mone-05 is used by rightshift-8-01-01, no-leading-zero-01, no-leading-zero, int2bytes-leading-zeros, bytes2int-int2bytes-len-eq, bytes2int-append,
• int-abs/mone-06 is used by short-2bytes, rightshift-8-01, rightshift-8, int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-minus-one, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-len-le, int2bytes-len-eq-pos, int2bytes-first-zerobyte-01, int2bytes-first-neg-01, int2bytes-first-neg, getInt-theorem, bytes2int-size-07, bytes2int-size-04, bytes2int-size-02, bytes2int-size-01, bytes2int-int2bytes-len-eq, bytes2int-append, bytes2int-1011x, bytes2int-100x-02, bytes2int-100x, bytes2int-011x-01,
• int-abs/mone-08 is used by rightshift-8-01-01, no-leading-zero-04, int2bytes-rec-neg-06, int2bytes-rec-neg-03, int2bytes-len-neg, int2bytes-byte-neg, bytes2int-size-06, bytes2int-int2bytes-len-eq,
• int-abs/neg is used by bits2int-pos,
• int-abs/neg-01 is used by no-leading-zero-04,
• int-abs/neg-03 is used by bytes2int-size-val-05, bytes2int-size-val-04, bits2int-2pot,
• int-abs/neg-05 is used by rightshift-8-01-01, int2bytes-rec-neg-06, int2bytes-rec-neg-03, int2bytes-len-neg, bytes2int-append,
• int-abs/neg-06 is used by rightshift-8-01-01, no-leading-zero-04, no-leading-zero-01, int2bytes-rec-neg-06, int2bytes-rec-neg-03, int2bytes-len-neg, int2bytes-first-neg-01, int2bytes-first-neg, bytes2int-append,
• int-abs/neg-07 is used by rightshift-8-01-01, no-leading-zero-04, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-04, int2bytes-rec-neg-03, int2bytes-rec-neg-02, int2bytes-rec-neg-01, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-neg-03, int2bytes-len-ls-neg-02, int2bytes-len-ls-neg-01, int2bytes-len-ls-neg, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-le-neg, int2bytes-len-eq-neg-01, int2bytes-len-eq-neg, int2bytes-byte, bytes2int-size-07, bytes2int-size-06, bits2int-pos,
• int-abs/neg-12 is used by bytes2int-size-val-07,
• int-abs/neg-13 is used by rightshift-8-02, rightshift-8-01-01, rightshift-8-01, rightshift-8, no-leading-zero-04, no-leading-zero-01, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-03, int2bytes-len-neg-01, int2bytes-first-neg-01, int2bytes-first-neg, int2bytes-butlast, bytes2int-int2bytes-len-eq, bytes2int-append, band-65535-neg,
• int-abs/neg-15 is used by rightshift-8-01-01, rightshift-8-01, no-leading-zero-04, no-leading-zero-01, int2bytes-rec-neg-06, int2bytes-rec-neg-03, int2bytes-len-neg, int2bytes-first-neg-01, int2bytes-first-neg, bytes2int-size-val-06, bytes2int-rec, bytes2int-append,
• int-abs/negeq is used by rightshift-8-01, int2bytes-len-neg-01, int2bytes-len-neg, bytes2int-size-val-06, bytes2int-size-val-05, bytes2int-size-val-04, bytes2int-rec, bytes2int-append, bytes2int-1011x, bytes2int-100x-03, bytes2int-100x-02, bytes2int-011x-02, bits2int-2pot,
• int-abs/negle-07 is used by int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-rec-neg-01, int2bytes-len-neg, int2bytes-last-01, bytes2int-append, bits2int-pos,
• int-abs/negle-13 is used by rightshift-8-01-01, int2bytes-rec-neg-05, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-neg-03, int2bytes-len-ls-neg-02, int2bytes-len-ls-neg-01, int2bytes-len-ls-neg, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-le-neg, int2bytes-len-eq-neg-01, int2bytes-len-eq-neg, int2bytes-byte, bytes2int-size-05, bytes2int-size-04, bytes2int-range, bits2int-pos, band-65535-pos, band-65535-neg,
• int-abs/num-subadd is used by bytes2int-rec, bytes2int-append,
• int-abs/numadd is used by int2bytes-first-zerobyte-01, band-65535-neg,
• int-abs/numadd-01 is used by short-2bytes, rightshift-8-01, no-leading-zero-04, int2bytes-rec-pos-any, int2bytes-rec-neg-06, int2bytes-rec-neg-03, int2bytes-len-pos-01, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-leading-zeros, int2bytes-first-zerobyte-01, bytes2int-size-val-06, bytes2int-rec, bytes2int-mklist-mones-01, bytes2int-mklist-mones, bytes2int-int2bytes-len-eq, bytes2int-1011x, bytes2int-011x-02,
• int-abs/numle-02 is used by rightshift-8-01-01, no-leading-zero, int2bytes-minus-one, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-le-neg, int2bytes-len-le, int2bytes-len-eq-pos, int2bytes-leading-zeros, int2bytes-index-rightshift, int2bytes-first-zerobyte-01, int2bytes-first-neg-01, int2bytes-first-neg, int2bytes-byte-neg, int2bytes-byte, bytes2int-size-06, bytes2int-size-05, bytes2int-size, bytes2int-len-one-02, bytes2int-len-one-01, bytes2int-int2bytes-len-eq, bits2int-pos, band-65535-neg,
• int-abs/numle-03 is used by rightshift-8-01-01, no-leading-zero-04, no-leading-zero-01, no-leading-zero, int2bytes-len-pos, int2bytes-leading-zeros, int2bytes-last-01, int2bytes-first-neg-01, int2bytes-first-neg, bytes2int-int2bytes-len-eq, bytes2int-append,
• int-abs/numleledel is used by rightshift-8-01, rightshift-8, no-leading-zero-01, int2bytes-zero, int2bytes-rec-pos-04, int2bytes-one, int2bytes-leading-zeros, int2bytes-last-01, int2bytes-index-rightshift-02, int2bytes-first-zerobyte, bytes2int-int2bytes-len-eq,
• int-abs/numleledel-01 is used by setInt-theorem, rightshift-8-02, rightshift-8-01, rightshift-8, no-leading-zero-04, no-leading-zero-01, no-leading-zero, int2bytes-rec255-neg, int2bytes-rec-pos-any, int2bytes-rec-pos-04, int2bytes-rec-case, int2bytes-one, int2bytes-not-neg, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-one, int2bytes-len-neg256, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-leading-zeros, int2bytes-le127, int2bytes-last-01, int2bytes-index-rightshift, int2bytes-first-zerobyte-01, int2bytes-first-zerobyte, int2bytes-first-neg-01, int2bytes-first-neg, int2bytes-fillsgn-rec, int2bytes-byte, int2bytes-butlast, bytes2int-int2bytes-len-eq, bytes2int-2-le-32767, bits2int-pos, bits2bits-sgn,
• int-abs/numlelsdel is used by short-2bytes, setInt-theorem, rightshift-8-02, rightshift-8, no-leading-zero-01, int2bytes-zero, int2bytes-rec255-neg, int2bytes-rec-neg-256-01, int2bytes-rec-neg-256, int2bytes-rec-neg-06, int2bytes-rec-neg-03, int2bytes-rec-case, int2bytes-one, int2bytes-len-one-01, int2bytes-len-one, int2bytes-len-neg-01, int2bytes-last-01, int2bytes-first-zerobyte-01, int2bytes-fillsgn-rec, int2bytes-butlast, getInt-theorem, bytes2int-int2bytes-len-eq,
• int-abs/numlelsdel-01 is used by short-2bytes-03, short-2bytes, rightshift-8-02, rightshift-8-01, rightshift-8, int2bytes-rec-pos-any, int2bytes-rec-pos-04, int2bytes-rec-case, int2bytes-one, int2bytes-last-01, int2bytes-first-zerobyte, int2bytes-butlast, bytes2int-int2bytes-len-eq,
• int-abs/numls-01 is used by int2bytes-first-zerobyte-01,
• int-abs/numls-02 is used by short-2bytes-03, short-2bytes, rightshift-8-02, rightshift-8-01, rightshift-8, no-leading-zero-04, no-leading-zero-01, no-leading-zero, int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-len-le, int2bytes-len-eq-pos, int2bytes-leading-zeros, int2bytes-first-zerobyte-01, int2bytes-first-neg-01, int2bytes-first-neg, int2bytes-butlast, getInt-theorem, bytes2int-size-07, bytes2int-size-04, bytes2int-size-02, bytes2int-size-01, bytes2int-int2bytes-len-eq, bytes2int-append, bytes2int-1011x, bytes2int-100x-02, bytes2int-100x, bytes2int-011x-01, band-65535-neg,
• int-abs/numls-03 is used by short-2bytes, no-leading-zero-04, no-leading-zero-01, no-leading-zero, int2bytes-rec-neg-06, int2bytes-rec-neg-03, int2bytes-len-pos-01, int2bytes-len-neg-01, int2bytes-len-le-neg-03, int2bytes-len-le-neg-01, int2bytes-len-eq-pos, int2bytes-first-zerobyte-01, int2bytes-first-neg-01, int2bytes-first-neg, int2bytes-byte, bytes2int-size-04, bytes2int-size-01, bytes2int-len-one-02, bytes2int-len-one-01, bytes2int-int2bytes-len-eq, bytes2int-diff, bits2int-pos,
• int-abs/numlsf-01 is used by int2bytes-rec-pos, int2bytes-le255,
• int-abs/numlsledel is used by rightshift-8-01, rightshift-8, no-leading-zero-01, int2bytes-zero, int2bytes-rec-pos-04, int2bytes-rec-case, int2bytes-one, int2bytes-len-one-01, int2bytes-len-one, int2bytes-le127, int2bytes-first-zerobyte, int2bytes-first-neg, int2bytes-butlast, bytes2int-int2bytes-len-eq, band-65535-neg,
• int-abs/numlsledel-01 is used by rightshift-8-01, rightshift-8, no-leading-zero-04, int2bytes-rec-pos-04, int2bytes-rec-pos-03, int2bytes-rec-case, int2bytes-one, int2bytes-not-neg, int2bytes-leading-zeros, int2bytes-last-01, int2bytes-first-zerobyte, int2bytes-first-neg-01, int2bytes-first-neg, bytes2int-2-le-32767,
• int-abs/numsub is used by no-leading-zero-04, no-leading-zero, int2bytes-rec-pos-any, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-03, int2bytes-rec-neg-02, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-len-ls, int2bytes-len-le-neg, int2bytes-len-le, int2bytes-index-rightshift, int2bytes-first-zerobyte-01, int2bytes-byte, bytes2int-int2bytes-len-eq,
• int-abs/sub-add-01 is used by no-leading-zero-04, int2bytes-rec-pos, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-03, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-le255, int2bytes-index-rightshift-02, int2bytes-first-zerobyte-01, bytes2int-size-07, bytes2int-size-04, bytes2int-size-02, bytes2int-size-01, bytes2int-rec, bytes2int-append, bytes2int-1011x, bytes2int-100x-02, bytes2int-100x, bytes2int-011x-01,
• int-abs/sub-add-05 is used by int2bytes-index-rightshift-02, int2bytes-index-rightshift,
• int-abs/sub-add-06 is used by bytes2int-append,
• int-abs/sub-add-09 is used by bytes2int-size-val-06,
• int-abs/sub-eq is used by short-2bytes, rightshift-8-02, rightshift-8-01-01, rightshift-8-01, rightshift-8, no-leading-zero-04, int2bytes-rec-pos, int2bytes-rec-neg-06, int2bytes-rec-neg-03, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-le255, int2bytes-butlast, bytes2int-size-val-02, bytes2int-size-val, bytes2int-size-07, bytes2int-size-04, bytes2int-size-02, bytes2int-size-01, bytes2int-rec, bytes2int-int2bytes-len-eq, bytes2int-append, bytes2int-1011x, bytes2int-100x-02, bytes2int-011x-01, bytes2int-011x,
• int-abs/sub-eq-01 is used by rightshift-8-01, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-first-zerobyte-01,
• int-abs/sub-le is used by no-leading-zero-01, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-le-neg, int2bytes-len-le, int2bytes-len-eq-pos, int2bytes-index-rightshift-02, int2bytes-first-neg-01, int2bytes-first-neg, bits2int-pos,
• int-abs/sub-le-01 is used by rightshift-8-01-01, rightshift-8-01, no-leading-zero-04, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-03, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-le-neg, int2bytes-len-le-01, int2bytes-len-le, int2bytes-len-eq-pos, int2bytes-index-rightshift-02, int2bytes-first-zerobyte-01, bytes2int-size-07, bytes2int-size-04, bytes2int-size-02, bytes2int-size-01, bytes2int-int2bytes-len-eq, bytes2int-append, bytes2int-1011x, bytes2int-100x-02, bytes2int-100x, bytes2int-011x-01,
• int-abs/sub-ls is used by short-2bytes, rightshift-8-01-01, no-leading-zero-04, no-leading-zero-01, int2bytes-rec-neg-06, int2bytes-rec-neg-03, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-le-neg, int2bytes-len-le-01, int2bytes-len-eq-pos, int2bytes-first-zerobyte-01, int2bytes-first-neg, int2bytes-byte, bytes2int-int2bytes-len-eq,
• int-abs/sub-ls-01 is used by short-2bytes, rightshift-8-01-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-ls-01, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-le-neg, int2bytes-len-le-01, int2bytes-len-le, int2bytes-len-eq-pos, bytes2int-int2bytes-len-eq,
• int-abs/sub-pred is used by int2bytes-len-ls-01, int2bytes-len-le-upper, int2bytes-len-le-01,
• int-abs/sub-sub-04 is used by int2bytes-rec-neg-06, int2bytes-rec-neg-03, int2bytes-index-rightshift-02,
• int-abs/sub-zero-01 is used by bytes2int-int2bytes-len-eq,
• int-abs/subsub is used by rightshift-8-01, int2bytes-rec-neg-06, int2bytes-rec-neg-03, bytes2int-rec, bytes2int-append, band-65535-neg,
• int-abs/succ-01 is used by int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-eq-pos, int2bytes-index-rightshift, bytes2int-append,
• int-abs/succ-02 is used by int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-le-01, int2bytes-len-eq-pos, int2bytes-index-rightshift, int2bytes-first-zerobyte-01,
• int-abs/zero-gels is used by setInt-theorem, int2bytes-rec-case, int2bytes-one, int2bytes-not-neg, int2bytes-len-one-01, int2bytes-len-one, int2bytes-leading-zeros, bytes2bytes-first-pos,
• int-abs/zero-gels-01 is used by setInt-theorem, rightshift-8-01-01, rightshift-8, no-leading-zero-04, no-leading-zero-01, no-leading-zero, int2bytes-rec-pos-any, int2bytes-rec-pos-04, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-03, int2bytes-rec-neg-02, int2bytes-not-neg, int2bytes-len-one-01, int2bytes-len-one, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-le-neg, int2bytes-last-01, int2bytes-first-zerobyte-01, int2bytes-first-neg-01, int2bytes-first-neg, int2bytes-fillsgn-rec, int2bytes-byte, fix-rec-pos, fix-rec-neg, fillsgn-len-short, fillsgn-butlast, bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-04, bytes2int-neg-01, bytes2int-neg, bytes2int-len-one-02, bytes2int-len-one-01, bytes2int-int2bytes-len-eq, bytes2int-ge-zero, bytes2int-first-pos-01, bytes2int-first-pos, bytes2int-first-neq, bytes2int-first-lez, bytes2int-first-gez, bytes2int-diff, bytes2int-append, bytes2bytes-mone, bytes2bytes-fix, bytes2bytes-first-pos, bytes2bytes-first-neg, bits2int-pos, bits2bits-sgn, band-65535-neg,
• int-abs/zero-gels-02 is used by setInt-theorem, int2bytes-rec-case, int2bytes-one,
• int-abs/zero-gels-03 is used by rightshift-8, no-leading-zero-04, no-leading-zero-01, no-leading-zero, int2bytes-zero, int2bytes-rec-pos-any, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-03, int2bytes-rec-neg-02, int2bytes-rec-neg-01, int2bytes-rec-case, int2bytes-one, int2bytes-minus-one, int2bytes-len-pos-01, int2bytes-len-one-01, int2bytes-len-one, int2bytes-last-01, int2bytes-first-neg, int2bytes-butlast, bytes2int-int2bytes-len-eq, bits2bits-sgn, band-65535-neg,
• int-abs/zero-gels-04 is used by short-2bytes, setShort-theorem, setInt-theorem, rightshift-8-02, rightshift-8-01-01, no-leading-zero-01, no-leading-zero, int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-len-le-01, int2bytes-len-le, int2bytes-len-eq-pos, int2bytes-first-zerobyte-01, int2bytes-first-neg-01, int2bytes-first-neg, int2bytes-fillsgn-rec, getInt-theorem, fix2rest-last, fix-butlast-longer, fillsgn-rec, bytes2int-neg, bytes2int-len-one-01, bytes2int-int2bytes-len-eq, bytes2int-ge-zero, bytes2int-first-neq, bytes2int-first-lez, bytes2bytes-mone, bytes2bytes-first-neg, bits2int-pos, bits2bits-sgn,
• int-abs/zero-gs is used by int2bytes-rec-neg-03,

Used from specification intops

• intops/band-011x-neg is used by bytes2int-append,
• intops/band-011x-pos is used by bytes2int-append,
• intops/band-31-pos-01 is used by int2bytes-index-rightshift-02,
• intops/band-65535-neg is used by band-65535-neg,
• intops/bor-256-plus-01 is used by bytes2int-rec-bor,
• intops/bor-2pot-plus-02 is used by getInt-theorem,
• intops/bor-assoc is used by getInt-theorem,
• intops/bor-com is used by getInt-theorem,
• intops/intshiftleft-is-mult is used by getInt-theorem,
• intops/intshiftright-def-unbounded is used by setShort-theorem, setInt-theorem, intrightshift-8, int2bytes-index-rightshift-02,
• intops/shiftright-abs is used by rightshift-8-01,
• intops/shiftright-neg-div-01 is used by rightshift-8-02, rightshift-8-01-01,
• intops/shiftright-neg-div-02 is used by rightshift-8-02, rightshift-8-01-01,
• intops/shiftright-neg-mone is used by rightshift-8-02, rightshift-8-01-01,
• intops/shiftright-pos-div is used by rightshift-8-02,
• intops/shiftright-pos-div-01 is used by rightshift-8-01-01, int2bytes-butlast,
• intops/shiftright-rec-8 is used by rightshift-8-01, rightshift-8, int2bytes-butlast,
• intops/shiftright-rec-8-neg is used by rightshift-8-01, rightshift-8, int2bytes-butlast,
• intops/shiftright-shift is used by setInt-theorem,
• intops/band-255-neg is used by no-leading-zero, bytes2int-size-01, bytes2int-size, bytes2int-rec, bytes2int-mklist-mones-01, bytes2int-mklist-mones, bytes2int-len-one-02, bytes2int-len-one-01, bytes2int-diff, bytes2int-1011x, bytes2int-100x, bytes2int-011x-02, bytes2int-011x-01, bytes2int-011x,
• intops/band-255-pos is used by short-2bytes, no-leading-zero, bytes2int-zero-01, bytes2int-size-07, bytes2int-size-05, bytes2int-rec, bytes2int-mklist-zeros-01, bytes2int-mklist-zeros, bytes2int-len-one-02, bytes2int-leading-zero, bytes2int-int2bytes-len-eq, bytes2int-diff, bytes2int-1011x, bytes2int-100x-03, bytes2int-100x-02, bytes2int-100x-01, bytes2int-100x,
• intops/band-31-pos is used by setShort-theorem, setInt-theorem, intrightshift-8,
• intops/band-65535-pos is used by band-65535-pos,
• intops/band-associativity is used by short-2bytes-03, short-2bytes, setShort-theorem, setInt-theorem, no-leading-zero, intrightshift-8, getInt-theorem, bytes2int-zero-06, bytes2int-zero-01, bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-04, bytes2int-size-03, bytes2int-size-02, bytes2int-size-01, bytes2int-size, bytes2int-rec-bor, bytes2int-rec, bytes2int-neg, bytes2int-mklist-zeros-01, bytes2int-mklist-zeros, bytes2int-mklist-mones-01, bytes2int-mklist-mones, bytes2int-len-one-02, bytes2int-len-one-01, bytes2int-leading-zero, bytes2int-int2bytes-len-eq, bytes2int-i2b, bytes2int-first-pos, bytes2int-diff, bytes2int-2-le-32767, bytes2int-1011x, bytes2int-100x-03, bytes2int-100x-02, bytes2int-100x-01, bytes2int-100x, bytes2int-011x-02, bytes2int-011x-01, bytes2int-011x, byte2bits-val, band-65535-pos,
• intops/band-commutativity is used by short-2bytes-03, short-2bytes, setShort-theorem, setInt-theorem, no-leading-zero, intrightshift-8, getInt-theorem, bytes2int-zero-06, bytes2int-zero-01, bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-04, bytes2int-size-03, bytes2int-size-02, bytes2int-size-01, bytes2int-size, bytes2int-rec-first-zero, bytes2int-rec-bor, bytes2int-rec-01, bytes2int-rec, bytes2int-neg, bytes2int-mklist-zeros-01, bytes2int-mklist-zeros, bytes2int-mklist-mones-01, bytes2int-mklist-mones, bytes2int-len-one-02, bytes2int-len-one-01, bytes2int-leading-zero, bytes2int-int2bytes-len-eq, bytes2int-i2b, bytes2int-first-pos, bytes2int-diff, bytes2int-2-le-32767, bytes2int-1011x, bytes2int-100x-03, bytes2int-100x-02, bytes2int-100x-01, bytes2int-100x, bytes2int-011x-02, bytes2int-011x-01, bytes2int-011x, byte2bits-val, band-65535-pos,
• intops/band-max-02 is used by short-2bytes-03, short-2bytes, getInt-theorem,
• intops/band-max-04 is used by no-leading-zero, getInt-theorem, bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-04, bytes2int-size-03, bytes2int-size-02, bytes2int-size-01, bytes2int-size, bytes2int-rec-bor, bytes2int-neg, bytes2int-len-one-01, bytes2int-int2bytes-len-eq, bytes2int-diff, bytes2int-2-le-32767,
• intops/band-notneg is used by short-2bytes, no-leading-zero, getInt-theorem, bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-04, bytes2int-size-03, bytes2int-size-02, bytes2int-size-01, bytes2int-size, bytes2int-rec-bor, bytes2int-neg, bytes2int-len-one-01, bytes2int-int2bytes-len-eq, bytes2int-first-pos, bytes2int-diff, bytes2int-2-le-32767,
• intops/bor-65536-plus is used by getInt-theorem,
• intops/bor-neq is used by getInt-theorem,
• intops/rightshift-zero is used by rightshift-8-01-01, rightshift-8-01, rightshift-8, int2bytes-butlast,
• intops/shiftright-not-neg is used by setInt-theorem, int2bytes-fillsgn-rec,
• intops/shiftright-not-pos-01 is used by setInt-theorem, int2bytes-fillsgn-rec,
• intops/shiftright-zero is used by rightshift-8-01,

Used from specification list-last

• list-last/bytelist/bc is used by rightshift-8-02,
• list-last/bytelist/mk-last-02 is used by bytes2int-mklist-zeros, bytes2int-mklist-mones, bytes2int-1011x, bytes2int-100x-03, bytes2int-100x-02, bytes2int-100x-01, bytes2int-100x, bytes2int-011x-02, bytes2int-011x-01, bytes2int-011x,
• list-last/bitlista/mk-plus is used by int2bytes-rec-pos-any, fix-bits2bytes-01, fix-bits2bytes, bits2bytes-mklist-01,
• list-last/bytelist/mk-rec is used by setInt-theorem, fix-rec-pos, fix-rec-neg, fix-bits2bytes-01, fillsgn-rec, bytes2int-size-val, bits2bytes-mklist-02,
• list-last/bitlista/mk-rest-01 is used by int2bytes-rec-pos-any,
• list-last/bytelist/mk-rest-01 is used by fix2rest-last,
• list-last/bytelist/mk-succ is used by bytes2int-size-val-05,
• list-last/bytelist/mklist-last is used by bytes2int-fillsgn-zero,
• list-last/bitlista/mklist-split-intro is used by bits2bytes-2pot,
• list-last/bytelist/splitlasteq is used by no-leading-zero-04, no-leading-zero-01, int2bytes-leading-zeros, int2bytes-first-neg-01, int2bytes-first-neg,
• list-last/bytelist/splitlasteq-01 is used by int2bytes-rec-shift,
• list-last/bytelist/b is used by rightshift-8-02, rightshift-8, no-leading-zero-01, int2bytes-leading-zeros, int2bytes-first-neg-01, int2bytes-first-neg, int2bytes-butlast, bytes2int-size-07, bytes2int-size-05, bytes2int-size-01, bytes2int-size,
• list-last/bytelist/b-01 is used by fillsgn-butlast, bytes2int-zero-06,
• list-last/bytelist/bapp is used by no-leading-zero-04, no-leading-zero-01, int2bytes-leading-zeros, int2bytes-first-neg-01, int2bytes-first-neg, fix-butlast-longer, fillsgn-butlast, bytes2int-zero-06, bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-04, bytes2int-size-03, bytes2int-size-02, bytes2int-size-01, bytes2int-size, bytes2int-rec-first-zero, bytes2int-neg, bytes2int-len-one-02, bytes2int-first-pos,
• list-last/bitlista/bin is used by bits2bytes-2pot,
• list-last/bytelist/bin is used by no-leading-zero-01, int2bytes-leading-zeros, bytes2int-size-07, bytes2int-size-05, bytes2int-size-01, bytes2int-size,
• list-last/bytelist/bin-01 is used by bytes2int-zero-06,
• list-last/bitlista/butlast-def is used by bits2bytes-2pot,
• list-last/bytelist/butlast-def is used by rightshift-8-02, rightshift-8-01, rightshift-8, int2bytes-butlast, fix-butlast, bytes2int-leading-zero, bytes2int-1011x,
• list-last/bytelist/butlast-last is used by no-leading-zero, bytes2int-len-one-01,
• list-last/bytelist/l is used by rightshift-8, no-leading-zero-01, int2bytes-rec255-neg, int2bytes-rec-pos-02, int2bytes-rec-pos-01, int2bytes-rec-pos, int2bytes-rec-neg-256, int2bytes-rec-case, int2bytes-leading-zeros, int2bytes-last-01, int2bytes-last, bytes2int-size-07, bytes2int-size-05, bytes2int-size-01, bytes2int-size, bytes2int-int2bytes-len-eq,
• list-last/bytelist/l-02 is used by no-leading-zero-01, int2bytes-rec255-neg, int2bytes-leading-zeros, int2bytes-first-neg-01, int2bytes-first-neg, fix2rest-last, bytes2int-zero-06, bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-04, bytes2int-size-03, bytes2int-size-02, bytes2int-size-01, bytes2int-size, bytes2int-rec-first-zero, bytes2int-neg, bytes2int-len-one-02, bytes2int-first-pos,
• list-last/bytelist/l-05 is used by no-leading-zero-04, no-leading-zero-01, int2bytes-leading-zeros, bytes2int-size-07, bytes2int-size-05, bytes2int-size-01, bytes2int-size, bytes2int-rec-first-zero, bytes2int-len-one-02,
• list-last/bytelist/l-in is used by no-leading-zero-04,
• list-last/bytelist/lapp is used by fix-last,
• list-last/bitlista/last-01 is used by bits2bytes-2pot,
• list-last/bitlista/last-def is used by int2bytes-minus-256,
• list-last/bytelist/last-def is used by int2bytes-rec-pos-03, int2bytes-rec-pos, int2bytes-last-01, fix-two-02, fix-last, bytes2int-leading-zero, bytes2int-int2bytes-len-eq, bytes2int-1011x,
• list-last/bytelist/last-elim is used by no-leading-zero-01, no-leading-zero, int2bytes-rec255-neg, int2bytes-leading-zeros, int2bytes-first-neg-01, int2bytes-first-neg, fix2rest-last, fix-two-03, fillsgn-butlast, bytes2int-zero-03, bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-04, bytes2int-size-03, bytes2int-size-02, bytes2int-size-01, bytes2int-size, bytes2int-rec-first-zero, bytes2int-rec-01, bytes2int-neg, bytes2int-mklist-zeros-01, bytes2int-mklist-mones-01, bytes2int-len-one-02, bytes2int-len-one-01, bytes2int-int2bytes-len-eq, bytes2int-i2b, bytes2int-diff,
• list-last/bytelist/lb is used by fix-butlast-longer, fix-butlast, fillsgn-butlast, bytes2int-zero-06, bytes2int-first-pos,
• list-last/bytelist/lin-01 is used by no-leading-zero-01, int2bytes-first-neg-01, int2bytes-first-neg, bytes2int-zero-06,
• list-last/bytelist/lin-02 is used by no-leading-zero-04, int2bytes-leading-zeros,
• list-last/bitlista/mk-elem is used by bits2bits-in,
• list-last/bytelist/mk-elem is used by setInt-theorem, fix-butlast-longer,
• list-last/bitlista/mk-empty is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-04, int2bytes-rec-neg-02, int2bytes-rec-neg-01, fix-bits2bytes-01, fix-bits2bytes, byte2bits-val, bits2bytes-mklist-03, bits2bytes-mklist-01,
• list-last/bytelist/mk-empty is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, fix2rest-last, fix-pos-le, fix-neg-le, fix-butlast-longer, fix-bits2bytes-01, fix-bits2bytes, fillsgn-empty, bytes2int-mklist-zeros-01, bytes2int-mklist-zeros, bytes2int-mklist-mones-01, bytes2int-mklist-mones, bits2bytes-mklist-03,
• list-last/bytelist/mk-in is used by setInt-theorem,
• list-last/bitlista/mk-in is used by bits2bits-in,
• list-last/bytelist/mk-inj-01 is used by int2bytes-rec-pos-any, int2bytes-rec-neg-04, int2bytes-rec-neg-01, int2bytes-fillsgn-rec, fix-bits2bytes-01, fix-bits2bytes, fillsgn-butlast, bits2bytes-mklist-03, bits2bytes-mklist-01,
• list-last/bitlista/mk-last is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-rec-neg-01, fix-bits2bytes, bytes2bits-mklist-01, bytes2bits-mklist, bits2bytes-fill,
• list-last/bytelist/mk-last is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-04, int2bytes-rec-neg-02, int2bytes-rec-neg-01, fix-bits2bytes, bytes2bits-mklist-01, bytes2bits-mklist, bits2bytes-mklist-03, bits2bytes-mklist-02, bits2bytes-mklist-01, bits2bytes-mklist,
• list-last/bitlista/mk-len is used by int2bytes-rec-pos-any, int2bytes-rec-pos, int2bytes-rec-neg-05, int2bytes-rec-neg-04, int2bytes-rec-neg-02, int2bytes-rec-neg-01, int2bytes-len-neg, int2bytes-first-zerobyte, fix-bits2bytes-01, fix-bits2bytes, byte2bits-val, bits2bytes-mklist-03, bits2bytes-mklist-02, bits2bytes-mklist-01, bits2bytes-mklist, bits2bytes-fill, bits2bytes-2pot,
• list-last/bytelist/mk-len is used by rightshift-8-01-01, fix-length, fillsgn-length, bytes2int-size-val-07, bytes2int-size-val-06, bytes2int-size-val-05, bytes2int-size-val-04, bytes2int-size-val-03, bytes2int-size-val-02, bytes2int-size-val-01, bytes2int-size-val, bytes2int-fillsgn-zero,
• list-last/bytelist/mk-one-01 is used by bits2bytes-mklist-02, bits2bytes-mklist,
• list-last/bytelist/mk-plus is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, fix-bits2bytes, bytes2int-fillsgn-zero, bytes2bits-mklist-01, bytes2bits-mklist, bits2bytes-mklist-03, bits2bytes-mklist-01, bits2bytes-mklist,
• list-last/bitlista/mk-plus is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-rec-neg-01, fix-bits2bytes-01, fix-bits2bytes, bytes2bits-mklist-01, bytes2bits-mklist, bits2bytes-mklist-01,
• list-last/bytelist/mk-rest is used by fix2rest-last,
• list-last/bytelist/mk-two-01 is used by setInt-theorem,
• list-last/bitlista/mk-zero is used by no-leading-zero, int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-rec-neg-01, int2bytes-first-zerobyte, fix-bits2bytes-01, fix-bits2bytes, bytes2int-zero-04, bytes2int-zero-02, bytes2int-mone, bytes2bytes-zero, bytes2bytes-mone, bytes2bits-mklist-01, bytes2bits-mklist, byte2bits-zero, byte2bits-val, byte2bits-mone, bits2bytes-mklist-03, bits2bytes-mklist-02, bits2bytes-mklist-01, bits2bytes-mklist, bits2bytes-2pot, bits2bits-sgn,
• list-last/bytelist/mk-zero is used by int2bytes-rec255-neg, int2bytes-rec-pos-any, fix2rest-last, bytes2int-mklist-zeros-01, bytes2int-mklist-zeros, bytes2int-mklist-mones-01, bytes2int-1011x, bytes2int-100x-03, bytes2int-100x-02, bytes2int-100x-01, bytes2int-100x, bytes2int-011x-02, bytes2int-011x-01, bytes2int-011x, bytes2bits-mklist-01, bytes2bits-mklist, bits2bytes-mklist-03, bits2bytes-mklist-01,
• list-last/bitlista/mklist-one is used by int2bytes-rec-pos-any,
• list-last/bytelist/mklist-one is used by setShort-theorem, setInt-theorem, rightshift-8-02, int2bytes-rec255-neg, int2bytes-rec-pos-any, int2bytes-rec-pos-04, int2bytes-rec-neg-05, int2bytes-rec-neg-02, fix-two, fix-bits2bytes-01, fix-bits2bytes, fillsgn-short, fillsgn-rec, bytes2int-mklist-mones, bytes2int-fillsgn-zero, bytes2bits-mklist-01, bytes2bits-mklist, bits2bytes-mklist-03, bits2bytes-mklist-01, bits2bytes-mklist,

Used from specification list-data

• list-data/bytelist/fr-02 is used by bytes2int-first-gez,
• list-data/bytelist/le-one is used by setShort-theorem-01,
• list-data/bytelist/length-neq is used by fix-two-04, fix-two-03, fillsgn-short, fillsgn-not-empty,
• list-data/bytelist/length-rest is used by int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-le-neg, int2bytes-len-le, int2bytes-len-eq-pos,
• list-data/bitlista/length-rest is used by int2bytes-rec-pos-any, int2bytes-rec-pos, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-first-zerobyte,
• list-data/bytelist/length-rest-intro is used by setShort-theorem-01,
• list-data/bytelist/lf-01 is used by setShort-theorem-01, rightshift-8-02, fillsgn-short, bytes2int-mklist-mones-01, bytes2int-int2bytes-len-eq, bytes2int-diff,
• list-data/bytelist/elim-list is used by setShort-theorem-01, rightshift-8-02, no-leading-zeros, int2bytes-rec255-neg, int2bytes-len-le-neg-03, int2bytes-len-le-neg-01, int2bytes-len-eq-pos, fix2rest-last, fix-two-04, fix-two-03, fix-rec-pos, fix-rec-neg, bytes2int-pos, bytes2int-mklist-zeros-01, bytes2int-mklist-mones-01, bytes2int-int2bytes-len-eq, bytes2int-diff, bytes2bytes-length, bytes2bytes-identity, bytes2bytes-fix, bytes2bytes-first-neg,
• list-data/bytelist/elim-list-c is used by setShort-theorem-01, no-leading-zero-03, no-leading-zero-02, no-leading-zero, int2bytes-first-neg, fix-butlast-longer, fillsgn-short, fillsgn-rec, fillsgn-butlast, bytes2int-zero-06, bytes2int-neg, bytes2int-len-one-02, bytes2int-len-one-01, bytes2int-int2bytes-len-eq, bytes2int-fillsgn-zero, bytes2bytes-zero, bytes2bytes-other, bytes2bytes-mone, bytes2bytes-identity,
• list-data/bitlista/elim-list-c is used by int2bytes-rec-pos, bits2int-pos, bits2bytes-fill,
• list-data/bytelist/l is used by setShort-theorem-01, setShort-theorem, setInt-theorem, rightshift-8-02, rightshift-8-01-01, rightshift-8-01, rightshift-8, no-leading-zeros, no-leading-zero-03, no-leading-zero, intrightshift-8, int2bytes-rec255-neg, int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-one, int2bytes-len-one-01, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-le-neg, int2bytes-len-le, int2bytes-len-eq-pos, int2bytes-len-eq-neg-01, int2bytes-len-eq-neg, int2bytes-index-rightshift-02, int2bytes-index-rightshift-01, int2bytes-index-rightshift, int2bytes-fillsgn-rec, int2bytes-bytes2int-length-01, fix2rest-last, fix-two-03, fix-one-01, fix-butlast-longer, fix-butlast, fix-bits2bytes-01, fillsgn-short, fillsgn-not-empty, fillsgn-len-short, fillsgn-butlast, bytes2int-zero-06, bytes2int-zero-05, bytes2int-zero-03, bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-04, bytes2int-size-03, bytes2int-size-02, bytes2int-size-01, bytes2int-size, bytes2int-rec-first-zero, bytes2int-rec-01, bytes2int-neg, bytes2int-mklist-zeros-01, bytes2int-mklist-mones-01, bytes2int-len-one-02, bytes2int-len-one-01, bytes2int-int2bytes-len-eq, bytes2int-first-pos, bytes2int-fillsgn-zero, bytes2int-diff, bytes2int-append, bytes2bytes-zero, bytes2bytes-mone, bytes2bytes-length, bytes2bytes-identity, bytes2bytes-fix, bytes2bytes-first-neg, bytes2bytes-fillsgn, band-65535-pos, band-65535-neg,
• list-data/bitlista/l is used by int2bytes-rec-pos-any, int2bytes-rec-pos, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-minus-one, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-len-def, int2bytes-le255, int2bytes-le127, int2bytes-first-zerobyte-01, int2bytes-first-zerobyte, int2bytes-byte-neg, int2bytes-byte, fix-bits2bytes, bytes2bytes-zero, bytes2bytes-other, bytes2bytes-mone, byte2bits-val, bits2int-pos, bits2bytes-rec-02, bits2bytes-rec-01, bits2bytes-len-01, bits2bytes-len, bits2bytes-fill, bits2bytes-app, bits2bits-sgn, bits2bits-inj, bits2bits-in,
• list-data/bytelist/length-rest is used by int2bytes-len-eq-pos,
• list-data/bitlista/length-rest is used by int2bytes-rec-pos, int2bytes-rec-neg-05, int2bytes-rec-neg-02,
• list-data/bitlista/lf-01 is used by int2bytes-rec-pos,
• list-data/bytelist/lr-04 is used by int2bytes-len-eq-pos,
• list-data/bitlista/size-01 is used by int2bytes-rec-neg-05, int2bytes-rec-neg-02, bytes2bits-length, byte2bits8, bits2bytes-len-02,
• list-data/bytelist/size-01 is used by setShort-theorem-01, int2bytes-rec255-neg, fix2rest-last, fillsgn-not-empty, fillsgn-empty, bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-04, bytes2int-size-03, bytes2int-size-02, bytes2int-size-01, bytes2int-size, bytes2int-rec-first-zero, bytes2int-int2bytes-len-eq, bytes2int-diff, bytes2bytes-mone, bytes2bytes-length, bytes2bytes-identity, bytes2bytes-fix, bytes2bits-length,

Used from specification int2bits

• int2bits/bits2bits-def is used by bytes2bytes-other, bits2int-pos, bits2bits-in,
• int2bits/bits2int-fill is used by bytes2bytes-zero, bytes2bytes-mone, byte2bits-value,
• int2bits/bits2int-ge-zero is used by bytes2int-pos,
• int2bits/bits2int-le8 is used by bits2int-pos,
• int2bits/bits2int-le8-01 is used by int2bytes-rec-pos-any,
• int2bits/bits2int-lez is used by int2bytes-rec-pos-any, bits2int-zero-ls, bits2int-pos,
• int2bits/bits2int-mklist is used by fix-value, bits2bytes-fill,
• int2bits/bits2int-neg is used by bits2int-pos,
• int2bits/bits2int-neg-03 is used by bytes2int-rec, bytes2int-append, bits2int-pos,
• int2bits/bits2int-nls is used by bytes2bits-nls,
• int2bits/bits2int-ones is used by bits2bytes-mklist-03, bits2bytes-mklist-02,
• int2bits/bits2int-pos-02 is used by int2bytes-rec-pos-any, fix-value, bytes2int-zero-04, bytes2int-rec, bytes2int-append, byte2bits-val,
• int2bits/bits2int-range is used by bytes2int-range,
• int2bits/bits2int-sgn is used by int2int, bits2int-2pot,
• int2bits/bits2int-sgn-intro is used by bytes2int-mone,
• int2bits/bits2int-zero-02 is used by no-leading-zero, bytes2int-len-one-01,
• int2bits/bits2int-zeros is used by int2bytes-rec-pos-any, fix-value,
• int2bits/bits2uint-inv-neg is used by bytes2int-rec, bytes2int-append,
• int2bits/bits2uint-inv-pos is used by bytes2int-rec, bytes2int-append,
• int2bits/bits2uint-ls is used by bits2int-pos,
• int2bits/bits2uint-nle is used by bytes2bits-nle,
• int2bits/bits2uint-not-zero is used by bits2int-pos,
• int2bits/bits2uint-ones is used by byte2bits-val,
• int2bits/bits2uint-split is used by bytes2int-rec, bytes2int-append, byte2bits-val,
• int2bits/bits2uint-succ is used by bytes2int-rec, bytes2int-append,
• int2bits/int2bits-2pot-04 is used by int2bytes-rec-neg-04,
• int2bits/int2bits-lelen is used by int2bytes-rec-pos-any, int2bytes-minus-one,
• int2bits/int2bits-lelen-01 is used by int2bytes-len-pos, int2bytes-len-ls-01,
• int2bits/int2bits-lelen-03 is used by int2bytes-minus-one,
• int2bits/int2bits-lelen-04 is used by int2bytes-len-neg,
• int2bits/int2bits-lelen-06 is used by int2bytes-first-zerobyte,
• int2bits/int2bits-len-mod2pot is used by int2bytes-rec-pos-any,
• int2bits/int2bits-len-neg is used by int2bytes-rec-neg-05,
• int2bits/int2bits-len-one is used by int2bytes-len-pos, int2bytes-len-ls-01, int2bytes-first-zerobyte,
• int2bits/int2bits-len-pos is used by int2bytes-len-pos-01, int2bytes-first-zerobyte,
• int2bits/int2bits-len-range is used by int2bytes-le127,
• int2bits/int2bits-leneq-neg is used by int2bytes-len-neg256, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-byte-neg, int2bytes-byte,
• int2bits/int2bits-leneq-pos is used by int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-ls-01, int2bytes-first-zerobyte-01, int2bytes-byte,
• int2bits/int2bits-lslen-01 is used by int2bytes-len-pos, int2bytes-len-ls-01,
• int2bits/int2bits-lslen-02 is used by int2bytes-len-neg,
• int2bits/int2bits-lslen-03 is used by int2bytes-byte-neg,
• int2bits/int2bits-lslen-04 is used by int2bytes-len-neg-01,
• int2bits/int2bits-lslen-05 is used by int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-byte-neg,
• int2bits/int2bits-lslen-06 is used by int2bytes-rec-pos-any, int2bytes-len-pos, int2bytes-len-ls-01, int2bytes-first-zerobyte,
• int2bits/int2bits-mone is used by int2bytes-len-neg, byte2bits-mone,
• int2bits/int2bits-neg-num is used by int2bytes-minus-256,
• int2bits/int2bits-ones is used by bytes2bytes-other, bytes2bytes-mone,
• int2bits/int2bits-pos is used by int2bytes-rec-pos-any, int2bytes-rec-pos, int2bytes-le255, bits2int-pos,
• int2bits/int2bits-rec-2pot-neg-01 is used by int2bytes-rec-neg-01,
• int2bits/int2bits-rec-2pot-neg-02 is used by int2bytes-rec-neg-05, int2bytes-rec-neg-02,
• int2bits/int2bits-rec-2pot-pos is used by int2bytes-rec-pos-any, int2bytes-first-zerobyte,
• int2bits/int2bits-rec-neg is used by int2bytes-len-neg-01,
• int2bits/int2bits-rest is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02,
• int2bits/int2int-rest-01 is used by int2bytes-byte-neg,
• int2bits/int2uint-neg is used by byte2bits-val,
• int2bits/ubits2bits is used by bytes2int-append,
• int2bits/uint2bits-2potrec is used by int2bytes-rec-pos,
• int2bits/uint2bits-first is used by int2bytes-le255,
• int2bits/uint2bits-len is used by int2bytes-rec-pos, int2bytes-le255,
• int2bits/uint2bits-len-max is used by int2bytes-rec-pos,
• int2bits/uint2int-rest is used by int2bytes-rec-pos, int2bytes-le255,
• int2bits/bits2bits-def is used by int2bytes-bytes2int-length-01, bytes2bytes-zero, bytes2bytes-mone, bytes2bytes, byte2bits8, bits2bits-sgn, bits2bits-in,
• int2bits/bits2int-2pot is used by bits2int-2pot,
• int2bits/bits2int-base is used by bytes2int-pos, bytes2int-mklist-zeros,
• int2bits/bits2int-fill is used by int2bytes-rec-pos,
• int2bits/bits2int-first is used by fix-value, bytes2int-append, bits2bits-sgn,
• int2bits/bits2int-first-01 is used by fix-value, bytes2int-append, bits2bits-sgn,
• int2bits/bits2int-inj is used by bytes2int-mone,
• int2bits/bits2int-le8 is used by bits2bits-sgn, bits2bits-in,
• int2bits/bits2int-le8-01 is used by bits2bits-sgn, bits2bits-in,
• int2bits/bits2int-mklist-01 is used by bits2bytes-fill,
• int2bits/bits2int-mklist-06 is used by bits2bytes-mklist-03, bits2bytes-mklist-02,
• int2bits/bits2int-one is used by int2bytes-rec-neg-05, int2bytes-rec-neg-02, bytes2bytes-mone, bits2bytes-true, bits2bytes-mklist-03, bits2bytes-mklist-02,
• int2bits/bits2int-pos is used by int2bytes-rec-pos-any, int2bytes-minus-256, fix-value, fix-bits2bytes-01, bytes2int-zero-04, bytes2int-zero-02, bits2int-pos, bits2bytes-mklist, bits2bytes-2pot,
• int2bits/bits2int-sgn is used by bytes2int-mone,
• int2bits/bits2int-zero is used by int2bytes-rec-pos-any, int2bytes-le255, bytes2bytes-zero,
• int2bits/bits2int-zeros-03 is used by bits2bytes-mklist-01, bits2bytes-mklist,
• int2bits/bits2int8 is used by byte2bits8,
• int2bits/bits2int8-01 is used by byte2bits8,
• int2bits/bits2int8-02 is used by bits2bits-sgn, bits2bits-in,
• int2bits/bits2int8-03 is used by bits2bits-sgn, bits2bits-in,
• int2bits/bits2uint-base is used by byte2bits-val,
• int2bits/bits2uint-not-neg is used by bits2int-pos,
• int2bits/bits2uint-not-neg-01 is used by int2bytes-rec-pos-any, bits2int-pos,
• int2bits/bits2uint-one-02 is used by int2bytes-minus-256, fix-bits2bytes-01, bits2bytes-mklist, bits2bytes-2pot,
• int2bits/bits2uint-zero is used by int2bytes-minus-256, fix-bits2bytes-01, bits2bytes-mklist, bits2bytes-2pot,
• int2bits/bits2uint-zeros is used by bits2int-pos,
• int2bits/bits2uint-zeros-03 is used by bytes2int-zero-04, bytes2int-zero-02,
• int2bits/int2bits-2pot-01 is used by int2bytes-len-neg,
• int2bits/int2bits-fillfirst is used by bytes2bytes-zero, byte2bits-first,
• int2bits/int2bits-first-01 is used by int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-byte-neg, bytes2bytes-zero, byte2bits-val, byte2bits-first,
• int2bits/int2bits-first-02 is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, bytes2int-len-one-01, byte2bits-first,
• int2bits/int2bits-len-one is used by int2bytes-len-pos-01, int2bytes-first-zerobyte-01,
• int2bits/int2bits-neg-num is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, bytes2bytes-mone, bytes2bits-mklist-01,
• int2bits/int2bits-not-empty is used by no-leading-zero, int2int, int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-04, int2bytes-rec-neg-02, int2bytes-rec-neg-01, int2bytes-minus-one, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-len-fits, int2bytes-len-def, int2bytes-le255, int2bytes-le127, int2bytes-first-zerobyte-01, int2bytes-first-zerobyte, int2bytes-byte-neg, int2bytes-byte, bytes2int-len-one-01, bytes2bytes-zero, bytes2bytes-other, bytes2bytes-mone, byte2bits-value, byte2bits-val, byte2bits-empty,
• int2bits/int2bits-sgn is used by int2int, bytes2bytes-other,
• int2bits/int2bits-truein is used by no-leading-zero, bytes2int-len-one-01, bytes2bytes-zero, bytes2bytes-other,
• int2bits/int2bits-zero is used by no-leading-zero, int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-04, int2bytes-rec-neg-02, int2bytes-rec-neg-01, int2bytes-first-zerobyte-01, int2bytes-first-zerobyte, bytes2int-zero-02, bytes2bytes-zero, bytes2bits-mklist, byte2bits-zero,
• int2bits/int2int-inj is used by int2int, int2bytes-rec-pos-any, int2bytes-rec-pos, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-minus-one, int2bytes-le255, int2bytes-le127, int2bytes-byte, bytes2bytes-zero, bytes2bytes-other, bytes2bytes-mone, byte2bits-value,
• int2bits/uint2bits-empty is used by int2bytes-rec-pos, int2bytes-le255, bits2int-pos,
• int2bits/uint2bits-first-02 is used by bits2int-pos,
• int2bits/uint2bits-one is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-minus-256, bytes2bytes-mone, bytes2bits-mklist-01,
• int2bits/uint2bits-pos-num is used by int2bytes-minus-256,
• int2bits/uint2uint-pos is used by int2bytes-rec-pos-any,

Used from specification list

• list/bytelist/Cons is used by bytes2int-first-pos-01,
• list/bytelist/Nil is used by bytes2int-first-pos-01,
• list/bytelist/One is used by bytes2int-first-pos-01,
• list/bitlista/a is used by int2bytes-rec-pos-any, fix-bits2bytes-01, fix-bits2bytes, bytes2bytes-zero,
• list/bytelist/app-06 is used by int2bytes-rec-pos,
• list/bitlista/app-08 is used by bits2bits-sgn,
• list/bitlista/first-01 is used by bytes2int-zero-04, bytes2int-rec, bytes2int-pos, bytes2int-mone, bytes2int-append, bits2int-zero-ls, bits2int-pos,
• list/bytelist/first-01 is used by int2bytes-rec-pos-any, int2bytes-not-neg, int2bytes-first-zerobyte, int2bytes-fillsgn-rec, bytes2bytes-other, bytes2bytes-mone,
• list/bytelist/fr is used by int2bytes-len-le-neg-02, int2bytes-len-le-neg, int2bytes-len-le, bytes2int-first-lez,
• list/bytelist/lastdiv-rew is used by bytes2bytes-zero, bytes2bytes-other, bytes2bytes-mone,
• list/bitlista/rest-01 is used by int2bytes-rec-neg-05, int2bytes-rec-neg-02,
• list/bytelist/rest-01 is used by fix2rest-last,
• list/bytelist/Last is used by setShortInt-theorem, setShort-theorem, setInt-theorem, no-leading-zero-04, no-leading-zero, int2bytes-rec-shift, int2bytes-rec-pos, int2bytes-minus-one, int2bytes-minus-256-01, int2bytes-minus-256, int2bytes-le255, int2bytes-fillsgn-rec, int2bytes-empty, int2bytes-byte, fix2rest-last, fix-last, fix-butlast, bytes2int-len-one-01, bytes2int-int2bytes-len-eq, bytes2bytes-zero, bytes2bytes-other, bytes2bytes-mone, bits2bytes-rec-02, bits2bytes-mklist-02, bits2bytes-mklist, bits2bytes-len, bits2bytes-empty, bits2bytes-app, bits2bytes-2pot, bits2bits-sgn, bits2bits-inj, bits2bits-in,
• list/bitlista/Last is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-minus-256, bytes2bytes-mone, bytes2bits-mklist-01,
• list/bitlista/Nil is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, fix-bits2bytes-01, fix-bits2bytes, bytes2bytes-other, bytes2bits-append, bits2bits-sgn,
• list/bytelist/Nil is used by int2bytes-rec255-neg, int2bytes-rec-pos-any, fix2rest-last, bytes2int-mklist-zeros-01, bytes2int-mklist-zeros, bytes2int-mklist-mones-01, bytes2int-int2bytes-len-eq, bytes2int-i2b, bytes2bytes-other, bytes2bytes-mone, bytes2bits-append,
• list/bytelist/Two is used by setShortInt-theorem, setShort-theorem-01,
• list/bitlista/Two is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-minus-256, bytes2bytes-mone, bytes2bits-mklist-01,
• list/bytelist/a is used by short-2bytes-02, setShort-theorem-01, setShort-theorem, setInt-theorem, rightshift-8-02, rightshift-8-01, rightshift-8, no-leading-zeros, no-leading-zero-04, no-leading-zero-03, no-leading-zero-02, no-leading-zero-01, no-leading-zero, int2bytes-zero, int2bytes-rec255-neg, int2bytes-rec-pos-any, int2bytes-rec-pos-04, int2bytes-rec-pos-03, int2bytes-rec-pos-02, int2bytes-rec-pos-01, int2bytes-rec-pos, int2bytes-rec-neg-256-01, int2bytes-rec-neg-256, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-04, int2bytes-rec-neg-03, int2bytes-rec-neg-02, int2bytes-rec-neg-01, int2bytes-rec-case, int2bytes-one, int2bytes-not-neg-01, int2bytes-not-neg, int2bytes-minus-one, int2bytes-minus-256-01, int2bytes-minus-256, int2bytes-len-one-01, int2bytes-len-one, int2bytes-len-le-neg-03, int2bytes-len-le-neg-01, int2bytes-len-eq-pos, int2bytes-leading-zeros, int2bytes-le255, int2bytes-last-01, int2bytes-first-zerobyte, int2bytes-first-neg-01, int2bytes-first-neg, int2bytes-fillsgn-rec, int2bytes-empty, int2bytes-byte-neg, int2bytes-butlast, getInt-theorem, fix2rest-last, fix-value, fix-two-04, fix-two-03, fix-two-02, fix-two-01, fix-two, fix-rec-pos, fix-rec-neg, fix-pos-le, fix-neg-le, fix-length, fix-last, fix-butlast-longer, fix-butlast, fix-bits2bytes-01, fix-bits2bytes, fillsgn-short, fillsgn-rec, fillsgn-length, fillsgn-fix, fillsgn-empty, fillsgn-butlast, bytes2int-zero-06, bytes2int-zero-04, bytes2int-zero-03, bytes2int-zero-02, bytes2int-size-val, bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-04, bytes2int-size-03, bytes2int-size-02, bytes2int-size-01, bytes2int-size, bytes2int-rec-first-zero, bytes2int-rec-01, bytes2int-rec, bytes2int-pos, bytes2int-neg-01, bytes2int-neg, bytes2int-mone, bytes2int-mklist-zeros-01, bytes2int-mklist-zeros, bytes2int-mklist-mones-01, bytes2int-len-one-02, bytes2int-len-one-01, bytes2int-leading-zero, bytes2int-le-zero, bytes2int-int2bytes-len-eq, bytes2int-i2b, bytes2int-ge-zero, bytes2int-first-pos, bytes2int-first-neq, bytes2int-fillsgn-zero, bytes2int-diff, bytes2int-append, bytes2int-1011x, bytes2int-100x-03, bytes2int-100x-02, bytes2int-100x-01, bytes2int-100x, bytes2int-011x-02, bytes2int-011x-01, bytes2int-011x, bytes2bytes-zero, bytes2bytes-other, bytes2bytes-mone, bytes2bytes-length, bytes2bytes-identity, bytes2bytes-fix, bytes2bytes-first-pos, bytes2bytes-first-neg, bytes2bits-one, bytes2bits-mklist-01, bytes2bits-mklist, bytes2bits-length, bytes2bits-empty-01, bytes2bits-append, bits2int-zero-ls, bits2int-pos, bits2bytes-rec-02, bits2bytes-rec-01, bits2bytes-mklist-03, bits2bytes-mklist-02, bits2bytes-mklist-01, bits2bytes-mklist, bits2bytes-len, bits2bytes-fill, bits2bytes-empty, bits2bytes-app, bits2bytes-2pot, bits2bits-sgn, bits2bits-inj, bits2bits-in,
• list/bitlista/a is used by no-leading-zero, int2bytes-rec-pos-any, int2bytes-rec-pos, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-rec-neg-01, int2bytes-minus-256, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-first-zerobyte, fix-value, fix-bits2bytes-01, fix-bits2bytes, bytes2int-zero-04, bytes2int-zero-02, bytes2int-rec, bytes2int-mone, bytes2int-len-one-01, bytes2int-append, bytes2bytes-zero, bytes2bytes-other, bytes2bytes-mone, bytes2bits-one, bytes2bits-mklist-01, bytes2bits-mklist, bytes2bits-length, bytes2bits-empty-01, bytes2bits-append, byte2bits-zero, byte2bits-mone, bits2int-zero-ls, bits2int-pos, bits2int-2pot, bits2bytes-rec-01, bits2bytes-mklist-02, bits2bytes-mklist-01, bits2bytes-mklist, bits2bytes-fill, bits2bytes-app, bits2bytes-2pot, bits2bits-sgn, bits2bits-in,
• list/bytelist/app is used by setShort-theorem-01, rightshift-8-02, no-leading-zeros, no-leading-zero-04, no-leading-zero-01, no-leading-zero, int2bytes-rec-neg-05, int2bytes-len-le-neg-03, int2bytes-len-le-neg-01, int2bytes-len-eq-pos, int2bytes-leading-zeros, int2bytes-first-neg-01, int2bytes-first-neg, fix-two-04, fix-two-03, fillsgn-short, bytes2int-zero-06, bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-04, bytes2int-size-03, bytes2int-size-02, bytes2int-size-01, bytes2int-size, bytes2int-rec-first-zero, bytes2int-neg, bytes2int-mklist-zeros-01, bytes2int-mklist-mones-01, bytes2int-len-one-02, bytes2int-int2bytes-len-eq, bytes2int-first-pos, bytes2int-fillsgn-zero, bytes2int-diff, bytes2int-1011x, bytes2int-100x-03, bytes2int-100x-02, bytes2int-100x-01, bytes2int-100x, bytes2int-011x-02, bytes2int-011x-01, bytes2int-011x, bytes2bytes-zero, bytes2bytes-mone, bytes2bytes-length, bytes2bytes-identity, bytes2bytes-fix, bytes2bytes-first-neg, bits2bytes-mklist-03, bits2bytes-mklist-01,
• list/bitlista/app is used by no-leading-zero, int2bytes-rec-pos-any, int2bytes-rec-pos, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-rec-neg-01, int2bytes-first-zerobyte, fix-bits2bytes-01, fix-bits2bytes, bytes2int-zero-04, bytes2int-zero-02, bytes2int-mone, bytes2bytes-zero, bytes2bytes-mone, bytes2bits-mklist-01, bytes2bits-mklist, byte2bits-zero, byte2bits-mone, bits2int-zero-ls, bits2bytes-rec-01, bits2bytes-mklist-02, bits2bytes-mklist-01, bits2bytes-mklist, bits2bytes-2pot,
• list/bitlista/app-01 is used by bytes2bits-mklist-01, bytes2bits-mklist, bytes2bits-append, byte2bits-zero, byte2bits-mone, bits2bits-sgn,
• list/bytelist/app-01 is used by setInt-theorem, no-leading-zero-04, no-leading-zero-01, no-leading-zero, int2bytes-rec255-neg, int2bytes-rec-pos-any, int2bytes-rec-pos-04, int2bytes-rec-pos-03, int2bytes-rec-pos-02, int2bytes-rec-pos-01, int2bytes-rec-neg-256-01, int2bytes-rec-neg-256, int2bytes-rec-neg-05, int2bytes-rec-neg-04, int2bytes-rec-neg-02, int2bytes-rec-neg-01, int2bytes-rec-case, int2bytes-minus-256-01, int2bytes-minus-256, int2bytes-leading-zeros, int2bytes-le255, int2bytes-byte-neg, fix-two-02, fix-two-01, fix-two, fix-rec-pos, fix-rec-neg, fix-bits2bytes-01, fix-bits2bytes, fillsgn-rec, fillsgn-fix, bytes2int-size-val, bytes2int-len-one-01, bytes2bytes-mone, bytes2bytes-fix, bits2bytes-rec-02, bits2bytes-mklist-03, bits2bytes-mklist-02, bits2bytes-mklist-01, bits2bytes-mklist, bits2bytes-app,
• list/bitlista/app-02-ant is used by no-leading-zero, int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, fix-bits2bytes-01, fix-bits2bytes, bytes2int-zero-04, bytes2int-rec, bytes2int-mone, bytes2int-append, bytes2bytes-zero, bytes2bytes-other, bytes2bits-empty-01, bits2int-zero-ls, bits2int-pos, bits2int-2pot, bits2bytes-mklist-02,
• list/bytelist/app-02-ant is used by no-leading-zero-04, no-leading-zero-02, no-leading-zero-01, no-leading-zero, int2bytes-leading-zeros, int2bytes-first-neg-01, int2bytes-first-neg, int2bytes-fillsgn-rec, int2bytes-empty, getInt-theorem, fix-rec-pos, fillsgn-rec, fillsgn-empty, fillsgn-butlast, bytes2int-rec-first-zero, bytes2int-neg-01, bytes2int-neg, bytes2int-mklist-zeros-01, bytes2int-mklist-mones-01, bytes2int-le-zero, bytes2int-ge-zero, bytes2int-first-neq, bytes2int-1011x, bytes2int-100x-03, bytes2int-100x-02, bytes2int-100x-01, bytes2int-100x, bytes2int-011x-02, bytes2int-011x-01, bytes2int-011x, bytes2bytes-other, bytes2bytes-length, bytes2bytes-identity, bytes2bytes-fix, bytes2bytes-first-neg, bits2bytes-empty,
• list/bytelist/app-03 is used by setInt-theorem, no-leading-zero-04, int2bytes-rec-pos-any, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-03, int2bytes-fillsgn-rec, fix-rec-pos, fix-rec-neg, fix-butlast-longer, fix-bits2bytes-01, fix-bits2bytes, fillsgn-rec, fillsgn-butlast, bytes2int-int2bytes-len-eq, bytes2int-diff, bytes2bytes-zero, bytes2bytes-other, bytes2bytes-mone, bits2bytes-rec-02, bits2bytes-fill, bits2bytes-app,
• list/bitlista/app-03 is used by bytes2bits-one, bytes2bits-mklist-01, bytes2bits-mklist,
• list/bytelist/app-04 is used by int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-len-le-neg-03, int2bytes-len-le-neg-01, fix-bits2bytes-01, bits2bytes-rec-01, bits2bytes-mklist-03,
• list/bytelist/app-05 is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, fix2rest-last, fix-rec-pos, fix-rec-neg, fix-pos-le, fix-neg-le, fix-bits2bytes-01, fix-bits2bytes, fillsgn-rec,
• list/bytelist/app-06 is used by setShort-theorem, setInt-theorem, no-leading-zero-04, no-leading-zero, bytes2int-int2bytes-len-eq,
• list/bitlista/c is used by int2bytes-rec-pos-any, int2bytes-rec-pos, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-minus-256, bytes2bytes-mone, bytes2bits-mklist-01, bits2int-pos, bits2bytes-fill,
• list/bytelist/c is used by setShort-theorem-01, setInt-theorem, rightshift-8-02, no-leading-zeros, no-leading-zero-03, no-leading-zero-02, no-leading-zero, int2bytes-rec255-neg, int2bytes-len-le-neg-03, int2bytes-len-le-neg-01, int2bytes-len-eq-pos, int2bytes-first-neg, fix2rest-last, fix-two-04, fix-two-03, fix-rec-pos, fix-rec-neg, fix-butlast-longer, fix-bits2bytes-01, fillsgn-short, fillsgn-rec, fillsgn-butlast, bytes2int-zero-06, bytes2int-size-val, bytes2int-pos, bytes2int-neg, bytes2int-mklist-zeros-01, bytes2int-mklist-mones-01, bytes2int-len-one-02, bytes2int-len-one-01, bytes2int-int2bytes-len-eq, bytes2int-first-pos-01, bytes2int-first-pos, bytes2int-fillsgn-zero, bytes2int-diff, bytes2bytes-zero, bytes2bytes-other, bytes2bytes-mone, bytes2bytes-length, bytes2bytes-identity, bytes2bytes-fix, bytes2bytes-first-neg, bytes2bits-length, bytes2bits-empty-01, bytes2bits-append, bits2int-zero-ls, bits2bytes-mklist-02,
• list/bytelist/c-03 is used by setShort-theorem-01, setInt-theorem, rightshift-8-02, no-leading-zeros, no-leading-zero-04, no-leading-zero-01, no-leading-zero, int2bytes-zero, int2bytes-len-one, int2bytes-len-le-neg-03, int2bytes-len-le-neg-01, int2bytes-len-eq-pos, int2bytes-leading-zeros, int2bytes-first-neg-01, int2bytes-first-neg, fillsgn-short, fillsgn-butlast, bytes2int-zero-06, bytes2int-mklist-mones-01, bytes2int-int2bytes-len-eq, bytes2int-diff,
• list/bytelist/c-04 is used by setShort-theorem, setInt-theorem, int2bytes-zero, int2bytes-rec255-neg, int2bytes-rec-pos-any, int2bytes-rec-pos-04, int2bytes-rec-pos-03, int2bytes-rec-pos-02, int2bytes-rec-pos-01, int2bytes-rec-neg-256, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-case, int2bytes-minus-one, int2bytes-len-one, int2bytes-leading-zeros, int2bytes-le255, int2bytes-le127, int2bytes-byte-neg, int2bytes-byte-01, int2bytes-byte, fix2rest-last, fix-one-01, fix-one, fix-butlast-longer, fix-bits2bytes-01, fillsgn-rec, bytes2int-int2bytes-len-eq, bytes2int-fillsgn-zero, bytes2bytes-zero, bytes2bytes-other, bytes2bytes-mone, bytes2bytes-identity, bytes2bytes-fix, bits2bytes-true, bits2bytes-rec-02, bits2bytes-mklist-03, bits2bytes-mklist-01, bits2bytes-fill,
• list/bytelist/c-05 is used by rightshift-8-02, int2bytes-zero, int2bytes-rec255-neg, int2bytes-minus-one, int2bytes-len-one, int2bytes-leading-zeros, fix2rest-last,
• list/bytelist/c-06 is used by setInt-theorem,
• list/bytelist/c-07 is used by no-leading-zero-03, int2bytes-rec255-neg, int2bytes-rec-pos-any, int2bytes-rec-pos-04, int2bytes-rec-pos-03, int2bytes-rec-neg-256, int2bytes-rec-neg-05, int2bytes-rec-neg-04, int2bytes-rec-neg-02, int2bytes-rec-neg-01, fix2rest-last, bytes2bytes-length, bytes2bytes-identity, bytes2bytes-fix, bytes2bytes-first-neg,
• list/bitlista/c-07 is used by int2bytes-rec-pos-any, int2bytes-rec-pos, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-rec-neg-01, bytes2bytes-mone, bits2int-pos,
• list/bytelist/c-08 is used by no-leading-zero-03, no-leading-zero-02, no-leading-zero, int2bytes-not-neg-01, int2bytes-not-neg, int2bytes-first-zerobyte, fix-rec-pos, fillsgn-rec, bytes2int-neg-01, bytes2int-neg, bytes2int-le-zero, bytes2int-ge-zero, bytes2int-first-neq, bytes2bytes-other, bytes2bytes-length, bytes2bytes-identity, bytes2bytes-fix, bytes2bytes-first-neg, bits2int-zero-ls,
• list/bitlista/c-08 is used by bytes2bytes-zero, bits2int-pos,
• list/bytelist/e is used by short-2bytes-03, short-2bytes, setInt-theorem, rightshift-8-02, no-leading-zeros, no-leading-zero-04, no-leading-zero-02, no-leading-zero-01, no-leading-zero, int2bytes-zero, int2bytes-len-one, int2bytes-leading-zeros, int2bytes-first-neg-01, int2bytes-first-neg, int2bytes-empty, getInt-theorem, fix-rec-pos, fix-rec-neg, fillsgn-short, fillsgn-rec, bytes2int-zero-03, bytes2int-zero-01, bytes2int-rec-first-zero, bytes2int-neg-01, bytes2int-neg, bytes2int-len-one-02, bytes2int-le-zero, bytes2int-ge-zero, bytes2int-first-neq, bytes2int-diff, bytes2int-2-le-32767, bytes2int-1011x, bytes2int-100x-03, bytes2int-100x-02, bytes2int-100x-01, bytes2int-100x, bytes2int-011x-02, bytes2int-011x-01, bytes2int-011x, bytes2bytes-other, bytes2bytes-mone, bytes2bytes-length, bytes2bytes-identity, bytes2bytes-fix, bytes2bytes-first-neg, bits2bytes-empty,
• list/bitlista/e is used by bytes2bytes-zero, bits2int-pos, bits2int-2pot, bits2bytes-mklist-02,
• list/bitlista/e-01 is used by int2bytes-rec-pos-any, int2bytes-rec-pos, int2bytes-first-zerobyte, bytes2bytes-zero, bits2int-pos, bits2bytes-mklist-02, bits2bytes-fill,
• list/bytelist/e-01 is used by setShort-theorem-01, setInt-theorem, no-leading-zeros, no-leading-zero-04, no-leading-zero-03, no-leading-zero-02, no-leading-zero-01, no-leading-zero, int2bytes-len-le-neg-03, int2bytes-len-le-neg-01, int2bytes-leading-zeros, int2bytes-first-neg-01, int2bytes-first-neg, getInt-theorem, fix2rest-last, fix-rec-pos, fix-rec-neg, fix-butlast-longer, fillsgn-short, fillsgn-rec, bytes2int-zero-06, bytes2int-rec-first-zero, bytes2int-pos, bytes2int-neg-01, bytes2int-neg, bytes2int-mklist-zeros-01, bytes2int-mklist-mones-01, bytes2int-len-one-02, bytes2int-len-one-01, bytes2int-le-zero, bytes2int-int2bytes-len-eq, bytes2int-ge-zero, bytes2int-fillsgn-zero, bytes2int-diff, bytes2int-1011x, bytes2int-100x-03, bytes2int-100x-02, bytes2int-100x-01, bytes2int-100x, bytes2int-011x-02, bytes2int-011x-01, bytes2int-011x, bytes2bytes-zero, bytes2bytes-other, bytes2bytes-mone, bytes2bytes-length, bytes2bytes-identity, bytes2bytes-fix, bytes2bytes-first-neg, bits2int-zero-ls,
• list/bytelist/e-02 is used by no-leading-zero-01, no-leading-zero, int2bytes-rec255-neg, int2bytes-leading-zeros, int2bytes-first-neg-01, int2bytes-first-neg, int2bytes-fillsgn-rec, fix2rest-last, fix-two-03, fillsgn-butlast, bytes2int-zero-03, bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-04, bytes2int-size-03, bytes2int-size-02, bytes2int-size-01, bytes2int-size, bytes2int-rec-first-zero, bytes2int-rec-01, bytes2int-neg, bytes2int-mklist-zeros-01, bytes2int-mklist-mones-01, bytes2int-len-one-02, bytes2int-len-one-01, bytes2int-int2bytes-len-eq, bytes2int-i2b, bytes2int-diff,
• list/bitlista/e-03 is used by no-leading-zero,
• list/bytelist/first is used by rightshift-8-01-01, int2bytes-rec-pos-any, int2bytes-not-neg, int2bytes-len-ls-01, int2bytes-first-zerobyte, bytes2bytes-other, bytes2bytes-mone, bytes2bytes-first-neg,
• list/bytelist/first-01 is used by fillsgn-butlast, bytes2int-mklist-zeros-01, bytes2int-mklist-mones-01, bytes2int-len-one-01, bytes2bytes-other, bytes2bytes-mone,
• list/bytelist/fr is used by int2bytes-len-eq-pos,
• list/bytelist/in-01 is used by int2bytes-leading-zeros, bytes2int-len-one-02,
• list/bitlista/in-06 is used by bytes2bytes-zero, bytes2bytes-mone, bits2bytes-mklist-02,
• list/bytelist/in-06 is used by int2bytes-first-neg, bytes2int-zero-06, bytes2int-len-one-02,
• list/bitlista/in-08 is used by bits2bits-in,
• list/bytelist/in-08 is used by bytes2int-zero-06, bytes2int-fillsgn-zero,
• list/bytelist/in-12 is used by no-leading-zero-04,
• list/bitlista/in-12 is used by bits2bits-in,
• list/bytelist/in-13 is used by no-leading-zeros, int2bytes-leading-zeros,
• list/bytelist/in-14 is used by setShort-theorem-01, setShort-theorem, setInt-theorem, rightshift-8-02, no-leading-zeros, no-leading-zero-04, no-leading-zero-01, no-leading-zero, int2bytes-rec255-neg, int2bytes-not-neg-01, int2bytes-len-le-neg-03, int2bytes-len-le-neg-01, int2bytes-len-eq-pos, int2bytes-leading-zeros, int2bytes-first-neg-01, int2bytes-first-neg, fix-two-03, fix-butlast-longer, fillsgn-short, bytes2int-size-val,
• list/bitlista/in-14 is used by int2bytes-rec-pos,
• list/bytelist/in-15 is used by setShort-theorem-01, setShort-theorem, setInt-theorem, no-leading-zero-04, no-leading-zero-01, no-leading-zero, int2bytes-leading-zeros, int2bytes-first-neg-01, int2bytes-first-neg, fix-two-03,
• list/bytelist/in-16 is used by no-leading-zero-04,
• list/bitlista/in-17 is used by bytes2bytes-zero, bytes2bytes-mone, bits2bytes-mklist-02,
• list/bytelist/in-17 is used by setShort-theorem-01, setShort-theorem, setInt-theorem, rightshift-8-02, no-leading-zeros, no-leading-zero-04, no-leading-zero-01, no-leading-zero, int2bytes-rec255-neg, int2bytes-leading-zeros, int2bytes-first-neg-01, int2bytes-first-neg, fix-butlast-longer, fillsgn-short, bytes2int-zero-03,
• list/bitlista/in-append is used by no-leading-zero, bytes2int-len-one-01, bytes2bytes-zero, bytes2bytes-other, bytes2bytes-mone, bits2bytes-mklist-02, bits2bits-in,
• list/bytelist/in-append is used by setShort-theorem-01, setShort-theorem, setInt-theorem, no-leading-zeros, no-leading-zero-04, no-leading-zero-01, no-leading-zero, int2bytes-rec255-neg, int2bytes-leading-zeros, int2bytes-first-neg-01, int2bytes-first-neg, fix-butlast-longer, bytes2int-zero-03,
• list/bitlista/in-empty is used by bytes2bytes-other, bytes2bytes-mone,
• list/bytelist/in-empty is used by bytes2int-zero-03,
• list/bytelist/inapp-02 is used by fix-butlast-longer,
• list/bytelist/inex is used by no-leading-zero-04,
• list/bytelist/len is used by setShort-theorem, setInt-theorem, rightshift-8-01, rightshift-8, no-leading-zeros, no-leading-zero-03, no-leading-zero, int2bytes-rec255-neg, int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-one, int2bytes-len-one-01, int2bytes-fillsgn-rec, fix2rest-last, fix-two-03, fix-two-02, fix-two-01, fix-rec-pos, fix-rec-neg, fix-length, fix-butlast-longer, fillsgn-rec, fillsgn-length, fillsgn-butlast, bytes2int-zero-06, bytes2int-zero-03, bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-04, bytes2int-size-03, bytes2int-size-02, bytes2int-size-01, bytes2int-size, bytes2int-rec-first-zero, bytes2int-rec-01, bytes2int-neg, bytes2int-mklist-zeros-01, bytes2int-mklist-mones-01, bytes2int-len-one-02, bytes2int-len-one-01, bytes2int-leading-zero, bytes2int-int2bytes-len-eq, bytes2int-first-pos, bytes2int-fillsgn-zero, bytes2int-diff, bytes2int-1011x, bytes2bytes-zero, bytes2bytes-other, bytes2bytes-mone, bytes2bytes-length, bytes2bytes-identity, bytes2bytes-fix, bytes2bytes-first-neg, bytes2bits-length, bits2bytes-len, bits2bytes-2pot,
• list/bitlista/len is used by int2bytes-rec-pos-any, int2bytes-rec-pos, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-minus-256, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-first-zerobyte, fix-bits2bytes-01, fix-bits2bytes, bytes2bytes-zero, bytes2bytes-other, bytes2bytes-mone, bytes2bits-length, bits2int-pos, bits2bytes-fill, bits2bytes-app, bits2bytes-2pot,
• list/bitlista/len-02 is used by int2bytes-rec-pos-any, int2bytes-rec-pos, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-minus-256, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-le255, int2bytes-first-zerobyte-01, int2bytes-first-zerobyte, fix-bits2bytes-01, bytes2bytes-zero, bytes2bytes-mone, bits2int-pos, bits2bytes-true, bits2bytes-fill, bits2bytes-2pot,
• list/bytelist/len-02 is used by setShort-theorem, setInt-theorem, rightshift-8-02, rightshift-8-01, rightshift-8, no-leading-zeros, no-leading-zero-03, no-leading-zero, int2bytes-rec255-neg, int2bytes-rec-pos-any, int2bytes-rec-pos-04, int2bytes-rec-neg-05, int2bytes-rec-neg-04, int2bytes-rec-neg-02, int2bytes-rec-neg-01, int2bytes-one, int2bytes-len-one-01, int2bytes-len-ls-01, int2bytes-len-le-neg-03, int2bytes-len-le-neg-01, int2bytes-len-eq-pos, int2bytes-fillsgn-rec, fix2rest-last, fix-two-04, fix-two-03, fix-two-02, fix-two-01, fix-two, fix-rec-pos, fix-rec-neg, fix-one, fix-butlast-longer, fillsgn-short, fillsgn-rec, fillsgn-butlast, bytes2int-zero-06, bytes2int-zero-03, bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-04, bytes2int-size-03, bytes2int-size-02, bytes2int-size-01, bytes2int-size, bytes2int-rec-first-zero, bytes2int-rec-01, bytes2int-neg, bytes2int-mklist-zeros-01, bytes2int-mklist-mones-01, bytes2int-len-one-02, bytes2int-len-one-01, bytes2int-leading-zero, bytes2int-int2bytes-len-eq, bytes2int-first-pos, bytes2int-fillsgn-zero, bytes2int-diff, bytes2int-1011x, bytes2bytes-zero, bytes2bytes-other, bytes2bytes-mone, bytes2bytes-length, bytes2bytes-identity, bytes2bytes-fix, bytes2bytes-first-neg, bytes2bits-length, bits2bytes-len, bits2bytes-2pot,
• list/bytelist/ni is used by no-leading-zero-04,
• list/bytelist/onein is used by int2bytes-len-le-neg-03, int2bytes-len-le-neg-01, int2bytes-len-eq-pos, bytes2int-zero-03,
• list/bytelist/rest is used by int2bytes-rec-neg-05,
• list/bitlista/rest is used by int2bytes-rec-neg-05, int2bytes-rec-neg-02,
• list/bytelist/rest-01 is used by bytes2bytes-mone,

Used from specification nat-basic2

• nat-basic2/c is used by int2bytes-len-ls-01, fix-bits2bytes-01, byte2bits-val,
• nat-basic2/a is used by setShort-theorem-01, setInt-theorem, rightshift-8-01-01, rightshift-8-01, rightshift-8, no-leading-zeros, no-leading-zero-03, no-leading-zero, int2bytes-rec255-neg, int2bytes-rec-pos-any, int2bytes-rec-pos, int2bytes-rec-neg-05, int2bytes-rec-neg-04, int2bytes-rec-neg-02, int2bytes-rec-neg-01, int2bytes-one, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-one-01, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-len-ls, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg, int2bytes-len-le-01, int2bytes-len-le, int2bytes-len-eq-pos, int2bytes-len-def, int2bytes-index-rightshift-02, int2bytes-index-rightshift, int2bytes-first-zerobyte-01, int2bytes-first-zerobyte, int2bytes-fillsgn-rec, int2bytes-bytes2int-length-01, int2bytes-byte, fix2rest-last, fix-value, fix-two-03, fix-rec-pos, fix-rec-neg, fix-length, fix-butlast-longer, fix-butlast, fix-bits2bytes-01, fix-bits2bytes, fillsgn-short, fillsgn-rec, fillsgn-length, fillsgn-fix, fillsgn-butlast, bytes2int-zero-06, bytes2int-zero-03, bytes2int-size-val-05, bytes2int-size-val, bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-04, bytes2int-size-03, bytes2int-size-02, bytes2int-size-01, bytes2int-size, bytes2int-rec-first-zero, bytes2int-rec-01, bytes2int-neg, bytes2int-mklist-zeros-01, bytes2int-mklist-zeros, bytes2int-mklist-mones-01, bytes2int-mklist-mones, bytes2int-len-one-02, bytes2int-len-one-01, bytes2int-int2bytes-len-eq, bytes2int-first-pos, bytes2int-fillsgn-zero, bytes2int-diff, bytes2int-1011x, bytes2int-100x-03, bytes2int-100x-02, bytes2int-100x-01, bytes2int-100x, bytes2int-011x-02, bytes2int-011x-01, bytes2int-011x, bytes2bytes-zero, bytes2bytes-other, bytes2bytes-mone, bytes2bytes-length, bytes2bytes-identity, bytes2bytes-fix, bytes2bytes-first-neg, bytes2bits-mklist-01, bytes2bits-mklist, bytes2bits-length, byte2bits-val, bits2int-pos, bits2bytes-rec-02, bits2bytes-rec-01, bits2bytes-mklist-03, bits2bytes-mklist-02, bits2bytes-mklist-01, bits2bytes-mklist, bits2bytes-len-02, bits2bytes-len-01, bits2bytes-len, bits2bytes-fill, bits2bytes-app, bits2bytes-2pot, bits2bits-sgn, bits2bits-inj, bits2bits-in,
• nat-basic2/c is used by setShort-theorem-01, setInt-theorem, rightshift-8-01-01, rightshift-8-01, rightshift-8, no-leading-zeros, no-leading-zero-03, no-leading-zero, int2bytes-rec255-neg, int2bytes-rec-pos-any, int2bytes-rec-pos, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-04, int2bytes-rec-neg-03, int2bytes-rec-neg-02, int2bytes-rec-neg-01, int2bytes-one, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-one-01, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-len-ls, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg, int2bytes-len-le-01, int2bytes-len-le, int2bytes-len-eq-pos, int2bytes-len-def, int2bytes-len-adjust, int2bytes-index-rightshift-02, int2bytes-index-rightshift, int2bytes-first-zerobyte-01, int2bytes-first-zerobyte, int2bytes-fillsgn-rec, int2bytes-bytes2int-length-01, int2bytes-byte, fix2rest-last, fix-value, fix-two-03, fix-rec-pos, fix-rec-neg, fix-length, fix-butlast-longer, fix-butlast, fix-bits2bytes-01, fix-bits2bytes, fillsgn-short, fillsgn-rec, fillsgn-length, fillsgn-fix, fillsgn-butlast, bytes2int-zero-06, bytes2int-zero-03, bytes2int-size-val-05, bytes2int-size-val, bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-04, bytes2int-size-03, bytes2int-size-02, bytes2int-size-01, bytes2int-size, bytes2int-rec-first-zero, bytes2int-rec-01, bytes2int-neg, bytes2int-mklist-zeros-01, bytes2int-mklist-zeros, bytes2int-mklist-mones-01, bytes2int-mklist-mones, bytes2int-len-one-02, bytes2int-len-one-01, bytes2int-int2bytes-len-eq, bytes2int-first-pos, bytes2int-fillsgn-zero, bytes2int-diff, bytes2int-1011x, bytes2int-100x-03, bytes2int-100x-02, bytes2int-100x-01, bytes2int-100x, bytes2int-011x-02, bytes2int-011x-01, bytes2int-011x, bytes2bytes-zero, bytes2bytes-other, bytes2bytes-mone, bytes2bytes-length, bytes2bytes-identity, bytes2bytes-fix, bytes2bytes-first-neg, bytes2bits-mklist-01, bytes2bits-mklist, bytes2bits-length, byte2bits-val, bits2int-pos, bits2bytes-rec-02, bits2bytes-rec-01, bits2bytes-mklist-03, bits2bytes-mklist-02, bits2bytes-mklist-01, bits2bytes-mklist, bits2bytes-len-02, bits2bytes-len-01, bits2bytes-len, bits2bytes-fill, bits2bytes-app, bits2bytes-2pot, bits2bits-sgn, bits2bits-inj, bits2bits-in,
• nat-basic2/eq is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-len-pos, int2bytes-len-def, fix-value, fix-two-03, fix-bits2bytes-01, bits2bytes-rec-01, bits2bytes-len-02, bits2bytes-fill,
• nat-basic2/eq-01 is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-def, int2bytes-first-zerobyte-01, int2bytes-fillsgn-rec, fix-bits2bytes-01, fix-bits2bytes, fillsgn-butlast, bytes2int-int2bytes-len-eq, bytes2int-diff, bytes2bytes-fix, bytes2bits-length, bits2bytes-len-02, bits2bytes-len, bits2bytes-2pot,
• nat-basic2/l is used by rightshift-8-01, int2bytes-rec-pos-any, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-01, fix-rec-pos, fix-rec-neg, fix-bits2bytes-01, fillsgn-rec, bytes2int-neg, bytes2bytes-other, bytes2bytes-length, bytes2bytes-fix, bits2bytes-rec-02, bits2bytes-rec-01, bits2bytes-app, bits2bytes-2pot,
• nat-basic2/l-01 is used by rightshift-8-01-01, int2bytes-rec-pos-any, int2bytes-rec-pos, int2bytes-rec-neg-05, int2bytes-byte, fix-value, fix-rec-pos, fix-rec-neg, fix-bits2bytes, fillsgn-rec, fillsgn-fix, bytes2bytes-zero, bytes2bytes-other, bytes2bytes-mone, bits2bytes-rec-02, bits2bytes-rec-01, bits2bytes-fill, bits2bytes-app,
• nat-basic2/l-02 is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-len-neg, int2bytes-len-le-neg-02, int2bytes-index-rightshift, fix-bits2bytes, fillsgn-butlast, bits2bytes-rec-02, bits2bytes-rec-01, bits2bytes-mklist-03, bits2bytes-mklist-02, bits2bytes-mklist, bits2bytes-fill, bits2bytes-app,
• nat-basic2/l-06 is used by int2bytes-len-ls-01,
• nat-basic2/l-07 is used by bits2bytes-rec-02,
• nat-basic2/neq-01 is used by int2bytes-rec-pos-any, fix-bits2bytes-01,
• nat-basic2/one is used by rightshift-8, no-leading-zeros, no-leading-zero, int2bytes-rec-pos, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-len-le-neg, int2bytes-len-le, int2bytes-first-zerobyte-01, int2bytes-fillsgn-rec, fix-butlast-longer, fillsgn-butlast, bytes2int-zero-06, bytes2int-zero-03, bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-04, bytes2int-size-03, bytes2int-size-02, bytes2int-size-01, bytes2int-size, bytes2int-rec-first-zero, bytes2int-rec-01, bytes2int-neg, bytes2int-mklist-zeros-01, bytes2int-mklist-mones-01, bytes2int-len-one-02, bytes2int-len-one-01, bytes2int-int2bytes-len-eq, bytes2int-first-pos, bytes2int-fillsgn-zero, bytes2int-diff, bytes2bytes-zero, bytes2bytes-mone, bytes2bytes-length, bytes2bytes-fix, bytes2bytes-first-neg, bits2bytes-len,
• nat-basic2/one-01 is used by int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, fix2rest-last,
• nat-basic2/one-03 is used by int2bytes-rec255-neg, int2bytes-rec-neg-05, int2bytes-rec-neg-04, int2bytes-rec-neg-02, int2bytes-rec-neg-01, int2bytes-one, int2bytes-len-one-01, int2bytes-len-neg-01, int2bytes-len-ls-01, fix2rest-last, bytes2int-zero-06, bytes2int-size-06, bytes2int-size-04, bytes2int-size-03, bytes2int-size-02, bytes2int-neg, bytes2int-mklist-zeros-01, bytes2int-int2bytes-len-eq, bytes2int-first-pos, bytes2int-fillsgn-zero, bytes2bytes-mone, bytes2bytes-length, bytes2bytes-identity, bytes2bytes-fix, bytes2bytes-first-neg,
• nat-basic2/oz is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-04, int2bytes-rec-neg-02, int2bytes-rec-neg-01, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-index-rightshift, int2bytes-first-zerobyte-01, int2bytes-fillsgn-rec, fix-rec-pos, fix-rec-neg, fix-butlast, fix-bits2bytes-01, fix-bits2bytes, fillsgn-rec, bytes2int-size-val, bytes2int-size-06, bytes2int-size-04, bytes2int-size-03, bytes2int-size-02, bytes2int-neg, bytes2int-mklist-zeros, bytes2int-mklist-mones, bytes2int-first-pos, bytes2int-fillsgn-zero, bytes2int-1011x, bytes2int-100x-03, bytes2int-100x-02, bytes2int-100x-01, bytes2int-100x, bytes2int-011x-02, bytes2int-011x-01, bytes2int-011x, bytes2bytes-length, bytes2bytes-identity, bytes2bytes-fix, bytes2bytes-first-neg, bits2int-pos,
• nat-basic2/pred is used by fix-butlast-longer, fix-butlast, bytes2int-mklist-zeros, bytes2int-mklist-mones, bytes2int-1011x, bytes2int-100x-03, bytes2int-100x-02, bytes2int-100x-01, bytes2int-100x, bytes2int-011x-02, bytes2int-011x-01, bytes2int-011x,
• nat-basic2/s is used by rightshift-8-01, no-leading-zero, int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-len-neg-01, int2bytes-len-ls-01, int2bytes-len-le-neg, int2bytes-len-le-01, int2bytes-len-le, int2bytes-index-rightshift, int2bytes-fillsgn-rec, int2bytes-bytes2int-length-01, fix-butlast-longer, fix-butlast, fix-bits2bytes-01, fix-bits2bytes, fillsgn-rec, fillsgn-butlast, bytes2int-zero-06, bytes2int-zero-03, bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-04, bytes2int-size-03, bytes2int-size-02, bytes2int-size-01, bytes2int-size, bytes2int-rec-first-zero, bytes2int-mklist-zeros-01, bytes2int-mklist-mones-01, bytes2int-int2bytes-len-eq, bytes2int-first-pos, bytes2int-fillsgn-zero, bytes2int-diff, bytes2bytes-zero, bytes2bytes-mone, bytes2bytes-first-neg, bits2bytes-mklist-02,
• nat-basic2/succ is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-len-neg-01, int2bytes-len-ls-01, int2bytes-index-rightshift-02, fillsgn-short, bytes2int-mklist-zeros, bytes2int-mklist-mones, bytes2int-1011x, bytes2int-100x-03, bytes2int-100x-02, bytes2int-100x-01, bytes2int-100x, bytes2int-011x-02, bytes2int-011x-01, bytes2int-011x, bytes2bits-mklist-01, bytes2bits-mklist, bits2bytes-rec-02, bits2bytes-rec-01, bits2bytes-mklist-03, bits2bytes-fill, bits2bytes-2pot,
• nat-basic2/succ-03 is used by int2bytes-rec-pos-any, int2bytes-len-pos, int2bytes-fillsgn-rec, fix-bits2bytes-01,
• nat-basic2/twols is used by fillsgn-short,
• nat-basic2/z is used by rightshift-8-01-01, int2bytes-rec-pos-any, int2bytes-rec-pos, int2bytes-rec-neg-05, int2bytes-rec-neg-04, int2bytes-rec-neg-02, int2bytes-rec-neg-01, int2bytes-len-pos-01, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-len-def, int2bytes-index-rightshift-02, int2bytes-index-rightshift, int2bytes-first-zerobyte-01, fix-bits2bytes-01, fix-bits2bytes, fillsgn-rec, bytes2int-size-val, bytes2bytes-zero, bytes2bytes-other, bytes2bytes-mone, byte2bits-val, bits2bytes-rec-02, bits2bytes-mklist-03, bits2bytes-len-01, bits2bytes-fill, bits2bytes-app,
• nat-basic2/z-01 is used by no-leading-zero-03, int2bytes-rec-pos-any, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-first-zerobyte-01, bytes2int-size-07, bytes2int-size-05, bytes2int-size-01, bytes2int-size, bytes2int-rec-first-zero, bytes2int-len-one-02, bits2bytes-fill,

Used from specification intnat

• intnat/Int2nat-pos is used by int2bytes-len-ls-01,
• intnat/add-01 is used by int2bytes-len-pos-01, int2bytes-len-neg-01, int2bytes-first-zerobyte-01,
• intnat/i2n-mult is used by int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-first-zerobyte-01,
• intnat/i2np is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-04, int2bytes-rec-neg-02, int2bytes-rec-neg-01,
• intnat/n2i-add is used by byte2bits-val,
• intnat/n2i-sub is used by int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-le-neg, int2bytes-len-le-01, int2bytes-len-le, int2bytes-len-eq-pos, int2bytes-index-rightshift-02,
• intnat/num-i2n-eq is used by rightshift-8-01,
• intnat/num-i2n-le-02 is used by int2bytes-len-neg-01, int2bytes-len-ls-01,
• intnat/num-i2n-ls is used by rightshift-8-01,
• intnat/num-n2i-eq is used by int2bytes-len-pos-01, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-first-zerobyte-01,
• intnat/num-n2i-ls-02 is used by int2bytes-len-neg-01, int2bytes-index-rightshift, band-65535-pos,
• intnat/num-n2i-ls-04 is used by int2bytes-len-neg-01, int2bytes-len-ls-01, int2bytes-len-le-neg-02, int2bytes-len-le-neg, int2bytes-len-le,
• intnat/num-n2i-ls-06 is used by int2bytes-index-rightshift-02,
• intnat/rax is used by int2bytes-rec-pos-any,
• intnat/rax-04 is used by int2bytes-rec-neg-05,
• intnat/sub is used by rightshift-8-01, int2bytes-len-pos, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-index-rightshift-02, int2bytes-index-rightshift,
• intnat/abs is used by rightshift-8-01,
• intnat/abs-02 is used by int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-first-zerobyte,
• intnat/abs-eq is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-len-neg, int2bytes-len-ls-01,
• intnat/abs-pred is used by int2bytes-len-ls-01,
• intnat/abs-succ-03 is used by int2bytes-rec-pos-any, int2bytes-rec-neg-06, int2bytes-rec-neg-05, int2bytes-rec-neg-04, int2bytes-rec-neg-03, int2bytes-rec-neg-02, int2bytes-rec-neg-01,
• intnat/abs-zero is used by rightshift-8-01-01, rightshift-8-01, int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-04, int2bytes-rec-neg-02, int2bytes-rec-neg-01, int2bytes-len-pos, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-index-rightshift-02, int2bytes-index-rightshift, int2bytes-first-zerobyte-01,
• intnat/add-nonneg-int-to-nat is used by int2bytes-len-le-neg-02, int2bytes-len-le-neg, int2bytes-len-le,
• intnat/i2i-pos is used by int2bytes-len-ls-01, int2bytes-index-rightshift-02,
• intnat/i2i-pos-01 is used by int2bytes-len-ls-01, int2bytes-index-rightshift, int2bytes-first-zerobyte-01,
• intnat/ini2-abs is used by rightshift-8-01-01, int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-len-pos,
• intnat/inj is used by int2bytes-len-neg-01,
• intnat/labs is used by rightshift-8-01, no-leading-zero-04, no-leading-zero-01, int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-not-neg, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-leading-zeros, int2bytes-first-zerobyte, int2bytes-first-neg-01, int2bytes-first-neg,
• intnat/labs-01 is used by rightshift-8-01, int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-len-ls-01,
• intnat/le is used by int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-le-01, int2bytes-len-eq-pos,
• intnat/le-int-le-nat is used by int2bytes-len-neg-01, int2bytes-len-le-neg-03, int2bytes-len-eq-pos,
• intnat/ls-int-ls-nat is used by int2bytes-len-le-neg-02, int2bytes-len-le-01, int2bytes-len-le, int2bytes-len-eq-pos,
• intnat/n2i-add is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05, int2bytes-rec-neg-02, int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-len-ls, int2bytes-len-le-neg, int2bytes-len-le, int2bytes-index-rightshift-02, int2bytes-index-rightshift, int2bytes-first-zerobyte-01, int2bytes-first-zerobyte, int2bytes-byte, bytes2int-size-val-05, bytes2int-size-val, bytes2int-size-07, bytes2int-size-06, bytes2int-size-05, bytes2int-size-04, bytes2int-size-03, bytes2int-size-02, bytes2int-size-01, bytes2int-size, bytes2int-rec-first-zero, bytes2int-1011x, bytes2int-100x-03, bytes2int-100x-02, bytes2int-100x-01, bytes2int-100x, bytes2int-011x-02, bytes2int-011x-01, bytes2int-011x,
• intnat/n2i-mult is used by int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-first-zerobyte-01, bytes2int-append, bytes2bits-nls, bytes2bits-nle,
• intnat/n2i-sub is used by int2bytes-len-le-neg-02, int2bytes-len-le-neg, int2bytes-index-rightshift-02,
• intnat/n2n is used by int2bytes-len-pos, int2bytes-len-ls-01, int2bytes-index-rightshift-02, int2bytes-index-rightshift-01, int2bytes-index-rightshift,
• intnat/nat2int is used by int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-ls-01, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-le, int2bytes-len-eq-pos, int2bytes-index-rightshift-02, int2bytes-index-rightshift-01, int2bytes-index-rightshift, int2bytes-first-zerobyte, bytes2int-size-07, bytes2int-size-06, bytes2int-size-04, bytes2int-size-03, bytes2int-size-02, bytes2int-size-01, bytes2int-rec-first-zero, bytes2int-append, bytes2int-1011x, bytes2int-100x-03, bytes2int-100x-02, bytes2int-100x-01, bytes2int-100x, bytes2int-011x-02, bytes2int-011x-01, bytes2int-011x, byte2bits-val, band-65535-pos,
• intnat/nat2int-02 is used by int2bytes-len-ls-01,
• intnat/nat2int-04 is used by int2bytes-len-le-neg-01, int2bytes-len-le-neg, int2bytes-len-eq-pos, int2bytes-index-rightshift-01,
• intnat/nat2int-05 is used by int2bytes-len-pos,
• intnat/nat2int-08 is used by int2bytes-len-eq-pos, int2bytes-first-zerobyte-01,
• intnat/nat2int-10 is used by int2bytes-len-pos, int2bytes-len-neg-01,
• intnat/nat2int-14 is used by int2bytes-len-neg-01, int2bytes-len-le-neg-03, int2bytes-byte,
• intnat/num-i2n-eq is used by int2bytes-rec-pos-any, int2bytes-len-pos-01, int2bytes-len-neg-01, int2bytes-first-zerobyte-01,
• intnat/num-i2n-eq-01 is used by rightshift-8-01,
• intnat/num-i2n-le is used by int2bytes-rec-pos-any,
• intnat/num-i2n-le-02 is used by int2bytes-rec-pos-any, int2bytes-len-neg, int2bytes-len-ls-01,
• intnat/num-i2n-ls is used by int2bytes-first-zerobyte-01,
• intnat/num-i2n-ls-01 is used by rightshift-8-01,
• intnat/num-i2n-ls-02 is used by int2bytes-rec-pos-any, int2bytes-rec-neg-05,
• intnat/num-n2i-eq is used by int2bytes-first-zerobyte,
• intnat/num-n2i-ls is used by int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-first-zerobyte,
• intnat/num-n2i-ls-02 is used by int2bytes-len-pos-01, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-len-ls-01, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-le-neg, int2bytes-len-le-01, int2bytes-len-le, int2bytes-len-eq-pos, int2bytes-index-rightshift-02, int2bytes-index-rightshift, int2bytes-first-zerobyte-01, band-65535-pos,
• intnat/num-n2i-ls-03 is used by int2bytes-len-pos,
• intnat/num-n2i-ls-06 is used by int2bytes-len-neg-01,
• intnat/num-n2i-ls-07 is used by int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, int2bytes-len-le-neg-01, int2bytes-len-le-neg, int2bytes-len-le, int2bytes-len-eq-pos, int2bytes-byte, bytes2int-size-05, bytes2int-size,
• intnat/rax-04 is used by int2bytes-len-pos-01, int2bytes-len-pos, int2bytes-len-neg-01, int2bytes-len-neg, int2bytes-index-rightshift,