Used simplifier rules/spec theorems by specification

Used from specification int-basic1

• int-basic1/lf-01 is used by getShort-isi, fits-law-shr,
• int-basic1/ls-rec is used by ubyte-max-01, byte-not-max,
• int-basic1/lsrec is used by ushort-max-05, ushort-band-shift, ushort-band-01, sis-neg-low, short-nle, short-ls, short-32767, byte-not-max, byte-mult-256, byte-ls-127, byte-law-neg, bib-neg-low,
• int-basic1/trans is used by short-nls, byte-size-01,
• int-basic1/forward-pos is used by ushort-short, ushort-pos-01, ushort-max-04, ushort-max-03, ushort-band-01, ubyte-max-02, ubyte-max, sis-pos-upper, sis-pos-low, sis-pos-high, sis-on-bits, sis-03, short-succ, short-size-01, short-size, short-overflow, short-ngr, short-mod-01, short-larger, short-in, short-ge, short-div256, short-div-max, short-add-max-01, short-32767, num-i2s-pos, num-i2l-pos, num-i2bi-pos, num-i2b-pos, mod-inshort, longin-mult-01, long-shiftzero-in, long-mod-pos-high, long-is-cast, long-band-add, long-automatic, lil-carry, issi-ubyte, inshort-01, getsetShort-theorem, fits-law-shr-01, fits-law-shr, fits-law-mod-01, fits-law-mod, fits-law-div-stronger, fits-law-div, div-inshort, byte-unsigned, byte-succ, byte-size-01, byte-size, byte-not-max, byte-ngr-01, byte-law-neg, byte-law-mult-one, byte-law-and-one, byte-law-add-pos, byte-law-add-one, byte-gr-127, byte-127, bint-unsigned-01, bint-unsigned, bint-trans-pos-03, bint-mod, bint-is-cast, bint-div2, bint-carry-01, bint-carry, bib-upper, bib-pos-low, bib-on-bits, bib-neg-high, bib-ls-same-01,
• int-basic1/irref is used by ushort-short, sis-ls-same-01, sis-ls-same, short-larger, short-in, byte-nge, bib-pos-high, bib-ls-same-01, bib-ls-same,
• int-basic1/lf-01 is used by getShort-isi, bib-pos-high,
• int-basic1/lf-03 is used by getShort-isi, bib-pos-high,
• int-basic1/ls-01 is used by ushort-pos-01, ushort-plus-01, ushort-band-shift, ushort-band-01, ubyte-zero-01, ubyte-max-02, sis-pos-upper, sis-pos-low, sis-neg-low, sis-neg-high, short-shift-pos, short-overflow, short-neq-01, short-mod-ngr, short-mod-add-02, short-max-11, short-max-05, short-max-02, short-larger, short-div-ngr, short-add-pos-02, short-add-pos-01, shiftright-byte-8-pos-01, shiftright-byte-8-neg-01, shiftright-byte-8-neg, mod-inshort, long-shiftzero-in, getsetShort-theorem, fits-law-shr-01, fits-law-mul, div-inshort, byte-not-max, byte-mult-neg, byte-mult-256, byte-mult, byte-law-neg, byte-law-and-one, bint-unsigned-01, bint-trans-pos-03, bint-trans-pos-02, bint-mod, bint-div2, bint-band-zero, bib-upper, bib-pos-low, bib-pos-high, bib-neg-low, bib-neg-high, bib-ls-same-01, band-011x-01,
• int-basic1/lst is used by ushort-pos-02, sis-sub-2pot, sis-pos-high, sis-on-bits, sis-neg-low, sis-neg-high, short-div256, longin-mult-01, long-is-cast, long-automatic, issi-ubyte, inshort-sis, getsetShort-theorem, fits-law-mod-01, fits-law-mod, byte-unsigned, byte-not-max, byte-mult-256, byte-law-neg, byte-law-mult-one, byte-law-add-one, bint-trans-pos-03, bint-trans-pos, bint-is-cast, bint-band-zero, bint-and-011x-bits2unit, bib-pos-low, bib-pos-high, bib-on-bits, bib-neg-low,
• int-basic1/lst-01 is used by ushort-max-05, ubyte-zero-01, ubyte-div-lsz, short-mod-max, short-mod-add, short-mod, short-max-11, short-div-ngr, mod-inshort, fits-law-mod-01, fits-law-mod, fits-law-div-stronger, div-inshort, byte-nle, byte-ngr-01, byte-127, bint-mod,
• int-basic1/lst-02 is used by short-max-11,
• int-basic1/numlsf is used by ushort-short, ushort-pos-02, ushort-band-shift, ushort-band-01, sis-on-bits, sis-neg-lower, sis-neg-low, sis-neg-high, sis-ls-same-01, sis-ls-same, short-range, short-nle-02, short-mod-01, short-min-03, short-min-01, short-min, short-add-min-03, short-add-min-02, short-add-min-01, num-i2l-neg, num-i2b-neg, mod-inshort, longin-mult-01, long-shiftzero-in, long-mod-neg-low, long-min-01, long-is-cast, long-band-add, long-band-11x, long-automatic, lil-carry, issi-ubyte, inshort-sis, getsetShort-theorem, getShort-isi, fits-law-shr-01, fits-law-shr, fits-law-mul, fits-law-mod-01, fits-law-mod, fits-law-div-stronger, fits-law-div, fits-law-band-02, fits-law-band-01, fits-law-add, div-inshort, byte-nls, byte-nle-02, byte-mult-neg, byte-min, byte-law-neg, byte-law-and-one, bint-mod, bint-is-cast, bint-div2, bint-carry-01, bint-carry, bint-band-one, bib-pos-low, bib-on-bits, bib-neg-low, bib-neg-high, bib-ls-same-01, bib-ls-same, bib-lower,
• int-basic1/numlslsdel is used by ushort-band-shift, ushort-band-01, sis-pos-high, sis-on-bits, sis-neg-low, sis-ls-same-01, sis-ls-same, short-succ-01, shiftright-byte-8-pos-01, num-i2l-neg, long-is-cast, getsetShort-theorem, byte-law-neg, bint-trans-pos-03, bint-mod, bint-is-cast, bib-pos-high, bib-on-bits, bib-neg-low, bib-ls-same-01, bib-ls-same,
• int-basic1/numlslsdel-01 is used by ushort-short, ushort-pos-01, ushort-max-04, ushort-max-03, ubyte-max-02, ubyte-max, sis-pos-low, sis-pos-high, sis-on-bits, sis-neg-low, sis-neg-high, sis-ls-same-01, sis-03, short-overflow, short-ngr, short-mod-01, short-larger, short-in, short-div256, short-div-max, short-add-max-01, short-32767, num-i2s-pos, num-i2l-pos, num-i2bi-pos, num-i2b-pos, mod-inshort, longin-mult-01, long-shiftzero-in, long-mod-pos-high, long-is-cast, long-band-add, long-automatic, lil-carry, issi-ubyte, inshort-01, getsetShort-theorem, fits-law-shr, fits-law-mod-01, fits-law-mod, fits-law-div-stronger, div-inshort, byte-not-max, byte-ngr-01, byte-mult-256, byte-law-neg, byte-law-mult-one, byte-law-add-pos, byte-law-add-one, byte-gr-127, byte-127, bint-mod, bint-is-cast, bint-carry-01, bib-upper, bib-pos-low, bib-pos-high, bib-on-bits, bib-neg-low, bib-neg-high, bib-ls-same-01,
• int-basic1/trans is used by getShort-isi,

Used from specification int-mult

• int-mult/commutativity is used by short-law-mult, byte-law-mult,
• int-mult/dist-rsplit is used by bib-neg-high,
• int-mult/dist-sub-split is used by ushort-band-shift, bib-neg-high,
• int-mult/minus-left is used by byte-mult-01,
• int-mult/modlsp-02 is used by getShort-isi,
• int-mult/mods-eq is used by ushort-band-01,
• int-mult/modzero-01 is used by ushort-band-01,
• int-mult/mult-gt-both is used by ubyte-mult,
• int-mult/numle-06 is used by getsetShort-theorem,
• int-mult/numls-06 is used by getsetShort-theorem,
• int-mult/one is used by ushort-band-shift,
• int-mult/ple-pos-better is used by longin-mult-01,
• int-mult/pnle-neg is used by fits-law-mul,
• int-mult/pnle-pos is used by fits-law-mul,
• int-mult/pnls-negpos is used by fits-law-mul,
• int-mult/pnls-posneg is used by fits-law-mul,
• int-mult/zero-ge-01 is used by fits-law-mul,
• int-mult/zero-ge-add is used by ushort-band-shift,
• int-mult/zero-ls is used by ushort-zero, ubyte-pos-02,
• int-mult/zero-ls-case is used by fits-law-mul,
• int-mult/Mult-zero is used by ubyte-pos-02, byte-law-mult-one,
• int-mult/add-mult-two is used by band-011x,
• int-mult/associativity is used by ushort-zero, ushort-pos-02, ushort-max-02, ushort-band-shift, ushort-band-01, ubyte-pos-02, sis-pos-low, sis-pos-high, sis-neg-low, sis-neg-high, sis-05, short-nls, short-neq-02, short-neq-01, short-max-11, longin-mult-mod, longin-mult-01, inshort-mult, getsetShort-theorem, getShort-isi, fits-law-shr, fits-law-mul, ex256, byte-mult-pos, byte-mult-neg, byte-mult-256-01, byte-mult-256, byte-mult, byte-law-mult-one, byte-law-add-pos, byte-law-add-one, bint-mult2, bib-pos-low, bib-pos-high, bib-neg-high, band-011x,
• int-mult/commutativity is used by ushort-zero, ushort-pos-02, ushort-max-02, ushort-band-shift, ushort-band-01, ubyte-pos-02, sis-pos-low, sis-pos-high, sis-neg-low, sis-neg-high, sis-05, short-nls, short-neq-02, short-neq-01, short-max-11, short-law-mult-one, short-law-mult, longin-mult-mod, longin-mult-01, inshort-mult, getsetShort-theorem, getShort-isi, fits-law-shr, fits-law-mul, ex256, byte-mult-pos, byte-mult-neg, byte-mult-256-01, byte-mult-256, byte-mult, byte-law-mult-one, byte-law-mult, byte-law-add-pos, byte-law-add-one, bint-mult2, bib-pos-low, bib-pos-high, bib-neg-low, bib-neg-high, band-011x,
• int-mult/dist-rmerge is used by byte-mult-256, byte-law-mult-one,
• int-mult/dist-sub-merge is used by byte-law-mult-one,
• int-mult/eq-dist is used by ushort-band-shift, ushort-band-01,
• int-mult/eq-neg is used by sis-neg-high, byte-law-mult-one, bib-neg-high,
• int-mult/eq-nonzero is used by ushort-band-shift,
• int-mult/eq-one is used by sis-neg-high,
• int-mult/eq-one-neg is used by bib-neg-high,
• int-mult/eq-pos is used by getsetShort-theorem, byte-mult-256,
• int-mult/eq-same is used by byte-mult-256,
• int-mult/eq-succ is used by getsetShort-theorem, byte-mult-256,
• int-mult/le-pos is used by longin-mult-01,
• int-mult/ls-same is used by bint-mult2,
• int-mult/minus-left is used by longin-mult-01, getShort-isi, byte-mult-256-01, byte-law-mult-one,
• int-mult/minus-one-01 is used by fits-law-shr,
• int-mult/modzero-01 is used by getShort-isi,
• int-mult/modzero-03 is used by inshort-mult, getShort-isi,
• int-mult/neq-two is used by sis-neg-high, bib-neg-high,
• int-mult/numleneg-02 is used by inshort-mult,
• int-mult/numleneg-03 is used by inshort-mult, fits-law-mul,
• int-mult/numlsneg-02 is used by longin-mult-01,
• int-mult/numlsneg-03 is used by longin-mult-01,
• int-mult/one is used by getsetShort-theorem,
• int-mult/pred-rmerge is used by ushort-band-shift, sis-neg-high, inshort-mult, getShort-isi,
• int-mult/succ-rmerge is used by ushort-band-shift, sis-neg-high, short-neq-02, getsetShort-theorem, getShort-isi, byte-mult-256,
• int-mult/two-zero is used by sis-neg-high, bib-neg-high, band-011x,
• int-mult/zero-eq is used by ushort-band-shift, byte-mult-256, byte-mult, bib-pos-low,
• int-mult/zero-ge is used by ushort-band-shift, fits-law-mul, byte-mult,
• int-mult/zero-ge-add is used by ushort-band-01, sis-pos-high, getsetShort-theorem, getShort-isi, byte-mult-256, byte-law-mult-one, byte-law-add-pos, byte-law-add-one, bib-pos-high,
• int-mult/zero-ge-add-01 is used by sis-pos-low, byte-mult-pos,
• int-mult/zero-gr is used by ushort-band-shift, sis-pos-low, short-neq-02, short-neq-01, longin-mult-01, bib-pos-low,
• int-mult/zero-gr-01 is used by longin-mult-01, fits-law-mul,
• int-mult/zero-gr-02 is used by longin-mult-01, fits-law-mul,
• int-mult/zero-le is used by ushort-band-shift, inshort-mult,
• int-mult/zero-ls is used by ushort-pos-02, ushort-band-shift, ushort-band-01, sis-neg-high, short-neq-01, getsetShort-theorem, getShort-isi, byte-mult-neg, byte-mult-256, byte-mult, bib-neg-high,
• int-mult/zero-ls-01 is used by longin-mult-01,
• int-mult/zero-ls-02 is used by longin-mult-01,
• int-mult/zero-ls-03 is used by ushort-zero,
• int-mult/zero-neq-01 is used by bib-neg-high,

Used from specification int-pot

• int-pot/ls-pos-2pot is used by short-size, cast-b2i-01,
• int-pot/two-le is used by shiftright-byte-8-pos-01,
• int-pot/abs-2pot is used by shiftright-byte-8-pos-01,
• int-pot/pot2-pos is used by short-size-01, short-size, fits-law-shr, byte-size-01, byte-size,
• int-pot/pot2-pos-01 is used by short-size-01, short-size, byte-size-01, byte-size,
• int-pot/two-zero is used by fits-law-shr,
• int-pot/zero is used by fits-law-shr,

Used from specification nat

• nat/add-num-03 is used by byte-law-and-one,
• nat/add-num-04 is used by byte-law-righthift-not, byte-law-and-one,
• nat/elim-pred-c is used by bib-pos-high,
• nat/elim-sub is used by byte-law-righthift-not,
• nat/eq-02 is used by short-size-01, bib-on-bits,
• nat/fle is used by fits-law-compl-01, byte-len, byte-law-righthift-not, byte-law-and-one, byte-bitlength-01,
• nat/fle-01 is used by byte-len, byte-law-righthift-not, byte-law-and-one,
• nat/l-num-04 is used by byte-law-and-one,
• nat/l-num-05 is used by byte-law-and-one,
• nat/le-ls-simp is used by sis-bitlength, byte-law-righthift-not, byte-law-and-one, bib-on-bits, bib-bitlength,
• nat/le-num-04 is used by byte-law-righthift-not,
• nat/le-num-05 is used by byte-law-righthift-not,
• nat/lels is used by sis-pos-low, num-i2l-pos, num-i2l-neg, long-is-cast, fits-law-band, byte-law-righthift-not, byte-law-and-one, bint-is-cast, bib-pos-low, bib-pos-high,
• nat/lels-01 is used by ushort-neg, ubyte-neg, sis-pos-low, sis-pos-high, sis-on-bits, sis-neg-low, sis-neg-high, sis-bitlength, short-size-01, short-size, long-shiftzero-in, fits-law-neg, fits-law-compl-01, fits-law-compl, fits-law-band, byte-length, byte-law-righthift-not, byte-law-and-one, byte-bitlength, bint-fillsgn-len, bib-pos-low, bib-pos-high, bib-on-bits, bib-neg-low, bib-neg-high, bib-bitlength,
• nat/lels-02 is used by sis-neg-low,
• nat/lels-03 is used by byte-law-righthift-not, byte-law-and-one,
• nat/lep is used by byte-law-and-one,
• nat/ler is used by byte-law-and-one,
• nat/let is used by byte-law-righthift-not, byte-law-and-one,
• nat/ls is used by sis-neg-low, short-size, bib-neg-low,
• nat/ls-01 is used by sis-neg-low,
• nat/ls-03 is used by byte-law-and-one,
• nat/ls-le-simp is used by byte-length, byte-law-and-one,
• nat/not-zero is used by sis-pos-low, sis-pos-high, sis-on-bits, sis-neg-low, fits-law-band, byte-law-righthift-not, byte-law-and-one, bib-pos-low, bib-on-bits, bib-neg-high,
• nat/pred-03 is used by sis-pos-low, sis-pos-high, sis-neg-low, bib-pos-high, bib-neg-low,
• nat/succ-01 is used by byte-law-and-one,
• nat/zero-01 is used by byte-law-and-one,

Used from specification intops

• intops/add-ones-lelen is used by byte-law-and-one,
• intops/and-com is used by byte-law-and-one,
• intops/and-notempty is used by byte-law-and-one,
• intops/and-sgn is used by byte-law-and-one,
• intops/band-011x-neg is used by short-011x-neg,
• intops/band-011x-neg-02 is used by bint-band-011x-neg, bint-and-011x-bits2unit,
• intops/band-011x-pos is used by bint-band-011x,
• intops/band-255-neg is used by ushort-band-shift,
• intops/band-255-pos is used by ushort-band-shift-01, ushort-band-shift, ushort-band-02, ushort-band-01, ushort-band, band-011x-01,
• intops/band-65535-pos is used by ushort-band-03,
• intops/band-bitlength is used by fits-law-band,
• intops/band-commutativity is used by bint-band-011x-neg, bint-band-011x, bint-and-011x-bits2unit,
• intops/band-def is used by getShort-isi, byte-law-and-one,
• intops/band-max-05 is used by fits-law-band-02, fits-law-band-01,
• intops/band-max-06 is used by fits-law-band-02, fits-law-band-01,
• intops/band-min-02 is used by fits-law-band-02, fits-law-band-01,
• intops/band-notneg is used by fits-law-band-02, fits-law-band-01,
• intops/band-notneg-01 is used by fits-law-band-02, fits-law-band-01,
• intops/band-num is used by byte-law-and-one,
• intops/bcompl-size is used by fits-law-compl,
• intops/bits2int-is-cast is used by num-i2l-pos, num-i2l-neg, long-is-cast, bint-is-cast,
• intops/bits2int-is-cast-01 is used by long-on-bits,
• intops/bitsand-app is used by byte-law-and-one,
• intops/bitsand-app-false is used by byte-law-and-one,
• intops/bitsand-app-true is used by byte-law-and-one,
• intops/bitsand-fillsgn is used by byte-law-and-one,
• intops/bitsand-len-false is used by byte-law-and-one,
• intops/bitsand-len-true is used by byte-law-and-one,
• intops/bitsand-rec is used by getShort-isi,
• intops/bor-256-plus is used by getShort-isi,
• intops/bor-256-plus-01 is used by getShort-isi,
• intops/bor-notAndNot is used by fits-law-bor-02, fits-law-bor-01, fits-law-bor,
• intops/bor-shift-plus is used by getsetShort-theorem,
• intops/bxor-def-logic is used by fits-law-bxor-02, fits-law-bxor-01, fits-law-bxor,
• intops/cast-def is used by short-is-cast, byte-is-cast-01, byte-is-cast,
• intops/cast-if is used by long-automatic, bint-unsigned-01,
• intops/cast-law-absorption is used by byte-sis, byte-short-neq,
• intops/cast-law-add-one is used by short-law-compl, short-law-add-one,
• intops/cast-law-and-one is used by short-law-and-one,
• intops/cast-law-leftshift is used by short-law-leftshift, byte-law-leftshift,
• intops/cast-law-mult-one is used by short-law-mult-one,
• intops/cast-law-neg is used by short-law-neg, short-law-compl,
• intops/cast-law-or-one is used by short-law-or-one,
• intops/cast-law-shift-snd-l is used by short-law-shift-snd-l,
• intops/cast-law-shift-snd-r is used by short-law-shift-snd-r,
• intops/cast-law-shift-snd-zr is used by short-law-shift-snd-rz,
• intops/cast-law-sub-one is used by short-law-sub-one,
• intops/cast-law-sub-one-01 is used by short-law-sub-one-01,
• intops/cast-law-xor-one is used by short-law-xor-one,
• intops/cast-mod-in is used by long-is-cast, bint-num-in, bint-is-cast,
• intops/cast-mod-neg-high is used by long-mod-neg-high,
• intops/cast-mod-neg-low is used by long-mod-neg-low,
• intops/cast-mod-pos-high is used by long-mod-pos-high,
• intops/cast-mod-pos-low is used by long-mod-pos-low,
• intops/cast-mult-add is used by short-mult-65536,
• intops/cast-nls is used by long-is-cast, bint-is-cast,
• intops/cast-nls-01 is used by long-is-cast, bint-is-cast,
• intops/cast-size-fits is used by sis-bitlength, fits-law-neg, fits-law-compl-01, fits-law-compl, fits-law-band, bib-bitlength,
• intops/cast-size-fits-01 is used by cast-b2i-01,
• intops/intshiftleft is used by getShort-isi,
• intops/intshiftright-ls-01 is used by fits-law-shr-01,
• intops/intshiftright-ls-02 is used by fits-law-shr-01,
• intops/intshiftright-unbounded-same is used by getsetShort-theorem,
• intops/intshiftrsign-2pot-neg is used by ushort-band-shift,
• intops/intshiftrsign-2pot-neg-01 is used by fits-law-shr,
• intops/intshiftrsign-2pot-neg-02 is used by ushort-band-shift,
• intops/intshiftrsign-2pot-pos is used by ushort-band-shift-01, ushort-band-shift, fits-law-shr,
• intops/intshiftrsign-abs-le is used by fits-law-shr-01,
• intops/intshiftrsign-band31 is used by fits-law-shr-01, fits-law-shr,
• intops/intshiftrsign-neg-01 is used by getsetShort-theorem,
• intops/intshiftrsign-neg-02 is used by getsetShort-theorem,
• intops/intshiftrsign-pos-8 is used by short-shift-pos, getsetShort-theorem,
• intops/intshiftrzero-def is used by short-law-righthift-not, byte-law-righthift-not,
• intops/longshiftzero-carry-01 is used by bint-carry-01,
• intops/longshiftzero-def-unbounded is used by long-shiftzero-in,
• intops/longshiftzero-not-neg is used by bint-carry-01,
• intops/longshiftzero-not-neg-01 is used by long-shiftzero-in,
• intops/shiftright-is-le is used by long-shiftzero-in,
• intops/shiftright-pos-div is used by shiftright-byte-8-pos-01, getsetShort-theorem,
• intops/shiftright-rec-8 is used by shiftright-byte-8-pos,
• intops/shiftright-rec-8-neg is used by shiftright-byte-8-neg-01, shiftright-byte-8-neg, getsetShort-theorem,
• intops/shiftzero-max-neg is used by long-shiftzero-in,
• intops/shiftzero-pos is used by long-shiftzero-in,
• intops/and-notempty-02 is used by byte-law-and-one,
• intops/and-notempty-09 is used by byte-law-and-one,
• intops/and-rec-07 is used by short-law-righthift-not, getShort-isi, byte-law-righthift-not,
• intops/and-zero-01 is used by getShort-isi,
• intops/band-255-neg is used by ushort-band-01, ushort-band, byte-011x-neg, byte-011x-ib,
• intops/band-255-pos is used by ushort-band-shift, ushort-band-01, byte-and-255, byte-011x-pos, band-ff,
• intops/band-63-lezero is used by long-shiftzero-in,
• intops/band-65535-pos is used by short-011x-pos,
• intops/band-associativity is used by ushort-band-shift, ushort-band-03, ushort-band-01, ushort-band, ubyte-band, short-mask, short-law-righthift-not, short-011x-pos, long-shiftzero-in, long-band-add, long-band-11x, lil-carry, getsetShort-theorem, getShort-isi, fits-law-shr-01, fits-law-shr, fits-law-band-02, fits-law-band-01, byte-law-righthift-not, byte-and-lsz, byte-and-le-256, byte-and-255, byte-011x-unsgn, byte-011x-pos-02, byte-011x-pos-01, byte-011x-pos, byte-011x-neg, byte-011x-ib, bint-carry-01, bint-carry, bint-band-one-01, bint-band-one, bint-band-and-nlsz, band-ff, band-011x, Byte-and-range,
• intops/band-commutativity is used by ushort-band-shift-01, ushort-band-shift, ushort-band-03, ushort-band-01, ushort-band, ubyte-band, short-mask, short-law-righthift-not, short-law-and-one, short-011x-pos, long-shiftzero-in, long-band-add, long-band-11x, lil-carry, getsetShort-theorem, getShort-isi, fits-law-shr-01, fits-law-shr, fits-law-bxor-02, fits-law-bxor-01, fits-law-bxor, fits-law-bor-02, fits-law-bor-01, fits-law-bor, fits-law-band-02, fits-law-band-01, fits-law-band, byte-law-righthift-not, byte-law-and-one, byte-and-lsz, byte-and-le-256, byte-and-255, byte-011x-unsgn, byte-011x-pos-02, byte-011x-pos-01, byte-011x-pos, byte-011x-neg, byte-011x-ib, bint-carry-01, bint-carry, bint-band-one-01, bint-band-one, bint-band-and-nlsz, band-ff, band-bib, band-011x-01, band-011x, Byte-and-range,
• intops/band-max-02 is used by long-band-add, long-band-11x, lil-carry,
• intops/band-max-04 is used by ubyte-band, getsetShort-theorem, byte-and-le-256, Byte-and-range,
• intops/band-max-05 is used by fits-law-shr-01, fits-law-shr, bint-band-one,
• intops/band-neg is used by fits-law-band-02, fits-law-band-01,
• intops/band-notneg is used by ushort-band, ubyte-band, short-mask, long-band-add, long-band-11x, lil-carry, getsetShort-theorem, fits-law-shr-01, fits-law-shr, byte-and-lsz, bint-band-one, bint-band-and-nlsz, band-011x, Byte-and-range,
• intops/band-num is used by short-law-righthift-not, byte-law-righthift-not,
• intops/bcompl-size-01 is used by fits-law-compl-01,
• intops/bitsand-zerol is used by short-law-righthift-not, byte-law-righthift-not,
• intops/cast-cast is used by short-is-cast-01, long-is-cast-01, long-eq, bint-is-cast-01,
• intops/cast-zero is used by fits-law-neg,
• intops/compl-def is used by short-law-compl, byte-law-compl,
• intops/intshiftrsign-num is used by short-law-righthift-not, byte-law-righthift-not,
• intops/intshiftrsign-zero is used by fits-law-shr,
• intops/longshiftzero-carry is used by bint-carry,
• intops/longshiftzero-carry-01 is used by bint-carry,
• intops/longshiftzero-zero-01 is used by long-shiftzero-in,
• intops/rightshift-zero is used by shiftright-byte-8-pos, shiftright-byte-8-neg, getsetShort-theorem,
• intops/shiftright-minus-one is used by shiftright-byte-8-neg-01,
• intops/shiftzero-zero is used by long-shiftzero-in,

Used from specification int-abs

• int-abs/Abs-neg is used by ushort-band-shift, ushort-band-01, longin-mult-01, fits-law-mod-01, fits-law-mod, div-inshort, byte-nle-01, byte-nle, byte-ngr-01, bint-mod, bib-neg-high,
• int-abs/Abs-pos is used by ushort-short, short-mod-max, short-mod-add, short-mod, fits-law-shr-01, fits-law-div-stronger, band-011x,
• int-abs/absle-01 is used by fits-law-shr-01,
• int-abs/estimate-add1-ls-left is used by fits-law-add, byte-nls-02,
• int-abs/estimate-add2-le-right is used by fits-law-add,
• int-abs/forward-lele is used by short-nle-03, getsetShort-theorem,
• int-abs/forward-lels is used by longin-mult-01, fits-law-div-stronger,
• int-abs/forward-lsle is used by ushort-max-03, short-nls-01,
• int-abs/le-def is used by ushort-max-05, ushort-max-04, ubyte-mult, ubyte-max-01, short-nle, short-add-min,
• int-abs/le-rew-succ is used by getsetShort-theorem, cast-b2i-01,
• int-abs/ls-rew-succ is used by longin-mult-01, fits-law-div-stronger, div-inshort,
• int-abs/mone-07 is used by sis-neg-high,
• int-abs/ple is used by long-band-add, lil-carry,
• int-abs/ple-01 is used by short-add-min,
• int-abs/ple-04 is used by short-add2,
• int-abs/pls-01 is used by ushort-band-shift,
• int-abs/rew-eqzero is used by short-neq-01,
• int-abs/rew-eqzero-01 is used by short-neq-01,
• int-abs/sub-add-01 is used by ushort-band-shift,
• int-abs/zero-ge-01 is used by byte-mult-neg,
• int-abs/zero-gs is used by long-band-add, bint-band-and-nlsz,
• int-abs/Abs-pos is used by ushort-band-shift, ushort-band-01, longin-mult-01, fits-law-mod-01, fits-law-mod, div-inshort, byte-nle-01, byte-nle, byte-ngr-01, bint-mod, bib-neg-high,
• int-abs/Sub-def is used by ushort-pos-01, ushort-band-shift, ushort-band-01, ubyte-pos-03, sis-pos-upper, sis-pos-high, sis-neg-high, short-sub-pos, short-larger, long-mod-pos-high, long-automatic, fits-law-sub, fits-law-shr, byte-size, byte-not-max, byte-mult-pos, byte-mult-256, byte-law-sub-one-01, byte-law-sub-one, byte-law-neg, byte-law-compl, byte-011x-unsgn, bint-unsigned-01, bint-unsigned, bib-upper, bib-pos-high, bib-neg-high,
• int-abs/abs-03 is used by ushort-short, ushort-band-shift, short-mod-max, short-mod-add, short-mod, longin-mult-01, div-inshort, byte-nle-01, byte-nle,
• int-abs/abs-05 is used by short-011x-neg, fits-law-shr, bint-band-011x-neg, bint-and-011x-bits2unit,
• int-abs/abs-06 is used by ushort-short, ushort-band-shift, short-mod-max, short-mod-add, short-mod, longin-mult-01, fits-law-shr-01, fits-law-mod-01, fits-law-mod, fits-law-div-stronger, div-inshort, byte-nle-01, byte-nle, byte-ngr-01, bint-mod,
• int-abs/abs-08 is used by ushort-pos-02, ushort-band-shift, sis-neg-lower, sis-neg-low, sis-neg-high, sis-ls-same-01, sis-ls-same, short-mod-max, short-mod-add, short-mod, short-011x-neg, shiftright-byte-8-neg-01, shiftright-byte-8-neg, longin-mult-01, fits-law-shr-01, fits-law-shr, fits-law-div-stronger, div-inshort, byte-mult-256, byte-law-mult-one, byte-law-add-one, bint-band-011x-neg, bint-and-011x-bits2unit, bib-neg-low, bib-neg-high, bib-ls-same-01, bib-ls-same, bib-lower, band-011x,
• int-abs/abs-16 is used by ushort-short, sis-ls-same, longin-mult-01, fits-law-shr-01, bib-pos-high, bib-ls-same-01, bib-ls-same,
• int-abs/abs-18 is used by ushort-abs, ubyte-abs,
• int-abs/absle is used by sis-pos-low, sis-neg-high, sis-ls-same, shiftright-byte-8-pos-01, shiftright-byte-8-pos, long-shiftzero-in, getShort-isi, bint-band-011x, bib-pos-low, bib-pos-high, bib-ls-same-01, bib-ls-same,
• int-abs/anti is used by ushort-pos-02, ushort-band-shift, ushort-band-01, sis-sub-2pot, sis-pos-low, sis-pos-high, sis-on-bits, sis-neg-low, sis-neg-high, short-size-02, short-size, short-neq-01, short-max-11, longin-mult-01, getShort-isi, cast-b2i-01, byte-mult-256, byte-law-neg, bint-succ-notin, bint-fillsgn-len, bib-pos-low, bib-pos-high, bib-neg-low, bib-neg-high,
• int-abs/bet is used by lil-carry,
• int-abs/bet-01 is used by fits-law-neg,
• int-abs/elim-sub is used by sis-sub-2pot, short-larger, getsetShort-theorem, cast-b2i-01, byte-mult-256, byte-law-add-pos, byte-law-add-one, bint-pred-02, bint-pred-01, bint-pred,
• int-abs/forward-le is used by ushort-short, ushort-max-06, ushort-max-05, ushort-max-02, ushort-max, ushort-band-shift, ushort-band-01, ushort-band, ubyte-mult, ubyte-mod, ubyte-max-01, sis-pos-upper, short-mod-ngr, short-mod-max, short-mod-add, short-mod, short-max-11, short-max-07, short-max-06, short-max-01, short-larger, short-div-ngr, short-div-max-01, short-add2, short-add-max, shiftright-byte-8-pos-01, shiftright-byte-8-neg-01, long-shiftzero-in, long-is-cast, long-band-add, inshort-le-num, getsetShort-theorem, fits-law-shr-01, fits-law-mul, fits-law-div-stronger, fits-law-band-02, fits-law-band-01, fits-law-add, cast-b2i-01, byte-unsigned, byte-succ, byte-nls-02, byte-nle-01, byte-nle, byte-ngr, byte-nge, byte-law-and-one, bint-unsigned-01, bint-unsigned, bint-trans-pos, bint-pred-01, bint-pred, bint-num-03, bint-num, bint-div2-01, bint-div2, bib-ls-same-01, band-011x-01,
• int-abs/forward-le-01 is used by ushort-short, ushort-pos-02, ushort-pos-01, ushort-pos, ushort-plus-01, ushort-plus, ushort-max-06, ushort-max-05, ushort-max-02, ushort-max, ushort-inj, ushort-band-shift-01, ushort-band-shift, ushort-band-01, ushort-band, ubyte-pos-03, ubyte-pos, ubyte-mult, ubyte-mod, ubyte-max-01, ubyte-inj, sis-sub-2pot, sis-pos-upper, sis-pos-low, sis-pos-high, sis-neg-high, sis-ls-same-01, sis-ls-same, sis-05, sis-03, short-succ-pos, short-sub-pos, short-overflow, short-neq-01, short-mod-ngr, short-mod-max, short-mod-add-01, short-mod-add, short-mod, short-max-11, short-max-07, short-max-06, short-max-04, short-max-03, short-max-01, short-larger, short-in, short-div-ngr, short-div-max-01, short-add2, short-add-pos-01, short-add-pos, short-add-min-02, short-add-max, short-32767, shiftright-byte-8-pos-01, shiftright-byte-8-pos, shiftright-byte-8-neg-01, mod-inshort, long-shiftzero-in, long-mod-pos-low, long-mod-pos-high, long-is-cast, long-automatic, lil-carry, inshort-le-num, inshort-01, getsetShort-theorem, fits-law-shr-01, fits-law-shr, fits-law-neg, fits-law-mul, fits-law-mod-01, fits-law-mod, fits-law-div-stronger, fits-law-band-02, fits-law-band-01, fits-law-add, div-inshort, cast-b2i-01, byte-unsigned, byte-succ, byte-nls-02, byte-nle-01, byte-nle, byte-ngr, byte-nge, byte-mult-pos, byte-mult-neg, byte-mult-256, byte-law-neg, byte-law-mult-one, byte-law-and-one, byte-law-add-pos, byte-law-add-one, byte-in, byte-127, byte-011x-unsgn, byte-011x-pos-01, bint-unsigned-01, bint-unsigned, bint-trans-pos-02, bint-trans-pos-01, bint-pred-02, bint-pred-01, bint-pred, bint-num-03, bint-num, bint-carry, bint-band-011x, bib-pos-low, bib-ls-same-01, bib-ls-same, band-011x-01,
• int-abs/forward-le-02 is used by ushort-zero-02, ushort-zero-01, ushort-zero, ushort-short, ushort-pos-02, ushort-pos-01, ushort-plus-01, ushort-plus, ushort-nlsz, ushort-neg, ushort-inj, ushort-band-shift, ushort-band-01, ushort-band, ubyte-pos-03, ubyte-pos-02, ubyte-pos-01, ubyte-neg, ubyte-inj, sis-sub-2pot, sis-neg-low, sis-neg-high, sis-ls-same-01, sis-ls-same, short-succ-01, short-neq-02, short-neq-01, short-mod-ngr, short-mod-add-01, short-mod-add, short-max-11, short-div-ngr, short-add-min-02, short-add-max-01, short-011x-neg, shiftright-byte-8-neg-01, shiftright-byte-8-neg, mod-inshort, longin-mult-01, long-shiftzero-in, long-mod-neg-low, long-mod-neg-high, long-automatic, getsetShort-theorem, fits-law-shr-01, fits-law-shr, fits-law-mul, fits-law-mod-01, fits-law-mod, fits-law-div-stronger, fits-law-band-02, fits-law-band-01, div-inshort, cast-b2i-01, byte-nls-02, byte-mult-neg, byte-mult-256, byte-law-mult-one, byte-law-and-one, byte-law-add-one, byte-011x-unsgn, bint-band-zero, bint-band-and-nlsz, bint-band-011x-neg, bint-and-011x-bits2unit, bib-on-bits, bib-neg-low, bib-neg-high, bib-ls-same-01, bib-ls-same,
• int-abs/forward-le-03 is used by ushort-band-shift, sis-neg-high, short-nle-01, short-nle, short-neq-02, short-mod-add, short-min-02, short-add-min, long-min-01, byte-nls-01, bint-num-02, bib-neg-low,
• int-abs/forward-le-04 is used by ushort-zero-02, ushort-band-shift, ushort-band-01, ubyte-zero-01, sis-sub-2pot, sis-on-bits, sis-neg-low, sis-neg-high, sis-ls-same-01, sis-ls-same, short-size-02, short-size, short-nle-01, short-nle, short-neq-02, short-neq-01, short-neq, short-mod-add, short-min-02, short-add-min, short-011x-neg, long-min-01, long-is-cast, getsetShort-theorem, fits-law-shr-01, fits-law-shr, fits-law-div-stronger, div-inshort, byte-nls-01, byte-mult-256, byte-law-mult-one, byte-law-add-one, byte-and-255, bint-num-02, bint-is-cast, bint-fillsgn-len, bib-on-bits, bib-neg-low, bib-neg-high, bib-ls-same-01, bib-ls-same,
• int-abs/forward-le-05 is used by ushort-zero-02, ushort-zero-01, ushort-short, ushort-pos-01, ushort-plus-01, ushort-max-04, ushort-max-03, ushort-band-shift, ushort-band, ubyte-zero-01, ubyte-zero, ubyte-pos-03, ubyte-max-02, ubyte-max, sis-sub-2pot, sis-pos-low, sis-pos-high, sis-on-bits, sis-ls-same, sis-03, short-succ-pos, short-succ, short-size-01, short-size, short-shift-pos, short-overflow, short-not-max, short-nls, short-ngr, short-neq-02, short-neq-01, short-mod-add-02, short-mod-01, short-max-11, short-max-05, short-max-02, short-larger, short-in, short-ge, short-div256, short-div-max-01, short-div-max, short-add-pos-02, short-add-pos-01, short-add-max-01, short-32767, shiftright-byte-8-neg-01, shiftright-byte-8-neg, num-i2s-pos, num-i2l-pos, num-i2bi-pos, num-i2b-pos, mod-inshort, longin-mult-01, long-shiftzero-in, long-mod-pos-high, long-is-cast, long-band-add, long-automatic, lil-carry, issi-ubyte, inshort-01, getsetShort-theorem, fits-law-shr-01, fits-law-shr, fits-law-mul, fits-law-mod-01, fits-law-mod, fits-law-div-stronger, fits-law-div, div-inshort, byte-succ, byte-size-01, byte-size, byte-not-max, byte-ngr-01, byte-mult-256, byte-law-neg, byte-law-mult-one, byte-law-and-one, byte-law-add-pos, byte-law-add-one, byte-gr-127, byte-127, byte-011x-unsgn, byte-011x-pos-01, bint-trans-pos-03, bint-trans-pos-02, bint-trans-pos, bint-pred-01, bint-pred, bint-mult2, bint-mod, bint-is-cast, bint-div2-01, bint-div2, bint-carry-01, bint-carry, bib-upper, bib-pos-low, bib-on-bits, bib-neg-high, bib-ls-same-01, bib-ls-same, band-011x-01,
• int-abs/forward-lele is used by ushort-inj, ushort-band-shift, ushort-band-01, sis-pos-low, sis-pos-high, sis-on-bits, sis-ls-same, short-sub-pos, short-size-02, short-size, short-mod, short-max-07, short-max-01, short-add2, short-011x-neg, shiftright-byte-8-pos-01, num-issi, num-illi, num-ibbi, num-i2b-equal, notequal-01, notequal, longin-mult-mod-01, longin-mult-01, longin-mult, long-is-cast, l2i-bint, getsetShort-theorem, fits-law-shr-01, fits-law-neg, fits-law-div, fits-law-bxor-02, fits-law-bxor-01, fits-law-bxor, byte-nge, byte-law-neg, bor-sis, bor-bib, bint-trans-pos-03, bint-trans-pos-02, bint-trans-pos-01, bint-trans-pos, bint-succ-notin, bint-num-03, bint-num-02, bint-num, bint-mod, bint-is-cast, bint-fillsgn-len, bint-div2, bint-band-zero, bint-and-011x-bits2unit, bib-pos-low, bib-pos-high, bib-on-bits, bib-neg-high, bib-ls-same, bcompl-sis, bcompl-bib, band-sis, band-bib,
• int-abs/forward-lels is used by ushort-short, ushort-pos-02, ushort-max-06, ushort-inj, ushort-band-shift, ushort-band-01, ubyte-inj, sis-pos-upper, sis-pos-low, sis-pos-high, sis-on-bits, sis-neg-low, sis-ls-same-01, sis-ls-same, sis-03, short-nle-02, short-neq-01, short-max-06, short-larger, short-inrange, short-in, short-011x-neg, shiftright-byte-8-pos-01, longin-mult-01, long-automatic, inshort-le-num, getsetShort-theorem, getShort-isi, fits-law-shr-01, fits-law-shr, fits-law-mod, fits-law-div-stronger, fits-law-div, byte-unsigned, byte-succ, byte-nls-02, byte-nle-02, byte-ngr, byte-mult-256, byte-law-neg, byte-law-mult-one, byte-law-and-one, byte-law-add-one, bint-unsigned-01, bint-unsigned, bint-num-02, bint-mult2, bint-mod, bint-div2, bint-band-011x-neg, bib-pos-low, bib-pos-high, bib-on-bits, bib-neg-high, bib-ls-same-01, bib-ls-same,
• int-abs/forward-lsle is used by ushort-zero-02, ushort-pos-02, ushort-pos-01, ushort-plus-01, ushort-plus, ushort-inj, ushort-band-shift, ushort-band-01, ushort-band, ubyte-zero-01, ubyte-pos-03, ubyte-inj, sis-neg-lower, sis-neg-low, sis-ls-same-01, sis-ls-same, short-neq-01, short-mod-ngr, short-mod-add-01, short-mod-add, short-min-02, short-max-11, short-div-ngr, short-add-min-02, shiftright-byte-8-neg-01, mod-inshort, longin-mult-01, long-shiftzero-in, long-min-01, long-is-cast, long-band-add, long-automatic, lil-carry, getsetShort-theorem, getShort-isi, fits-law-shr-01, fits-law-shr, fits-law-div-stronger, fits-law-div, fits-law-band-02, fits-law-band-01, div-inshort, cast-b2i-01, byte-succ, byte-nls-02, byte-nls-01, byte-mult-neg, byte-mult-256, byte-law-neg, byte-law-add-one, byte-011x-unsgn, bint-trans-pos-03, bint-trans-pos-02, bint-num-02, bint-mod, bint-is-cast, bint-div2, bib-neg-high, bib-ls-same-01, bib-ls-same, bib-lower,
• int-abs/ge-def is used by shiftright-byte-8-pos-01, fits-law-sub, cast-b2i-01, byte-ngr, byte-nge,
• int-abs/le-add-03 is used by short-sub-pos,
• int-abs/lels is used by ushort-zero-02, ushort-zero, ushort-short, ushort-pos-02, ushort-pos-01, ushort-plus-01, ushort-plus, ushort-nlsz, ushort-neg, ushort-max-02, ushort-max-01, ushort-max, ushort-inj, ushort-band-shift-01, ushort-band-shift, ushort-band-01, ushort-band, ubyte-pos-03, ubyte-pos-02, ubyte-mult, ubyte-mod, ubyte-max-02, ubyte-max-01, ubyte-inj, ubyte-div-lsz, ubyte-band, sis-sub-2pot, sis-pos-low, sis-pos-high, sis-on-bits, sis-neg-lower, sis-neg-low, sis-neg-high, sis-ls-same-01, sis-ls-same, short-size-02, short-size, short-shift-pos, short-nls, short-nle, short-neq-02, short-neq-01, short-mod-ngr, short-mod-max, short-mod-add, short-mod, short-max-11, short-larger, short-div256, short-div-ngr, short-add-min-03, short-add-min, short-add-max-01, short-add-max, short-32767, short-011x-neg, shiftright-byte-8-pos-01, shiftright-byte-8-pos, shiftright-byte-8-neg-01, shiftright-byte-8-neg, num-i2l-neg, mod-inshort, longin-mult-01, long-shiftzero-in, long-mod-neg-low, long-mod-neg-high, long-is-cast, long-automatic, issi-ubyte, getsetShort-theorem, getShort-isi, fits-law-sub, fits-law-shr-01, fits-law-shr, fits-law-neg, fits-law-mul, fits-law-mod-01, fits-law-mod, fits-law-div-stronger, fits-law-band-02, fits-law-band-01, fits-law-add, div-inshort, cast-b2i-01, byte-nls-02, byte-ngr, byte-nge, byte-mult-pos, byte-mult-neg, byte-mult-256, byte-mult, byte-mod-100x-01, byte-mod-100x, byte-length, byte-law-neg, byte-law-mult-one, byte-law-and-one, byte-law-add-pos, byte-law-add-one, byte-127, bint-short, bint-mult2, bint-is-cast, bint-fillsgn-len, bint-div2, bint-byte, bint-band-zero, bint-band-one, bint-band-011x-neg, bint-and-011x-bits2unit, bib-pos-low, bib-pos-high, bib-on-bits, bib-neg-low, bib-neg-high, bib-ls-same-01, bib-ls-same, bib-lower, band-ff, Byte-and-range,
• int-abs/lels-01 is used by ushort-zero-02, ushort-zero-01, ushort-short, ushort-pos-02, ushort-pos-01, ushort-plus-01, ushort-plus, ushort-neg, ushort-max-03, ushort-max-02, ushort-max-01, ushort-band-shift-01, ushort-band-shift, ushort-band-03, ushort-band-02, ushort-band-01, ushort-band, ushort-abs, ubyte-zero-01, ubyte-zero, ubyte-pos-03, ubyte-pos-01, ubyte-mult, ubyte-mod, ubyte-max, ubyte-div-lsz, ubyte-band, ubyte-abs, sis-sub-2pot, sis-pos-upper, sis-pos-low, sis-pos-high, sis-on-bits, sis-neg-low, sis-neg-high, sis-ls-same-01, sis-ls-same, sis-03, short-succ, short-sub-pos, short-size-02, short-size, short-shift-pos, short-range, short-overflow, short-nls-01, short-nle-03, short-neq-02, short-neq-01, short-neq, short-mod-ngr, short-mod-add-02, short-mod-add-01, short-mod-01, short-min-03, short-min, short-max-11, short-max-05, short-max-02, short-larger, short-inrange, short-in, short-ge, short-div256, short-div-ngr, short-div-max, short-byte, short-add2, short-add-pos-02, short-add-pos-01, short-add-pos, short-add-min-01, short-add-min, shiftright-byte-8-pos-01, shiftright-byte-8-pos, shiftright-byte-8-neg-01, mod-inshort, longin-mult-01, longin-mod, long-shiftzero-in, long-mod-pos-low, long-mod-pos-high, long-is-cast, long-band-add, long-band-11x, long-automatic, lil-num, lil-carry, issi-ubyte, inshort-sis, inshort-num, inshort-neg, inshort-le-num, inshort-01, inbyte-bib, getsetShort-theorem, getShort-isi, fits-law-sub, fits-law-shr-01, fits-law-shr, fits-law-neg, fits-law-mul, fits-law-mod-01, fits-law-mod, fits-law-div-stronger, fits-law-div, fits-law-band-02, fits-law-band-01, fits-law-add, div-inshort, cast-b2i-01, byte-unsigned, byte-succ, byte-range, byte-nge, byte-mult-neg, byte-mult-256, byte-mult, byte-min, byte-length, byte-le, byte-law-neg, byte-law-mult-one, byte-law-add-pos, byte-law-add-one, byte-011x-unsgn, byte-011x-pos-01, byte-011x-ib, bint-unsigned-01, bint-trans-pos-03, bint-trans-pos-02, bint-trans-pos, bint-succ-notin, bint-short, bint-num-04, bint-mult2, bint-mod, bint-is-cast, bint-div2, bint-carry-01, bint-carry, bint-byte, bint-band-zero, bint-band-one, bint-band-and-nlsz, bint-band-011x, bint-and-011x-bits2unit, bib-upper, bib-pos-low, bib-pos-high, bib-on-bits, bib-neg-low, bib-neg-high, bib-ls-same-01, bib-ls-same, band-011x-01, Byte-and-range,
• int-abs/lels-02 is used by ushort-zero-02, ushort-zero, ushort-short, ushort-pos-02, ushort-max-01, ushort-band-shift, ushort-band-01, ubyte-zero, ubyte-max-01, sis-on-bits, sis-neg-low, sis-neg-high, short-size-02, short-size, short-neq-02, short-neq-01, short-mod-ngr, short-min-03, short-max-11, short-ge, short-div-ngr, shiftright-byte-8-neg-01, shiftright-byte-8-neg, longin-mult-01, lil-carry, inshort-mult, getsetShort-theorem, fits-law-shr-01, fits-law-shr, fits-law-neg, fits-law-mul, div-inshort, cast-b2i-01, byte-mult-256, byte-mult, byte-min, byte-length, byte-law-neg, byte-law-mult-one, bint-succ-notin, bint-fillsgn-len, bint-band-zero, bib-pos-low, bib-pos-high, bib-on-bits, bib-neg-high,
• int-abs/lels-03 is used by ushort-short, ushort-pos-02, ushort-pos-01, ushort-plus-01, ushort-plus, ushort-max, ushort-band-shift, ushort-band-01, ubyte-pos-03, ubyte-pos-01, ubyte-max, ubyte-div-lsz, sis-sub-2pot, sis-neg-lower, sis-neg-high, sis-ls-same-01, sis-ls-same, short-range, short-not-max, short-nls, short-ngr, short-neq-02, short-min-01, short-min, short-max-11, short-larger, short-add-min-03, short-add-max-01, short-011x-neg, shiftright-byte-8-neg-01, shiftright-byte-8-neg, num-i2s-pos, num-i2s-neg, num-i2l-neg, num-i2bi-pos, num-i2bi-neg, num-i2b-pos, num-i2b-neg, mod-inshort, long-shiftzero-in, long-mod-neg-low, long-mod-neg-high, long-min-01, long-is-cast, long-automatic, getsetShort-theorem, getShort-isi, fits-law-shr, fits-law-mul, fits-law-div-stronger, fits-law-add, div-inshort, cast-b2i-01, byte-not-max, byte-nls-02, byte-nls, byte-mult-neg, byte-mult-256, byte-law-neg, byte-law-mult-one, byte-law-and-one, byte-law-add-one, byte-gr-127, byte-011x-unsgn, bint-num-01, bint-mult2, bint-is-cast, bint-band-011x-neg, bint-and-011x-bits2unit, bib-pos-low, bib-neg-low, bib-ls-same-01, bib-ls-same, bib-lower,
• int-abs/lels-04 is used by ushort-pos-01, ushort-plus-01, ushort-nlsz, ushort-max-02, ushort-band-shift, ushort-band-01, ubyte-pos-03, sis-pos-low, sis-neg-lower, sis-neg-high, sis-ls-same, sis-03, short-nle-03, short-mod-ngr, short-max-04, short-max-03, short-in, short-div-ngr, short-add2, short-add-pos-01, short-add-min-02, short-add-max, shiftright-byte-8-pos-01, shiftright-byte-8-pos, shiftright-byte-8-neg-01, longin-mult-01, long-mod-pos-low, long-mod-pos-high, long-is-cast, long-automatic, getsetShort-theorem, getShort-isi, fits-law-shr-01, fits-law-div-stronger, fits-law-add, div-inshort, cast-b2i-01, byte-range, byte-nge, byte-mult-256, byte-mult, byte-law-neg, byte-law-and-one, byte-law-add-pos, byte-law-add-one, byte-011x-unsgn, bint-num-02, bint-mod, bint-band-011x, bib-pos-low, bib-on-bits, bib-ls-same-01, bib-ls-same, bib-lower,
• int-abs/lenls is used by sis-pos-high,
• int-abs/leone is used by ushort-band-shift, short-size-01, getsetShort-theorem, byte-size-01, byte-size, byte-mult-256,
• int-abs/lep is used by ushort-band-shift,
• int-abs/lep-01 is used by bib-ls-same-01,
• int-abs/lsone is used by ushort-band-shift, ushort-band-01, sis-neg-high, short-not-max, short-nls, short-max-11, inshort-mult, byte-not-max, bib-neg-high,
• int-abs/minus-02 is used by ushort-band-shift, bib-neg-high,
• int-abs/minus-add is used by ushort-band-shift, ushort-band-01, sis-neg-high, short-sub-pos, short-neq-01, short-max-11, short-add-min-03, short-add-min, longin-mult-01, inshort-neg, inshort-mult, getsetShort-theorem, fits-law-sub, fits-law-shr, fits-law-neg, fits-law-mod-01, fits-law-mod, fits-law-div-stronger, fits-law-div, fits-law-band-02, fits-law-band-01, fits-law-add, div-inshort, byte-mult-256, byte-law-neg, bint-succ-notin, bint-mod, bib-neg-high,
• int-abs/minus-ass is used by ushort-band-shift,
• int-abs/minus-neg is used by div-inshort,
• int-abs/minus-sub is used by div-inshort, byte-law-sub-one-01, byte-law-neg,
• int-abs/mone-05 is used by ushort-band-shift, fits-law-shr, bib-neg-high,
• int-abs/mone-06 is used by ushort-pos-02, ushort-band-shift, ubyte-max, sis-on-bits, short-size-02, short-size, short-neq-01, short-max-11, div-inshort, cast-b2i-01, byte-mult-256, bint-pred-01, bint-pred, bint-fillsgn-len,
• int-abs/mone-08 is used by ushort-neg, ushort-max-01, ushort-band-shift, ushort-band, sis-neg-low, num-i2l-neg, long-shiftzero-in, fits-law-shr, div-inshort, byte-mult-256, bib-on-bits, bib-neg-high,
• int-abs/neg is used by short-mod-ngr, short-div-ngr, longin-mult-01, fits-law-neg, div-inshort,
• int-abs/neg-02 is used by short-div-ngr, longin-mult-01, getShort-isi, fits-law-shr,
• int-abs/neg-03 is used by fits-law-neg, fits-law-div, byte-law-neg,
• int-abs/neg-05 is used by short-div-ngr, fits-law-shr, byte-law-neg,
• int-abs/neg-06 is used by ushort-band-shift, ushort-band-01, longin-mult-01, fits-law-shr, fits-law-mod-01, fits-law-mod, div-inshort, byte-nle-01, byte-nle, byte-ngr-01, bint-mod, bib-neg-high,
• int-abs/neg-07 is used by sis-neg-low, longin-mult-01, fits-law-mod-01, fits-law-mod, fits-law-div-stronger, div-inshort, byte-ngr-01, byte-law-neg, bint-mod, bib-neg-low,
• int-abs/neg-10 is used by short-div-ngr, fits-law-div-stronger,
• int-abs/neg-11 is used by byte-mult-256-01,
• int-abs/neg-12 is used by byte-mult-256-01, byte-law-neg, byte-law-compl, byte-add-256-01,
• int-abs/neg-13 is used by ushort-pos-02, ushort-band-shift, ushort-band-01, sis-neg-lower, sis-neg-low, sis-neg-high, sis-ls-same-01, sis-ls-same, short-neq-01, short-div-ngr, short-011x-neg, shiftright-byte-8-neg-01, shiftright-byte-8-neg, longin-mult-01, fits-law-neg, fits-law-div-stronger, byte-mult-256, byte-law-neg, byte-law-mult-one, byte-law-add-one, bint-band-011x-neg, bint-and-011x-bits2unit, bib-neg-low, bib-neg-high, bib-ls-same-01, bib-ls-same, bib-lower,
• int-abs/neg-15 is used by ushort-band-shift, fits-law-shr, fits-law-neg, fits-law-div-stronger, byte-law-sub-one-01, byte-law-sub-one, byte-law-neg, byte-law-mult-one, byte-law-compl, bib-neg-high,
• int-abs/negeq is used by short-neq-01, fits-law-shr, fits-law-neg, fits-law-div-stronger, fits-law-div, byte-law-neg, byte-law-compl, bib-neg-high, band-011x,
• int-abs/negle-07 is used by sis-neg-high, short-neq-01, short-mod-max, short-mod-add, short-mod, short-div-ngr, inshort-neg, fits-law-shr-01, fits-law-shr, fits-law-mod-01, fits-law-mod, fits-law-div-stronger, fits-law-div, fits-law-band-02, fits-law-band-01, div-inshort, byte-nle-01, byte-nle, byte-law-neg, bint-mod, bib-neg-high,
• int-abs/negle-13 is used by short-mod-ngr, inshort-neg, fits-law-shr-01, fits-law-div-stronger, fits-law-div, div-inshort, cast-b2i-01, byte-law-neg,
• int-abs/num-between is used by fits-law-div-stronger, byte-law-neg,
• int-abs/numadd is used by ushort-band-01, short-011x-neg, bint-band-011x-neg,
• int-abs/numadd-01 is used by ushort-zero-01, ushort-short, ushort-pos-02, ushort-max-05, ushort-max-01, ushort-band-shift, ushort-band-01, ubyte-zero-01, sis-neg-high, short-neq-02, short-ls, mtwo, mthree-01, mthree, minus-two, minus-three-01, minus-three, minus-four-02, minus-four-01, minus-four, minus-five-01, minus-five, mfive, getsetShort-theorem, fits-law-neg, fits-law-div-stronger, cast-b2i-01, byte-not-max, byte-nle-01, byte-mult-256, byte-ls-127, byte-law-neg, bint-fillsgn-len, bint-band-zero, bib-pos-high, bib-neg-high,
• int-abs/numle-02 is used by ushort-short, ushort-pos-02, ushort-neg, ushort-max-01, ushort-max, ushort-inj, ushort-band-shift, ushort-band-01, ushort-band, ubyte-inj, sis-sub-2pot, sis-on-bits, sis-neg-low, sis-neg-high, short-succ, short-size-02, short-size, short-mod-ngr, short-larger, short-add2, num-i2l-neg, long-shiftzero-in, long-is-cast, inshort-neg, inshort-01, getsetShort-theorem, fits-law-div, fits-law-add, div-inshort, cast-b2i-01, byte-succ, byte-nle-01, byte-mult-256, byte-law-neg, bint-succ-notin, bint-pred-02, bint-pred-01, bint-pred, bint-is-cast, bint-fillsgn-len, bib-on-bits, bib-neg-low, bib-neg-high, bib-ls-same-01,
• int-abs/numle-03 is used by ushort-short, ushort-inj, ushort-band-shift, ubyte-inj, sis-sub-2pot, sis-neg-low, sis-neg-high, short-succ, short-nle-03, short-neq-02, short-mod-max, short-mod-add, short-mod, longin-mult-01, inshort-01, getsetShort-theorem, fits-law-shr, fits-law-mul, fits-law-div-stronger, div-inshort, byte-succ, byte-nle-01, byte-nle, byte-mult-256, bint-succ-notin, bint-pred-02, bint-pred-01, bint-pred, bint-div2, bib-neg-low, bib-neg-high,
• int-abs/numleledel is used by ushort-band-shift, sis-pos-low, sis-on-bits, sis-05, short-neq-02, short-add-pos-02, short-add-pos-01, short-add-pos, num-issi, num-illi, num-ibbi, notequal-01, notequal, longin-mult-mod-01, longin-mult-01, longin-mult, long-mod-pos-low, long-automatic, lil-carry, inshort-sis, fits-law-shr-01, byte-range, byte-mult-pos, byte-law-neg, byte-in, bor-sis, bint-pred-01, bint-fillsgn-len, bint-band-zero, bint-and-011x-bits2unit, bib-pos-low, bib-on-bits, bib-in-01, bcompl-sis, band-sis,
• int-abs/numleledel-01 is used by ushort-short, ushort-pos-02, ushort-pos-01, ushort-plus-01, ushort-plus, ushort-inj, ushort-band-shift, ushort-band-01, ushort-band, ubyte-inj, sis-sub-2pot, sis-pos-low, sis-pos-high, sis-on-bits, sis-neg-high, sis-ls-same-01, sis-ls-same, sis-05, sis-03, short-mod, short-max-01, short-larger, short-inrange, num-illi, notequal-01, notequal, longin-mult-01, long-shiftzero-in, long-mod-neg-high, long-is-cast, long-automatic, lil-num, l2i-bint, inshort-sis, inshort-num, inshort-01, getsetShort-theorem, fits-law-shr-01, div-inshort, byte-unsigned, byte-succ, byte-range, byte-nls-02, byte-mult-256, byte-law-neg, byte-law-mult-one, byte-law-add-one, byte-in, byte-011x-unsgn, bor-sis, bint-unsigned, bint-trans-pos-02, bint-trans-pos-01, bint-succ-notin, bint-pred-02, bint-pred-01, bint-pred, bint-num-in, bint-num-03, bint-num, bint-is-cast, bint-fillsgn-len, bint-band-zero, bint-band-011x, bint-and-011x-bits2unit, bib-pos-low, bib-pos-high, bib-on-bits, bib-neg-low, bib-neg-high, bib-ls-same-01, bib-ls-same, bib-in-01, bcompl-sis, band-sis,
• int-abs/numlelsdel is used by ushort-plus, ushort-max-05, ushort-max-02, ushort-band-01, ubyte-pos-03, sis-pos-high, sis-neg-low, short-nls, short-max-11, short-add-min-02, longin-mult-01, long-mod-neg-low, long-automatic, getsetShort-theorem, fits-law-shr, div-inshort, byte-unsigned, byte-mult-neg, byte-mult-256, byte-law-mult-one, byte-law-and-one, byte-law-add-one, bint-unsigned, bint-num-in, bib-pos-high, bib-neg-low,
• int-abs/numlelsdel-01 is used by ushort-pos-01, ushort-max-03, ushort-band-shift, sis-pos-high, sis-neg-lower, sis-neg-low, short-overflow, short-add-max-01, long-mod-pos-high, long-automatic, div-inshort, byte-size-01, byte-mult-256, byte-law-mult-one, byte-law-add-one, bint-unsigned-01, bib-upper, bib-pos-high, bib-neg-low, bib-lower,
• int-abs/numls-02 is used by ushort-zero-02, ushort-pos-02, ushort-band-shift, ushort-band-01, ushort-band, ubyte-max-02, ubyte-max, sis-neg-lower, sis-neg-low, sis-neg-high, sis-ls-same-01, sis-ls-same, short-neq-01, short-max-11, short-larger, short-div-ngr, short-011x-neg, shiftright-byte-8-neg-01, shiftright-byte-8-neg, lil-carry, getsetShort-theorem, getShort-isi, fits-law-neg, div-inshort, cast-b2i-01, byte-mult-256, byte-law-neg, byte-law-mult-one, byte-law-add-one, bint-pred-01, bint-pred, bint-band-011x-neg, bint-and-011x-bits2unit, bib-neg-low, bib-neg-high, bib-ls-same-01, bib-ls-same, bib-lower,
• int-abs/numls-03 is used by ushort-short, ushort-plus, ushort-nlsz, ushort-max-05, ushort-max-02, ushort-band-shift, ushort-band-01, ushort-band, ubyte-pos-01, sis-sub-2pot, sis-neg-low, sis-ls-same-01, short-not-max, short-nls-01, short-max-11, short-ls, longin-mult-01, lil-carry, getsetShort-theorem, getShort-isi, fits-law-sub, fits-law-shr, fits-law-mod-01, fits-law-mod, fits-law-div-stronger, div-inshort, byte-not-max, byte-nls-02, byte-nle-01, byte-ngr-01, byte-mult-256, byte-ls-127, byte-law-neg, byte-011x-pos-01, bint-mod, bib-neg-low, bib-ls-same-01,
• int-abs/numlsf-01 is used by getShort-isi, bib-pos-high,
• int-abs/numlsledel is used by ushort-short, ushort-band-shift, ushort-band-01, sis-sub-2pot, sis-pos-low, sis-on-bits, sis-ls-same-01, short-in, short-add2, l2i-bint, inshort-num, getsetShort-theorem, bint-pred-02, bint-pred, bint-is-cast, bint-fillsgn-len, bint-band-011x, bib-pos-low, bib-pos-high, bib-on-bits, bib-neg-high, bib-ls-same-01,
• int-abs/numlsledel-01 is used by ushort-pos-02, ushort-band-shift, ushort-band-01, ushort-band, sis-sub-2pot, sis-pos-upper, sis-neg-high, sis-ls-same, short-larger, getsetShort-theorem, byte-unsigned, byte-mult-256, byte-law-mult-one, byte-law-add-one, bint-unsigned-01, bint-band-011x-neg, bint-and-011x-bits2unit, bib-neg-low, bib-neg-high, bib-ls-same, bib-lower,
• int-abs/numsub is used by ushort-band-shift, ushort-band-01, sis-sub-2pot, short-011x-neg, getShort-isi, byte-mult-256, bint-succ-notin, b2i-i2b-same,
• int-abs/sub-add-01 is used by ushort-band-shift, ushort-band-01, getsetShort-theorem, fits-law-shr, byte-mult-256, byte-law-add-pos, byte-law-add-one,
• int-abs/sub-add-09 is used by byte-law-compl,
• int-abs/sub-eq is used by ushort-short, ushort-band-shift, ushort-band-01, ubyte-pos-03, sis-pos-upper, sis-pos-high, sis-neg-high, short-sub-pos, short-size-01, short-larger, short-in, shiftright-byte-8-neg, long-mod-pos-high, long-automatic, getsetShort-theorem, fits-law-sub, fits-law-shr, div-inshort, byte-unsigned, byte-not-max, byte-mult-pos, byte-mult-256, byte-law-sub-one-01, byte-law-sub-one, byte-law-neg, byte-law-compl, byte-011x-unsgn, bint-unsigned-01, bint-unsigned, bint-succ-notin, bint-pred-02, bint-pred, bib-upper, bib-pos-high, bib-neg-high, b2i-i2b-same,
• int-abs/sub-eq-01 is used by ushort-band-01, byte-law-neg,
• int-abs/sub-le is used by ushort-band-shift, sis-pos-high, short-sub-pos, short-neq-01, short-add-min, inshort-neg, inshort-mult, getsetShort-theorem, fits-law-sub, fits-law-shr, fits-law-mod-01, fits-law-mod, fits-law-div-stronger, fits-law-div, fits-law-band-02, fits-law-band-01, div-inshort, byte-unsigned, byte-law-neg, bint-mod, bib-pos-high, bib-neg-high,
• int-abs/sub-le-01 is used by ushort-pos-01, ushort-band-shift, ushort-band-01, ubyte-pos-03, sis-pos-high, short-sub-pos, short-size-01, short-overflow, short-larger, getsetShort-theorem, fits-law-sub, fits-law-shr, fits-law-neg, fits-law-div-stronger, div-inshort, byte-unsigned, byte-size-01, byte-size, byte-mult-256, byte-law-neg, byte-011x-unsgn, bib-pos-high,
• int-abs/sub-ls is used by ushort-band-shift, ushort-band-01, sis-neg-high, short-max-11, short-add-min-03, short-add-min, getsetShort-theorem, fits-law-sub, fits-law-div-stronger, fits-law-add, div-inshort, byte-nge, byte-mult-256, bib-neg-high, bib-ls-same-01,
• int-abs/sub-ls-01 is used by ushort-band-shift, sis-ls-same, short-size-01, longin-mult-01, fits-law-neg, fits-law-div-stronger, byte-size-01, byte-size, byte-not-max, byte-law-neg, bib-neg-high, bib-ls-same,
• int-abs/sub-pred is used by byte-nge, b2i-i2b-same,
• int-abs/sub-sub is used by sis-neg-high,
• int-abs/sub-sub-04 is used by fits-law-shr,
• int-abs/subsub is used by short-law-compl, short-011x-neg, getShort-isi, fits-law-shr, byte-law-neg, byte-law-compl, bint-band-011x-neg, bint-and-011x-bits2unit,
• int-abs/succ-01 is used by fits-law-shr,
• int-abs/succ-02 is used by cast-b2i-01, byte-nge,
• int-abs/zero-ge-01 is used by short-mod-add-01,
• int-abs/zero-gels is used by sis-ls-same, getsetShort-theorem, byte-law-neg, bib-ls-same,
• int-abs/zero-gels-01 is used by ushort-pos-02, ushort-pos-01, ushort-plus-01, ushort-plus, ushort-inj, ushort-band-shift, ushort-band-01, ushort-band, ubyte-pos-03, ubyte-inj, sis-neg-lower, sis-neg-low, sis-neg-high, sis-ls-same-01, sis-ls-same, short-neq-01, short-mod-ngr, short-mod-add-01, short-max-11, short-div-ngr, short-add-min-02, shiftright-byte-8-neg-01, mod-inshort, long-mod-neg-low, long-automatic, getsetShort-theorem, fits-law-shr-01, fits-law-shr, fits-law-mul, fits-law-div-stronger, fits-law-band-02, fits-law-band-01, div-inshort, cast-b2i-01, byte-nls-02, byte-mult-neg, byte-mult-256, byte-law-neg, byte-law-add-one, byte-011x-unsgn, bib-neg-low, bib-neg-high, bib-ls-same-01, bib-ls-same, bib-lower,
• int-abs/zero-gels-02 is used by bint-div2,
• int-abs/zero-gels-03 is used by ushort-pos-02, ushort-pos-01, ushort-plus-01, ushort-plus, ushort-band-shift, ushort-band-01, sis-sub-2pot, sis-on-bits, sis-neg-low, sis-neg-high, sis-ls-same-01, sis-ls-same, short-nle-01, short-nle, short-mod, short-min-02, short-add-min, short-011x-neg, longin-mult-01, long-min-01, long-is-cast, long-automatic, getsetShort-theorem, fits-law-neg, fits-law-mul, byte-nls-01, byte-mult-256, byte-law-neg, byte-law-add-one, byte-011x-unsgn, bint-mod, bint-is-cast, bint-band-zero, bint-band-011x-neg, bint-and-011x-bits2unit, bib-on-bits, bib-neg-low, bib-neg-high, bib-ls-same-01, bib-ls-same,
• int-abs/zero-gels-04 is used by ushort-short, ushort-max-02, ushort-band-shift, ushort-band-01, sis-pos-low, sis-pos-high, short-neq-01, long-automatic, getsetShort-theorem, fits-law-shr, fits-law-div-stronger, byte-mult-neg, byte-mult-256, byte-law-mult-one, byte-law-and-one, byte-law-add-pos, byte-law-add-one, bib-on-bits,
• int-abs/zero-gs is used by ushort-plus,

Used from specification list-last

• list-last/bitlista/l is used by bib-neg-high,
• list-last/bitlista/l-05 is used by short-law-righthift-not, long-automatic-03, byte-law-righthift-not,
• list-last/bitlista/last-def is used by sis-pos-low, short-law-righthift-not, long-automatic-03, long-automatic-02, long-automatic-01, byte-mult-256, byte-law-righthift-not, bib-neg-high,
• list-last/bitlista/mk-empty is used by getShort-isi, byte-law-and-one,
• list-last/bitlista/mk-len is used by sis-neg-high, getShort-isi, byte-law-righthift-not, byte-law-and-one, bib-on-bits, bib-neg-low,
• list-last/bitlista/mk-plus is used by byte-law-righthift-not,
• list-last/bitlista/mk-zero is used by ushort-neg, sis-pos-low, sis-on-bits, short-law-righthift-not, byte-size, byte-law-righthift-not, byte-law-and-one, bint-fillsgn-len, bib-on-bits, bib-neg-high,

Used from specification list-data

• list-data/bitlista/length-rest is used by sis-pos-low, sis-pos-high, sis-neg-low, bib-pos-high, bib-neg-low,
• list-data/bitlista/elim-list is used by bib-neg-low,
• list-data/bitlista/elim-list-c is used by bib-pos-low,
• list-data/bitlista/l is used by ushort-neg, sis-pos-low, sis-on-bits, sis-neg-low, sis-neg-high, short-size-02, short-size-01, short-size, long-shiftzero-in, long-is-cast, getShort-isi, fits-law-neg, fits-law-compl-01, fits-law-compl, fits-law-band, byte-size-01, byte-size, byte-length, byte-len, byte-law-righthift-not, byte-law-and-one, bint-is-cast, bint-fillsgn-len, bib-pos-low, bib-pos-high, bib-on-bits, bib-neg-low, bib-neg-high,
• list-data/bitlista/size-01 is used by sis-pos-low, byte-law-and-one,

Used from specification int2bits

• int2bits/bits2bits-def is used by byte-law-and-one,
• int2bits/bits2int-fill is used by ushort-neg, ubyte-neg, sis-on-bits, sis-neg-high, bint-and-011x-bits2unit, bib-neg-low, bib-neg-high,
• int2bits/bits2int-inj is used by byte-law-and-one,
• int2bits/bits2int-mklist is used by bib-on-bits,
• int2bits/bits2int-neg is used by long-automatic-02,
• int2bits/bits2int-neg-03 is used by short-law-righthift-not, byte-law-righthift-not,
• int2bits/bits2int-split is used by getShort-isi,
• int2bits/bits2int-split-01 is used by getShort-isi,
• int2bits/bits2int-zeros-03 is used by sis-neg-high,
• int2bits/bits2int16 is used by sis-on-bits,
• int2bits/bits2int16-01 is used by sis-on-bits,
• int2bits/bits2int8 is used by bib-on-bits,
• int2bits/bits2int8-01 is used by bib-on-bits,
• int2bits/bits2uint-mklist is used by byte-law-righthift-not,
• int2bits/bits2uint-ones is used by getShort-isi,
• int2bits/bits2uint-split is used by byte-law-righthift-not,
• int2bits/int2bits-2pot is used by byte-size,
• int2bits/int2bits-2pot-04 is used by sis-neg-high, bib-neg-high,
• int2bits/int2bits-add-high is used by sis-neg-low, bib-neg-low,
• int2bits/int2bits-add-low is used by sis-neg-high, bib-neg-high,
• int2bits/int2bits-lelen is used by num-i2l-pos, long-is-cast, bint-is-cast,
• int2bits/int2bits-lelen-03 is used by num-i2l-neg, long-is-cast, bint-is-cast,
• int2bits/int2bits-lelen-05 is used by bib-neg-high,
• int2bits/int2bits-lelen-06 is used by sis-pos-low, bib-pos-low,
• int2bits/int2bits-len-neg is used by sis-neg-low, bib-neg-low,
• int2bits/int2bits-len-pos is used by sis-pos-high, bib-pos-high,
• int2bits/int2bits-len-range is used by byte-length,
• int2bits/int2bits-lslen is used by sis-on-bits, bib-pos-low, bib-pos-high, bib-on-bits,
• int2bits/int2bits-lslen-01 is used by byte-size,
• int2bits/int2bits-lslen-03 is used by sis-on-bits, bib-on-bits,
• int2bits/int2bits-lslen-05 is used by ushort-neg, sis-on-bits, sis-neg-high, short-size-02, short-size, long-shiftzero-in, fits-law-neg, bint-fillsgn-len, bib-on-bits, bib-neg-low, bib-neg-high,
• int2bits/int2bits-lslen-06 is used by sis-pos-low, sis-on-bits, short-size-02, short-size, fits-law-neg, byte-law-and-one, bint-fillsgn-len, bib-on-bits,
• int2bits/int2bits-mod256 is used by bib-pos-low, bib-pos-high,
• int2bits/int2bits-mod2pot is used by sis-pos-low, sis-pos-high,
• int2bits/int2bits-mone is used by sis-on-bits, short-size-02, short-size, long-shiftzero-in, fits-law-neg, bint-fillsgn-len, bib-on-bits,
• int2bits/int2bits-neg is used by long-automatic-01, bib-neg-high,
• int2bits/int2bits-neg-num is used by short-law-righthift-not, byte-law-righthift-not,
• int2bits/int2bits-pos is used by sis-pos-high, short-law-righthift-not, long-automatic-03, long-automatic-02, getShort-isi, byte-law-righthift-not, bib-pos-high,
• int2bits/int2bits-pos-num is used by short-law-righthift-not,
• int2bits/int2bits-rec-neg is used by sis-neg-high,
• int2bits/int2int-lastn-negneg is used by bib-neg-high,
• int2bits/int2int-lastn-posneg is used by bib-pos-high,
• int2bits/int2int-lastn-pospos is used by bib-pos-low,
• int2bits/int2int-rest is used by sis-pos-high, bib-pos-high,
• int2bits/int2int-rest-01 is used by sis-neg-low, bib-neg-low,
• int2bits/ubits2bits is used by ushort-neg, ubyte-neg, bint-and-011x-bits2unit,
• int2bits/uint2bits-rec-01 is used by bib-neg-high,
• int2bits/bits2bits-def is used by byte-is-cast-01,
• int2bits/bits2int-fill is used by sis-pos-low,
• int2bits/bits2int-inj is used by byte-law-and-one, byte-is-cast-01,
• int2bits/bits2int-neg is used by sis-neg-high, bib-neg-low,
• int2bits/bits2int-pos is used by ushort-pos, ushort-neg, ubyte-pos, ubyte-neg, sis-pos-low, sis-on-bits, short-law-righthift-not, out-test-06, out-test-05, out-test-02, long-automatic-03, long-automatic-01, getShort-isi, byte-mult-256, byte-law-righthift-not, bib-on-bits, bib-neg-high,
• int2bits/bits2uint-2pot-02 is used by sis-neg-high,
• int2bits/bits2uint-one is used by short-law-righthift-not, out-test-05, out-test-02, long-automatic-03, long-automatic-02, long-automatic-01, byte-law-righthift-not,
• int2bits/bits2uint-one-02 is used by sis-pos-low, sis-on-bits, short-law-righthift-not, out-test-06, out-test-05, long-automatic-03, long-automatic-02, byte-mult-256, byte-law-righthift-not, bib-on-bits, bib-neg-high,
• int2bits/bits2uint-one-03 is used by short-law-righthift-not, out-test-02, long-automatic-01, getShort-isi, byte-law-righthift-not, bib-neg-low,
• int2bits/bits2uint-zero is used by sis-pos-low, sis-on-bits, short-law-righthift-not, out-test-06, out-test-05, long-automatic-03, long-automatic-02, getShort-isi, byte-mult-256, byte-law-righthift-not, bib-on-bits, bib-neg-low, bib-neg-high,
• int2bits/bits2uint-zeros-03 is used by byte-law-righthift-not,
• int2bits/bits2uint-zeros-04 is used by getShort-isi,
• int2bits/int2bits-011x is used by bint-band-011x-neg, bint-and-011x-bits2unit,
• int2bits/int2bits-eq is used by bib-neg-low,
• int2bits/int2bits-fillfirst is used by ushort-neg, ubyte-neg, byte-law-and-one, bint-and-011x-bits2unit, bib-pos-low, bib-neg-high,
• int2bits/int2bits-first-01 is used by ushort-neg, ubyte-neg, getShort-isi, byte-law-righthift-not, byte-law-and-one, bint-and-011x-bits2unit, bib-on-bits, bib-neg-high,
• int2bits/int2bits-first-02 is used by sis-pos-low, getShort-isi, byte-law-righthift-not, byte-law-and-one, bib-pos-low, bib-on-bits,
• int2bits/int2bits-len-one is used by byte-law-righthift-not,
• int2bits/int2bits-leneq-neg is used by sis-neg-low, byte-law-and-one,
• int2bits/int2bits-leneq-pos is used by byte-law-righthift-not, byte-law-and-one,
• int2bits/int2bits-mone-02 is used by sis-neg-low, bib-neg-high,
• int2bits/int2bits-neg-num is used by ushort-neg, sis-neg-high, out-test-06, out-test-05, out-test-02, byte-mult-256, byte-len, bib-neg-low,
• int2bits/int2bits-not-empty is used by ushort-neg, ubyte-neg, sis-pos-low, sis-pos-high, sis-on-bits, sis-neg-low, sis-neg-high, short-size-02, short-size-01, short-size, long-shiftzero-in, long-is-cast, getShort-isi, fits-law-neg, fits-law-compl-01, fits-law-compl, fits-law-band, byte-size-01, byte-size, byte-length, byte-len, byte-law-righthift-not, byte-law-and-one, bint-is-cast, bint-fillsgn-len, bint-and-011x-bits2unit, bib-pos-low, bib-pos-high, bib-on-bits, bib-neg-low, bib-neg-high,
• int2bits/int2bits-pos-num is used by getShort-isi, bib-neg-low,
• int2bits/int2bits-true is used by bib-neg-low,
• int2bits/int2bits-zero is used by sis-pos-low, sis-on-bits, sis-neg-high, short-size-02, short-size, fits-law-neg, bint-fillsgn-len, bib-pos-low, bib-pos-high, bib-on-bits, bib-neg-high,
• int2bits/int2int-inj is used by ushort-neg, ubyte-neg, sis-pos-low, sis-on-bits, sis-neg-high, bint-and-011x-bits2unit, bib-on-bits, bib-neg-high,
• int2bits/int2uint-fill is used by ushort-pos, ubyte-pos, bint-and-011x-bits2unit,
• int2bits/int2uint-inv-01 is used by getShort-isi,
• int2bits/uint2bits-one is used by ushort-neg, sis-neg-high, short-law-righthift-not, out-test-06, out-test-05, out-test-02, long-automatic-03, long-automatic-02, long-automatic-01, getShort-isi, byte-mult-256, byte-len, byte-law-righthift-not, bib-neg-low, bib-neg-high,
• int2bits/uint2bits-onein-01 is used by bib-neg-high,
• int2bits/uint2bits-pos-num is used by sis-neg-high, short-law-righthift-not, out-test-06, out-test-05, out-test-02, long-automatic-03, long-automatic-02, long-automatic-01, getShort-isi, byte-mult-256, byte-len, byte-law-righthift-not, bib-neg-low,
• int2bits/uint2uint-pos is used by getShort-isi,

Used from specification list

• list/bitlista/a is used by byte-law-and-one,
• list/bitlista/split-rest is used by byte-law-and-one,
• list/bitlista/Last is used by ushort-neg, sis-neg-high, short-law-righthift-not, out-test-06, out-test-05, out-test-02, long-automatic-03, long-automatic-02, long-automatic-01, getShort-isi, byte-mult-256, byte-len, byte-law-righthift-not, bib-neg-low, bib-neg-high,
• list/bitlista/Nil is used by out-test-06, out-test-05, out-test-02, byte-law-and-one, bib-neg-low,
• list/bitlista/Two is used by ushort-neg, sis-neg-high, short-law-righthift-not, out-test-06, out-test-05, out-test-02, long-automatic-03, long-automatic-02, long-automatic-01, getShort-isi, byte-mult-256, byte-len, byte-law-righthift-not, bib-neg-low, bib-neg-high,
• list/bitlista/a is used by ushort-pos, ushort-neg, ubyte-pos, ubyte-neg, sis-pos-low, sis-on-bits, sis-neg-low, sis-neg-high, short-law-righthift-not, out-test-06, out-test-05, out-test-02, long-automatic-03, long-automatic-02, long-automatic-01, getShort-isi, byte-size, byte-mult-256, byte-len, byte-law-righthift-not, byte-law-and-one, bint-fillsgn-len, bib-pos-low, bib-on-bits, bib-neg-low, bib-neg-high,
• list/bitlista/app is used by ushort-neg, sis-pos-low, sis-on-bits, short-law-righthift-not, byte-size, byte-law-righthift-not, byte-law-and-one, bint-fillsgn-len, bib-pos-low, bib-on-bits, bib-neg-low, bib-neg-high,
• list/bitlista/app-01 is used by byte-law-and-one,
• list/bitlista/app-02-ant is used by short-law-righthift-not, byte-law-righthift-not, byte-law-and-one,
• list/bitlista/c is used by ushort-neg, sis-neg-high, short-law-righthift-not, out-test-06, out-test-05, out-test-02, long-automatic-02, long-automatic-01, byte-mult-256, byte-len, byte-law-righthift-not, bib-pos-low, bib-neg-low, bib-neg-high,
• list/bitlista/c-07 is used by sis-pos-low, bib-neg-low,
• list/bitlista/c-08 is used by short-law-righthift-not, byte-law-righthift-not, byte-law-and-one, bib-neg-high,
• list/bitlista/e is used by short-law-righthift-not, byte-law-righthift-not, byte-law-and-one,
• list/bitlista/e-01 is used by ushort-neg, short-law-righthift-not, byte-law-and-one, bib-neg-low,
• list/bitlista/in-14 is used by bib-pos-low,
• list/bitlista/in-17 is used by bib-pos-low,
• list/bitlista/in-append is used by bib-pos-low,
• list/bitlista/len is used by ushort-neg, sis-on-bits, sis-neg-high, short-law-righthift-not, byte-size, byte-len, byte-law-righthift-not, byte-law-and-one, bint-fillsgn-len, bib-on-bits, bib-neg-high,
• list/bitlista/len-02 is used by ushort-neg, sis-on-bits, sis-neg-low, sis-neg-high, short-size-02, short-size, short-law-righthift-not, long-shiftzero-in, fits-law-neg, byte-size, byte-len, byte-law-righthift-not, byte-law-and-one, bint-fillsgn-len, bib-pos-low, bib-on-bits, bib-neg-high,
• list/bitlista/rest is used by sis-pos-low, bib-pos-low,

Used from specification nat-basic2

• nat-basic2/a is used by sis-pos-high, sis-neg-low, short-size-01, byte-law-righthift-not, byte-law-and-one, bib-on-bits, bib-neg-high,
• nat-basic2/c is used by sis-pos-high, sis-neg-low, short-size-01, byte-law-righthift-not, byte-law-and-one, bib-on-bits, bib-neg-high,
• nat-basic2/eqs is used by byte-law-righthift-not,
• nat-basic2/l is used by byte-law-and-one,
• nat-basic2/l-01 is used by byte-law-righthift-not, byte-law-and-one,
• nat-basic2/l-02 is used by byte-law-righthift-not, byte-law-and-one,
• nat-basic2/l-06 is used by byte-law-and-one,
• nat-basic2/l-08 is used by byte-law-and-one,
• nat-basic2/one is used by byte-law-righthift-not,
• nat-basic2/oz is used by byte-law-righthift-not,
• nat-basic2/s is used by byte-law-righthift-not, byte-law-and-one,
• nat-basic2/succ is used by byte-law-and-one,

Used from specification intnat

• intnat/succ is used by byte-size,
• intnat/n2i-add is used by byte-law-righthift-not,
• intnat/n2n is used by byte-size,
• intnat/nat2int is used by short-size,
• intnat/nat2int-05 is used by short-size-01,
• intnat/num-n2i-ls-02 is used by short-size-01, short-size, byte-size-01, byte-size,
• intnat/num-n2i-ls-04 is used by sis-bitlength, fits-law-neg, fits-law-compl-01, fits-law-compl, fits-law-band, bib-bitlength,

Used from specification int-basic2

• int-basic2/add-c is used by ushort-max-02, short-mod-add-01, short-max-11, short-max-04, short-law-add, short-add-min-03, short-add-min-02, short-add-max-01, byte-law-add,
• int-basic2/ls-01 is used by getShort-isi,
• int-basic2/lst-01 is used by short-add-max-01,
• int-basic2/lst-02 is used by short-max-11,
• int-basic2/lst-03 is used by ushort-max-02, short-max-11, short-add-min-03, short-add-min-02,
• int-basic2/not-zero-pos is used by short-neq-02, short-neq-01,
• int-basic2/pls is used by short-add-max,
• int-basic2/pls-01 is used by lil-carry,
• int-basic2/pls-02 is used by short-max-04, short-max-03,
• int-basic2/zero is used by short-neq-01,
• int-basic2/add-a is used by ushort-zero-02, ushort-zero-01, ushort-short, ushort-pos-02, ushort-pos-01, ushort-plus-01, ushort-plus, ushort-nlsz, ushort-neg, ushort-max-05, ushort-max-02, ushort-max-01, ushort-max, ushort-inj, ushort-band-shift, ushort-band-03, ushort-band-01, ushort-band, ubyte-zero-01, ubyte-pos-03, ubyte-pos-01, ubyte-neg, ubyte-max-02, ubyte-max, ubyte-inj, sis-sub-2pot, sis-pos-upper, sis-pos-low, sis-pos-high, sis-on-bits, sis-neg-lower, sis-neg-low, sis-neg-high, sis-ls-same-01, sis-ls-same, sis-03, short-succ-pos, short-succ, short-sub-pos, short-size-02, short-size-01, short-size, short-overflow, short-not-max, short-nls-01, short-nle-03, short-neq-02, short-neq-01, short-mod-ngr, short-mod-max, short-mod-add-01, short-mod-add, short-mod, short-max-11, short-ls, short-larger, short-in, short-div-ngr, short-add2, short-add-pos-02, short-add-pos-01, short-add-pos, short-add-min-03, short-add-min-02, short-add-min-01, short-add-min, short-add-max-01, short-011x-neg, shiftright-byte-8-neg-01, shiftright-byte-8-neg, num-i2l-neg, mtwo, mthree-01, mthree, minus-two, minus-three-01, minus-three, minus-four-02, minus-four-01, minus-four, minus-five-01, minus-five, mfive, longin-mult-01, long-shiftzero-in, long-mod-pos-high, long-mod-neg-low, long-is-cast, long-band-add, long-automatic, lil-carry, inshort-neg, inshort-mult, inshort-01, getsetShort-theorem, getShort-isi, fits-law-sub, fits-law-shr-01, fits-law-shr, fits-law-neg, fits-law-mul, fits-law-mod-01, fits-law-mod, fits-law-div-stronger, fits-law-div, fits-law-band-02, fits-law-band-01, fits-law-add, ex256, div-inshort, cast-b2i-01, byte-succ, byte-size, byte-not-max, byte-nls-02, byte-nle-01, byte-nle, byte-ngr-01, byte-nge, byte-mult-pos, byte-mult-neg, byte-mult-256-01, byte-mult-256, byte-mod-100x-01, byte-ls-127, byte-law-sub-one-01, byte-law-sub-one, byte-law-neg, byte-law-mult-one, byte-law-compl, byte-law-add-pos, byte-law-add-one, byte-add-256, byte-011x-unsgn, byte-011x-pos-01, byte-011x-neg, byte-011x-ib, bint-unsigned-01, bint-unsigned, bint-succ-notin, bint-pred-02, bint-pred-01, bint-pred, bint-mod, bint-is-cast, bint-fillsgn-len, bint-div2, bint-carry-01, bint-carry, bint-band-zero, bint-band-011x-neg, bint-and-011x-bits2unit, bib-upper, bib-pos-low, bib-pos-high, bib-on-bits, bib-neg-low, bib-neg-high, bib-ls-same-01, bib-ls-same, bib-lower, band-ff, band-011x, b2i-i2b-same,
• int-basic2/add-c is used by ushort-zero-02, ushort-zero-01, ushort-short, ushort-pos-02, ushort-pos-01, ushort-plus-01, ushort-plus, ushort-nlsz, ushort-neg, ushort-max-05, ushort-max-02, ushort-max-01, ushort-max, ushort-inj, ushort-band-shift, ushort-band-03, ushort-band-01, ushort-band, ubyte-zero-01, ubyte-pos-03, ubyte-pos-01, ubyte-neg, ubyte-max-02, ubyte-max, ubyte-inj, ubyte-div-lsz, sis-sub-2pot, sis-pos-upper, sis-pos-low, sis-pos-high, sis-on-bits, sis-neg-lower, sis-neg-low, sis-neg-high, sis-ls-same-01, sis-ls-same, sis-03, short-succ-pos, short-succ, short-sub-pos, short-size-02, short-size-01, short-size, short-overflow, short-not-max, short-nls-01, short-nle-03, short-neq-02, short-neq-01, short-mod-ngr, short-mod-max, short-mod-add-01, short-mod-add, short-mod, short-max-11, short-ls, short-law-compl, short-law-add-one, short-law-add, short-larger, short-in, short-div-ngr, short-add2, short-add-pos-02, short-add-pos-01, short-add-pos, short-add-min-03, short-add-min-02, short-add-min-01, short-add-min, short-add-max-01, short-add-max, short-011x-neg, shiftright-byte-8-neg-01, shiftright-byte-8-neg, num-i2l-neg, mtwo, mthree-01, mthree, minus-two, minus-three-01, minus-three, minus-four-02, minus-four-01, minus-four, minus-five-01, minus-five, mfive, longin-mult-01, long-shiftzero-in, long-mod-pos-high, long-mod-neg-low, long-is-cast, long-band-add, long-automatic, lil-carry, inshort-neg, inshort-mult, inshort-01, getsetShort-theorem, getShort-isi, fits-law-sub, fits-law-shr-01, fits-law-shr, fits-law-neg, fits-law-mul, fits-law-mod-01, fits-law-mod, fits-law-div-stronger, fits-law-div, fits-law-band-02, fits-law-band-01, fits-law-add, ex256, div-inshort, cast-b2i-01, byte-succ, byte-size, byte-not-max, byte-nls-02, byte-nle-01, byte-nle, byte-ngr-01, byte-nge, byte-mult-pos, byte-mult-neg, byte-mult-256-01, byte-mult-256, byte-mod-100x-01, byte-ls-127, byte-law-sub-one-01, byte-law-sub-one, byte-law-neg, byte-law-mult-one, byte-law-compl, byte-law-add-pos, byte-law-add-one, byte-law-add, byte-add-256-01, byte-add-256, byte-011x-unsgn, byte-011x-pos-01, byte-011x-neg, byte-011x-ib, bint-unsigned-01, bint-unsigned, bint-succ-notin, bint-pred-02, bint-pred-01, bint-pred, bint-mod, bint-is-cast, bint-fillsgn-len, bint-div2, bint-carry-01, bint-carry, bint-band-zero, bint-band-011x-neg, bint-and-011x-bits2unit, bib-upper, bib-pos-low, bib-pos-high, bib-on-bits, bib-neg-low, bib-neg-high, bib-ls-same-01, bib-ls-same, bib-lower, band-ff, band-011x, b2i-i2b-same,
• int-basic2/add-in is used by ushort-pos-02, ushort-plus, ushort-neg, ushort-inj, ushort-band-shift, ushort-band-03, ushort-band-01, ubyte-neg, ubyte-inj, sis-neg-lower, long-mod-neg-low, long-automatic, lil-carry, getsetShort-theorem, fits-law-shr, byte-mult-neg, byte-mult-256, byte-law-compl, byte-add-256, byte-011x-neg, bint-pred-02, bint-pred, bint-and-011x-bits2unit, bib-neg-high, bib-lower, band-ff,
• int-basic2/add-less is used by getsetShort-theorem, fits-law-div-stronger, bib-ls-same-01,
• int-basic2/add-zero is used by ushort-band-shift, sis-sub-2pot, sis-pos-low, sis-pos-high, sis-neg-low, sis-neg-high, short-neq-02, short-neq-01, short-max-11, short-div-ngr, short-add-min-02, short-add-max-01, lil-carry, getShort-isi, fits-law-neg, fits-law-div-stronger, div-inshort, byte-mult-256, byte-law-neg, byte-law-add-one, bint-carry-01, bib-pos-low, bib-pos-high, bib-neg-low, bib-neg-high, b2i-i2b-same,
• int-basic2/eq is used by ushort-short, ushort-pos-02, ushort-pos-01, ushort-plus, ushort-band-shift, ubyte-pos-03, sis-neg-lower, short-larger, short-in, getsetShort-theorem, byte-mult-256, byte-law-neg, byte-011x-unsgn, byte-011x-pos-01, bib-pos-high, bib-neg-low, bib-lower,
• int-basic2/ls is used by ushort-plus, ushort-band-shift, ushort-band-01, sis-ls-same-01, sis-03, short-add-min-02, getsetShort-theorem, getShort-isi, fits-law-shr-01, fits-law-div-stronger, byte-not-max, byte-nls-02, byte-mult-256, bib-ls-same-01,
• int-basic2/ls-02 is used by ushort-band-shift, sis-pos-low, getsetShort-theorem, bib-pos-low,
• int-basic2/lst-03 is used by short-nls-01,
• int-basic2/num-between is used by ushort-max-04, ushort-band-shift, ushort-band-01, sis-sub-2pot, sis-pos-high, sis-neg-low, sis-ls-same-01, short-inrange, num-i2l-pos, long-shiftzero-in, long-is-cast, lil-num, inshort-num, getsetShort-theorem, byte-mult-256, byte-law-neg, byte-127, bint-succ-notin, bint-num-04, bint-is-cast, bib-ls-same-01,
• int-basic2/succ-01 is used by ushort-max-05, ushort-band-01, short-ls, getShort-isi, fits-law-shr, byte-not-max, byte-mult-256, byte-ls-127, byte-law-neg, b2i-i2b-same,
• int-basic2/zero-01 is used by fits-law-shr,

Used from specification int-div

• int-div/Div-left is used by fits-law-div-stronger, div-inshort,
• int-div/Div-right is used by fits-law-div-stronger, div-inshort,
• int-div/abs-intro is used by div-inshort,
• int-div/div-add1-negneg is used by fits-law-shr,
• int-div/div-eq-same-01 is used by fits-law-div-stronger,
• int-div/div-ls-01 is used by short-div256,
• int-div/div-ls-zero is used by ubyte-div-lsz,
• int-div/div-minus255-256 is used by shiftright-byte-8-neg-01, shiftright-byte-8-neg,
• int-div/div-mult-neg is used by ushort-band-shift,
• int-div/div-mult-pos is used by ushort-band-shift,
• int-div/div-nle is used by short-div-ngr,
• int-div/div-nls is used by short-div-max, div-inshort,
• int-div/div-nls-01 is used by div-inshort,
• int-div/div-rec-01 is used by div-inshort,
• int-div/div-zero-02 is used by ushort-band-shift, shiftright-byte-8-pos-01, shiftright-byte-8-pos, shiftright-byte-8-neg-01, shiftright-byte-8-neg,
• int-div/div-zero-ngr is used by short-div-ngr, fits-law-shr, div-inshort,
• int-div/le-abs-numerator is used by fits-law-shr, fits-law-div-stronger,
• int-div/ls-01 is used by ushort-max-03,
• int-div/mod-grz-02 is used by mod-inshort,
• int-div/mod-mult-neg is used by ushort-band-shift,
• int-div/mod-mult-neg-03 is used by byte-mult-neg,
• int-div/mod-ngez is used by ushort-band,
• int-div/mod-nle-01 is used by ubyte-mod, short-mod-ngr, bib-ls-same-01,
• int-div/mod-nls-01 is used by mod-inshort, bib-pos-high,
• int-div/mod-nls-02 is used by short-mod-01, mod-inshort,
• int-div/mod-nls-03 is used by short-mod-01, mod-inshort,
• int-div/mod-nls-04 is used by sis-ls-same-01, fits-law-mod-01, fits-law-mod, bint-mod, bib-ls-same-01,
• int-div/mod-nls-06 is used by fits-law-mod-01, fits-law-mod, bint-mod,
• int-div/mod-zero-03 is used by short-in,
• int-div/mod-zero-05 is used by ushort-short, ushort-pos-02, ushort-band-shift-01, sis-pos-low, sis-neg-lower, sis-neg-high, sis-ls-same-01, sis-ls-same, short-mod-max, short-mod-add, short-mod, short-011x-neg, byte-mod-100x-01, byte-mod-100x, bint-band-011x-neg, bint-band-011x, bint-and-011x-bits2unit, bib-pos-low, bib-pos-high, bib-neg-low, bib-neg-high, bib-ls-same-01, bib-ls-same, bib-lower,
• int-div/modex is used by ushort-pos-02, ushort-band-shift, getsetShort-theorem, byte-mult-256, byte-law-mult-one, byte-law-add-one,
• int-div/modnum-neg-01 is used by short-mod-ngr,
• int-div/abs is used by ushort-band-shift-01,
• int-div/div-elim-negpos is used by ushort-band-shift, ushort-band-01, sis-neg-low, sis-neg-high, getsetShort-theorem, byte-mult-256, byte-law-mult-one, byte-law-add-one, bib-neg-low, bib-neg-high,
• int-div/div-elim-pos is used by bib-pos-low, bib-pos-high,
• int-div/div-elim-pospos is used by ushort-band-shift, ushort-band-01, sis-pos-low, sis-pos-high, getsetShort-theorem, byte-mult-256, byte-law-mult-one, byte-law-add-pos, byte-law-add-one,
• int-div/div-lezero is used by ushort-band-shift,
• int-div/div-ls-same is used by bint-div2,
• int-div/div-ls-zero is used by ushort-band-shift, getsetShort-theorem, bint-div2,
• int-div/div-mone-01 is used by fits-law-shr, fits-law-div, div-inshort,
• int-div/div-mult-03 is used by ushort-band-shift, sis-neg-high,
• int-div/div-mult-num is used by getsetShort-theorem,
• int-div/div-same is used by fits-law-shr,
• int-div/div-zero-ngr is used by short-div256, short-div-ngr, short-div-max, getsetShort-theorem,
• int-div/div-zero-ngr-01 is used by div-inshort,
• int-div/div-zero-nls-01 is used by div-inshort,
• int-div/div2-odd-01 is used by bib-neg-high,
• int-div/divmod-rew is used by getsetShort-theorem, ex256,
• int-div/divmult is used by getsetShort-theorem,
• int-div/mod-add is used by short-larger,
• int-div/mod-grz is used by byte-law-neg, bib-neg-high,
• int-div/mod-grz-01 is used by ubyte-mod, short-mod-ngr, fits-law-mod-01, fits-law-mod,
• int-div/mod-le-num is used by byte-law-neg,
• int-div/mod-less-01 is used by bint-mod,
• int-div/mod-ls-same-01 is used by sis-neg-low,
• int-div/mod-ls-same-02 is used by sis-pos-high, bib-neg-high,
• int-div/mod-ls-zero is used by ushort-pos-02, sis-neg-lower, sis-neg-low, sis-ls-same-01, sis-ls-same, long-mod-neg-low, long-automatic, getsetShort-theorem, byte-mult-neg, byte-law-neg, byte-law-mult-one, byte-law-add-one, bib-pos-low, bib-ls-same-01, bib-ls-same, bib-lower,
• int-div/mod-lsz is used by ushort-pos-02, sis-ls-same, long-automatic, getsetShort-theorem, bib-ls-same,
• int-div/mod-mult-pos-01 is used by byte-mult-pos,
• int-div/mod-neg is used by short-mod-ngr,
• int-div/mod-neg-01 is used by fits-law-shr, byte-law-neg,
• int-div/mod-neq-02 is used by short-mod-max, short-mod-add, short-mod,
• int-div/mod-ngez is used by ushort-pos-02, getsetShort-theorem, byte-mult-256, byte-law-mult-one,
• int-div/mod-nle is used by bib-ls-same-01,
• int-div/mod-nle-01 is used by ushort-band, getsetShort-theorem,
• int-div/mod-nle-02 is used by sis-ls-same, byte-law-neg, bib-ls-same,
• int-div/mod-nls-01 is used by sis-ls-same, bib-pos-high, bib-ls-same,
• int-div/mod-nls-02 is used by longin-mod,
• int-div/mod-nls-03 is used by longin-mod,
• int-div/mod-nls-05 is used by bint-mod,
• int-div/mod-same is used by fits-law-shr,
• int-div/mod-two-pred-01 is used by sis-neg-high,
• int-div/mod-two-pred-02 is used by bib-neg-high,
• int-div/mod-zero is used by byte-mult-256, bib-pos-high,
• int-div/mod-zero-01 is used by byte-mult-256, byte-law-add-one,
• int-div/mod-zero-02 is used by byte-law-neg,
• int-div/mod-zero-06 is used by fits-law-mod-01, fits-law-mod,
• int-div/mod-zero-07 is used by ushort-pos-01, sis-pos-upper, short-larger, bint-unsigned-01, bib-upper, bib-ls-same-01,
• int-div/mod-zero-08 is used by bib-upper,
• int-div/mod-zero-num is used by byte-mult,
• int-div/modmod is used by byte-law-neg,
• int-div/neg is used by short-div-ngr, div-inshort,
• int-div/neg-01 is used by short-div-ngr, fits-law-shr, div-inshort,
• int-div/num-ls is used by ushort-band-shift-01, short-shift-pos, getsetShort-theorem,
• int-div/nummult-le is used by sis-05, short-neq-01, byte-mult,
• int-div/nummult-le-01 is used by ushort-band-shift, fits-law-mul, bib-neg-high,
• int-div/nummult-le-02 is used by getsetShort-theorem,
• int-div/nummult-le-03 is used by ushort-band-shift, sis-05, getsetShort-theorem, byte-mult,
• int-div/nummult-ls is used by ushort-max-02, ushort-band-shift, sis-neg-high, short-nls, short-max-11, bib-neg-high,
• int-div/nummult-ls-01 is used by ushort-pos-02, ushort-band-01, sis-neg-high, longin-mult-01,
• int-div/nummult-ls-02 is used by short-nls, longin-mult-01, getShort-isi, bib-pos-low,
• int-div/nummult-ls-03 is used by ushort-pos-02, ushort-band-shift, short-neq-01, short-max-11,
• int-div/pos is used by ushort-band-shift-01,
• int-div/zero-05 is used by fits-law-div-stronger,
• int-div/zero-07 is used by fits-law-div-stronger,

Used from specification nat-basic1

• nat-basic1/f is used by ushort-neg, sis-pos-low, sis-pos-high, sis-on-bits, sis-neg-low, sis-neg-high, short-size-02, short-size, long-shiftzero-in, long-is-cast, fits-law-neg, fits-law-compl-01, fits-law-compl, fits-law-band, byte-length, byte-len, byte-law-righthift-not, byte-law-and-one, byte-bitlength-01, bint-is-cast, bint-fillsgn-len, bib-pos-high, bib-on-bits, bib-neg-low, bib-neg-high,
• nat-basic1/lf-01 is used by sis-pos-high, sis-neg-low, byte-law-righthift-not, byte-law-and-one,
• nat-basic1/lf-02 is used by sis-pos-high, sis-neg-low, byte-law-righthift-not, byte-law-and-one, bib-neg-high,
• nat-basic1/ls-02 is used by sis-pos-high, sis-neg-low, byte-law-righthift-not, byte-law-and-one,
• nat-basic1/one is used by short-size-01, byte-size-01, byte-size, byte-law-righthift-not,
• nat-basic1/one-01 is used by short-size-01, short-size, bib-neg-low,
• nat-basic1/ref-1 is used by byte-law-and-one,
• nat-basic1/trans is used by fits-law-band, byte-law-and-one,
• nat-basic1/trans-1 is used by fits-law-band, byte-law-and-one,
• nat-basic1/z is used by short-size-01, short-size, byte-size-01, byte-size,

Used from specification bitopsaux

• bitopsaux/fill-fill is used by short-law-righthift-not, byte-law-righthift-not, byte-law-and-one, bib-on-bits,
• bitopsaux/fill-lastn-04 is used by bib-pos-low,
• bitopsaux/fill-length is used by ushort-neg, ubyte-neg, sis-pos-low, sis-pos-high, sis-on-bits, byte-law-righthift-not, byte-law-and-one, bint-fillsgn-len, bib-neg-low, bib-neg-high,
• bitopsaux/fill-rec is used by sis-pos-low, byte-law-and-one,
• bitopsaux/fill-sgn-04 is used by byte-is-cast-01,
• bitopsaux/fillsgn-longer is used by sis-pos-high, sis-on-bits, sis-neg-low, byte-law-and-one, bib-pos-high, bib-on-bits,
• bitopsaux/lastn-fill-sgn is used by byte-law-and-one,
• bitopsaux/sgn-last-diff is used by bib-neg-high,
• bitopsaux/fill-empty is used by ushort-neg, ubyte-neg, sis-pos-low, sis-pos-high, byte-law-and-one, bint-and-011x-bits2unit,
• bitopsaux/fill-lastn is used by sis-on-bits, byte-law-and-one, bib-on-bits,
• bitopsaux/fill-length is used by sis-neg-high,
• bitopsaux/fill-nls is used by byte-law-and-one, bib-neg-high,
• bitopsaux/fill-rec is used by byte-law-and-one,
• bitopsaux/fill-rec-one is used by ushort-neg, sis-pos-low, sis-on-bits, bint-fillsgn-len, bib-on-bits, bib-neg-high,
• bitopsaux/fillsgn-empty is used by byte-law-and-one, bib-neg-low,
• bitopsaux/fillsgn-longer is used by sis-pos-low, byte-law-and-one, bib-pos-low,
• bitopsaux/inv-append is used by bib-neg-high,
• bitopsaux/inv-false is used by sis-neg-high, short-law-righthift-not, out-test-06, long-automatic-02, byte-mult-256, byte-len, byte-law-righthift-not, bib-neg-low,
• bitopsaux/inv-in-01 is used by bib-neg-high,
• bitopsaux/inv-mklist is used by sis-neg-high, getShort-isi,
• bitopsaux/inv-one-01 is used by ushort-neg, sis-neg-high, out-test-05, out-test-02, long-automatic-01, bib-neg-high,
• bitopsaux/invert-one is used by sis-neg-high, short-law-righthift-not, out-test-06, out-test-05, out-test-02, long-automatic-02, long-automatic-01, byte-mult-256, byte-len, byte-law-righthift-not, bib-neg-low,
• bitopsaux/invert-zero is used by ushort-neg, sis-neg-high, short-law-righthift-not, out-test-06, out-test-05, out-test-02, long-automatic-01, byte-mult-256, byte-len, byte-law-righthift-not, bib-neg-low, bib-neg-high,
• bitopsaux/sgn-base-01 is used by sis-neg-high, short-law-righthift-not, out-test-06, out-test-05, out-test-02, long-automatic-01, byte-mult-256, byte-len, byte-law-righthift-not, bib-neg-low,
• bitopsaux/sgn-empty is used by byte-law-and-one,
• bitopsaux/sgn-empty-01 is used by byte-law-and-one,
• bitopsaux/sgn-rec is used by sis-neg-high, short-law-righthift-not, out-test-06, byte-mult-256, byte-len, byte-law-righthift-not, bib-neg-low,
• bitopsaux/sgn-two-01 is used by ushort-neg, sis-neg-high, bib-neg-high,
• bitopsaux/succ-mklist is used by sis-neg-high,
• bitopsaux/succ-one is used by short-law-righthift-not, byte-law-righthift-not, bib-neg-low,
• bitopsaux/succ-rec is used by sis-neg-high, short-law-righthift-not, out-test-06, long-automatic-02, byte-mult-256, byte-len, byte-law-righthift-not, bib-neg-low,
• bitopsaux/succ-zero is used by ushort-neg, sis-neg-high, short-law-righthift-not, out-test-06, out-test-05, out-test-02, long-automatic-02, long-automatic-01, byte-mult-256, byte-len, byte-law-righthift-not, bib-neg-low, bib-neg-high,

Used from specification list-del

• list-del/bitlista/firstN-rec-01 is used by byte-law-righthift-not,
• list-del/bitlista/firstn-app-02 is used by byte-law-righthift-not,
• list-del/bitlista/lastN-all is used by sis-on-bits, sis-neg-low, byte-law-and-one, bib-on-bits,
• list-del/bitlista/lastN-append is used by sis-pos-low, sis-pos-high, sis-neg-high, bib-pos-high, bib-neg-low, bib-neg-high,
• list-del/bitlista/lastN-append-01 is used by byte-law-and-one,
• list-del/bitlista/lastN-rest-01 is used by sis-pos-high, sis-neg-low, bib-pos-high, bib-neg-low,
• list-del/bitlista/sublist-def is used by byte-law-righthift-not,
• list-del/bitlista/first-length is used by byte-law-righthift-not,
• list-del/bitlista/firstn-one is used by byte-law-righthift-not,
• list-del/bitlista/lastN-append is used by byte-law-and-one,
• list-del/bitlista/lastN-append-01 is used by sis-neg-low, byte-law-and-one,
• list-del/bitlista/lastN-empty is used by byte-law-and-one, byte-is-cast-01, bib-pos-low,
• list-del/bitlista/lastN-zero is used by out-test-06, out-test-05, out-test-02, bib-neg-low,
• list-del/bitlista/lastn-lastn-01 is used by byte-is-cast-01,
• list-del/bitlista/lastn-length is used by byte-is-cast-01,
• list-del/bitlista/lastn-length-01 is used by sis-on-bits, bib-on-bits,
• list-del/bitlista/lastn-mklist-01 is used by sis-neg-high,
• list-del/bitlista/lastn-one is used by sis-pos-low, short-law-righthift-not, long-automatic-03, long-automatic-02, long-automatic-01, byte-mult-256, byte-law-righthift-not, bib-neg-high,
• list-del/bitlista/lastn-one-01 is used by sis-on-bits, byte-law-and-one, bib-on-bits,
• list-del/bitlista/num-lastN is used by sis-pos-low, sis-on-bits, short-law-righthift-not, out-test-06, out-test-05, out-test-02, long-automatic-03, long-automatic-02, long-automatic-01, byte-mult-256, byte-law-righthift-not, byte-law-and-one, bib-on-bits, bib-neg-low, bib-neg-high,
• list-del/bitlista/restN-zero is used by byte-law-righthift-not,
• list-del/bitlista/sub-zerozero is used by short-law-righthift-not, byte-law-righthift-not,
• list-del/bitlista/sublist-num-01 is used by short-law-righthift-not, byte-law-righthift-not,

Used from specification bitlista

• bitlista/inmklist-01 is used by getShort-isi, byte-law-and-one,
• bitlista/mklist-num is used by sis-pos-low, sis-on-bits, short-law-righthift-not, byte-size, byte-law-righthift-not, byte-law-and-one, bint-fillsgn-len, bib-on-bits, bib-neg-high,
• bitlista/mklist-num-01 is used by ushort-neg, sis-on-bits, short-law-righthift-not, byte-law-righthift-not, bint-fillsgn-len, bib-neg-high,

Used from specification byte

• byte/bint-band-and-nlsz is used by bint-carry-01,