[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Lemma dependency for Specification intops

A lemma (entry) may depend on lemmas (entries) below its position, but never on lemmas above its position. This means the list is a topological order of the dependency graph. An entry 'all subs proved' means that all used lemmas are (transitively) proved.

Name: Status: Subs proved? Used:
band-011x-is-unsigned-fix-02provedall subs proved band-011x-is-unsigned-fix-03, band-commutativity,
band-011x-is-unsigned-fix-03provedall subs proved band-011x-is-unsigned-fix-01,
cast-law-xor-oneprovedall subs proved band-commutativity, cast-law-compl, bor-com, cast-law-and-one, cast-law-or-one, bxor-def-logic,
cast-law-or-oneprovedall subs proved band-commutativity, cast-law-and-one, cast-law-compl, bor-notAndNot,
band-011x-is-unsigned-fix-01provedall subs proved band-commutativity, band-associativity, band-zero, band-011x-is-unsigned-fix,
cast-law-complprovedall subs proved cast-neg-add-01, cast-law-sub-one, compl-def,
band-011x-is-unsigned-fixprovedall subs proved band-commutativity, band-associativity, band-zero, band-011x-is-unsigned-01, band-011x-is-lastn,
cast-law-multprovedall subs proved cast-law-mult-one,
cast-law-leftshiftprovedall subs proved intshiftleft-is-mult-01, cast-law-mult-one, band-commutativity,
cast-law-mult-oneprovedall subs proved cast-zero, cast-add-2pot, cast-mult-add, cast-cast, cast-mult-2pot, cast-law-add, cast-law-mult-pos,
cast-neg-add-01provedall subs proved cast-law-sub-one-01, cast-neg-add,
band-011x-is-lastnprovedall subs proved add-ones-lelen-01, and-one, bitsand-first-samesize, bitsand-app-false, band-def, band-011x-is-unsigned-03,
longshiftzero-zero-01provedall subs proved longshiftzero-zero-02, longshiftzero-band-63,
intshiftrsign-neg-02provedall subs proved intshiftrsign-2pot-neg-02, intshiftrsign-2pot-neg-01,
cast-law-subprovedall subs proved cast-law-sub-one-01, cast-law-sub-one,
longshiftzero-band-63provedall subs proved band-associativity, band-63-pos-02, band-commutativity, longshiftzero-def-unbounded,
longshiftzero-zero-02provedall subs proved shiftzero-zero, band-commutativity, band-associativity, band-63-pos-01, longshiftzero-def-unbounded,
intshiftrsign-2pot-neg-02provedall subs proved intshiftrsign-2pot-neg-01,
cast-neg-addprovedall subs proved cast-law-add-one,
cast-law-sub-one-01provedall subs proved cast-law-add-one, cast-law-neg,
cast-law-addprovedall subs proved cast-law-add-one,
cast-law-sub-oneprovedall subs proved cast-law-add-one,
band-011x-is-unsigned-03provedall subs proved band-commutativity, band-associativity, band-num, band-011x-is-unsigned-01,
longshiftzero-carry-01provedall subs proved band-max-05, band-max-02, shiftright-pos-div, band-32-not-neg, shiftzero-pos, band-commutativity, band-associativity, band-63-pos-02, longshiftzero-def-unbounded,
longshiftright-2pot-posprovedall subs proved shiftright-pos-div, band-commutativity, band-associativity, band-63-pos-02, longshiftright-def-unbounded,
intshiftrzero-prop-01provedall subs proved intshiftrsign32, band-ls-zero-01, band-associativity, band-max-02, band-011x-eq-01, band-commutativity, band-011x-neg-03, intshiftleft, compl-def, intshiftrzero-def,
intshiftrsign-pos-numprovedall subs proved intshiftrsign-2pot-pos,
intshiftrsign-pos-8provedall subs proved intshiftrsign-2pot-pos,
intshiftrsign-neg-01provedall subs proved intshiftrsign-2pot-neg,
intshiftrsign-abs-leprovedall subs proved intshiftrsign-2pot-pos, intshiftrsign-band31, intshiftrsign-zero, intshiftrsign-2pot-neg-01, band-notneg, band-commutativity, band-associativity, band-max-05,
intshiftright-ls-02provedall subs proved intshiftrsign-band31, intshiftrsign-zero, intshiftrsign-2pot-neg-01, band-ls-zero-01, band-max-05, band-commutativity, band-associativity, band-le-zero,
band-63-pos-01provedall subs proved band-63-pos,
band-63-pos-02provedall subs proved band-63-pos,
band-011x-eq-01provedall subs proved band-011x-eq,
intshiftrsign-2pot-negprovedall subs proved intshiftrsign-rec-neg, intshiftrsign-zero,
intshiftrsign-2pot-posprovedall subs proved intshiftrsign-rec-pos, intshiftrsign-zero,
intshiftrsign-2pot-neg-01provedall subs proved intshiftrsign-rec-neg, intshiftrsign-zero,
cast-law-add-oneprovedall subs proved cast-mult-2pot, cast-add-2pot, cast-mult-add, cast-law-add-pos-01, cast-law-add-pos,
band-011x-is-unsigned-01provedall subs proved band-011x-is-unsigned,
intshiftright-unbounded-sameprovedall subs proved shiftrsign-01, band-commutativity, band-associativity, band-31-pos, intshiftrsign,
intshiftright-lsprovedall subs proved intshiftright-ls-01,
intshiftleft-band31provedall subs proved band-associativity, band-31-pos, band-commutativity, intshiftleft,
divide-by-10provedall subs proved shiftright-pos-div, shiftzero-pos, band-commutativity, band-associativity, band-31-pos, intshiftzero-def-unbounded,
band-31-pos-02provedall subs proved band-31-pos,
band-31-pos-01provedall subs proved band-31-pos,
band-011x-neg-04provedall subs proved band-commutativity, band-011x-neg-03,
intshiftrsign32provedall subs proved band-max-02, band-ls-zero-01, band-associativity, band-commutativity, intshiftrsign,
intshiftrsign-rec-posprovedall subs proved band-commutativity, band-associativity, band-011x-pos-01, band-011x-pos-02, intshiftrsign,
intshiftrsign-rec-negprovedall subs proved band-commutativity, band-associativity, bitsand-oner, band-num, band-011x-pos-02, intshiftrsign,
intshiftright-ls-01provedall subs proved band-011x-pos-02, intshiftrsign,
cast-law-negprovedall subs proved cast-zero, cast-mult-2pot, cast-mult-neg-01, cast-add-2pot-01, cast-add-2pot, cast-mult-add, cast-mult-neg-02, cast-law-neg-pos,
intshiftleft-is-mult-01provedall subs proved band-011x-pos-02, band-011x-neg-02, intshiftleft,
cast-law-add-pos-01provedall subs proved cast-mult-add, cast-mod-pos-low, cast-mod-pos-high, cast-law-add-pos,
band-63-posprovedall subs proved band-011x-pos-02,
band-31-posprovedall subs proved band-011x-pos-02,
band-011x-neg-03provedall subs proved band-011x-pos-02, band-011x-neg-02,
band-011x-is-unsignedprovedall subs proved band-011x-neg, band-associativity, band-commutativity, band-011x-neg-02, band-011x-pos,
band-011x-eqprovedall subs proved band-011x-neg-02, band-commutativity, band-associativity, band-011x-neg-01, band-011x-pos-02,
longshiftzero-zero-03provedall subs proved band-commutativity, band-associativity, band-notneg, shiftright-pos-div, longshiftzero-def-pos,
band-one-is-mod2provedall subs proved band-011x-pos-02,
band-011xprovedall subs proved band-011x-neg-02, band-commutativity,
longshiftzero-def-posprovedall subs proved band-commutativity, longshiftright-def-unbounded, longshiftzero-pos,
band-max-02provedall subs proved band-commutativity, band-associativity, band-max-03,
cast-law-neg-posprovedall subs proved cast-sub-2pot, cast-mult-neg-02, cast-mod-pos-low, cast-mod-pos-high,
cast-law-add-posprovedall subs proved cast-add-2pot, cast-mult-pos, cast-mod-pos-low, cast-mod-pos-high,
band-011x-pos-02provedall subs proved band-commutativity, band-associativity, band-011x-pos-01,
band-011x-neg-02provedall subs proved band-commutativity, band-associativity, band-011x-neg-01,
longshiftzero-not-neg-01provedall subs proved band-commutativity, shiftzero-not-neg, longshiftzero-def-unbounded, longshiftzero-not-neg,
longshiftzero-carryprovedall subs proved band-commutativity, band-associativity, band-32-not-neg, longshiftzero-not-neg,
intshiftrsign-zero-01provedall subs proved intshiftrsign-if, band-le-zero, band-ls-zero-01, band-associativity, band-commutativity,
bxor-zeroprovedall subs proved bor-zero, band-zero, band-commutativity, band-associativity, band-minus-one, bcompl-num, bxor-def-logic,
bxor-minus-oneprovedall subs proved bor-com, bor-zero, band-minus-one, band-commutativity, band-associativity, band-zero, bcompl-num, bxor-def-logic,
bxor-comprovedall subs proved bor-com, band-commutativity, bxor-def-logic,
bxor-bitlengthprovedall subs proved band-commutativity, bcompl-size-01, band-bitlength, bor-bitlength, bxor-def-logic,
bor-shift-plusprovedall subs proved intshiftleft-is-mult, bor-2pot-plus-01, bor-2pot-plus,
band-max-04provedall subs proved band-commutativity, band-associativity, band-255-pos, band-255-neg,
longshiftzero-posprovedall subs proved band-commutativity, shiftzero-pos, longshiftright-def-unbounded, longshiftzero-def-unbounded,
longshiftzero-not-negprovedall subs proved shiftright-not-neg, shiftzero-pos, longshiftzero-def-unbounded,
band-32-not-negprovedall subs proved band-commutativity, band-associativity, band-notneg,
band-le-zeroprovedall subs proved band-associativity, band-notneg, band-commutativity,
band-ls-zero-01provedall subs proved band-commutativity, band-associativity, band-notneg,
intshiftrsign-zeroprovedall subs proved band-commutativity, band-associativity, bitsand-zerol, band-num, intshiftrsign,
intshiftrsign-band31provedall subs proved intshiftrsign-if, band-commutativity, band-idempotent,
cast-sub-2potprovedall subs proved cast-mult-add,
cast-mult-neg-02provedall subs proved cast-mult-add,
cast-add-2pot-01provedall subs proved cast-mult-add,
cast-law-mult-posprovedall subs proved cast-zero, cast-mult-2pot, cast-mod-pos-low, cast-mod-pos-high, cast-mult-add, cast-mult-pos,
cast-add-2potprovedall subs proved cast-mult-add,
bor-zeroprovedall subs proved bcompl-absorption, band-commutativity, band-associativity, band-minus-one, bcompl-num, bor-notAndNot,
bor-comprovedall subs proved band-commutativity, bor-notAndNot,
bor-bitlengthprovedall subs proved bcompl-size-01, band-bitlength, band-commutativity, bcompl-size, bor-notAndNot,
intshiftleft-is-multprovedall subs proved band-011x-pos, intshiftleft,
band-255-negprovedall subs proved band-commutativity, band-associativity, band-def, band-011x-neg,
band-255-posprovedall subs proved band-commutativity, band-associativity, band-def, band-011x-pos,
band-max-03provedall subs proved band-commutativity, band-associativity, band-max-01,
band-011x-pos-01provedall subs proved band-commutativity, band-associativity, band-011x-pos,
band-011x-neg-01provedall subs proved band-commutativity, band-associativity, band-011x-neg,
intshiftzero-moneprovedall subs proved and-two, bitsand-rec, band-commutativity, band-associativity, band-num, intshiftrzero-def,
intshiftright-moneprovedall subs proved intshiftrsign-num, band-commutativity, band-associativity, and-two, and-rec-10, band-num,
cast-law-shift-snd-zrprovedall subs proved band-commutativity, cast-band, intshiftrzero-def,
cast-law-shift-snd-rprovedall subs proved band-commutativity, cast-band, intshiftrsign,
cast-law-shift-snd-lprovedall subs proved band-commutativity, cast-band, intshiftleft,
bor-assocprovedall subs proved band-commutativity, band-associativity, bcompl-absorption, bor-notAndNot,
band-mod256-posprovedall subs proved band-associativity, band-def, band-011x-pos, band-commutativity,
band-mod256-negprovedall subs proved band-associativity, band-def, band-011x-neg, band-commutativity,
band-min-02provedall subs proved bitsand-len-true, and-com, and-notempty-09, band-def, band-notneg-01, band-notneg, band-commutativity,
band-min-01provedall subs proved bitsand-len-true, and-com, and-notempty-09, band-def, band-notneg-01, band-notneg, band-commutativity,
band-max-06provedall subs proved band-commutativity, band-associativity, band-max-05,
band-65535-posprovedall subs proved band-commutativity, band-associativity, band-def, band-011x-pos,
band-65535-negprovedall subs proved band-commutativity, band-associativity, band-def, band-011x-neg,
band-63-lezeroprovedall subs proved band-associativity, band-notneg, band-commutativity,
band-011x-zeroprovedall subs proved band-associativity, band-notneg, band-commutativity,
longshiftzero-def-unboundedprovedall subs proved band-commutativity, shiftrzero-def-01, longshiftrzero-def,
longshiftright-def-unboundedprovedall subs proved band-commutativity, shiftrsign-01, longshiftrsign,
band-idempotentprovedall subs proved band-idempotent-01, band-commutativity, band-associativity,
intshiftrsign-numprovedall subs proved intshiftrsign-if, band-commutativity,
intshiftzero-def-unboundedprovedall subs proved band-commutativity, shiftrzero-def-01, intshiftrzero-def,
cast-bandprovedall subs proved bitsand-cast-05, and-bits2int-sgn, and-rec-02, band-def, cast-def,
cast-mult-addprovedall subs proved cast-mult-add-h, cast-mult-pos, cast-mult-2pot, cast-mult-add-h-01, cast-mult-neg,
bor-notAndNotprovedall subs proved and-com, and-sgn, and-notempty, or-invandinv, band-commutativity, band-associativity, band-def, bcompl-def, bor-def,
band-max-05provedall subs proved band-commutativity, band-associativity, band-max,
band-max-01provedall subs proved band-commutativity, band-associativity, band-max,
band-notnegprovedall subs proved band-commutativity, band-associativity, band-notneg-01,
band-numprovedall subs proved band-commutativity, band-associativity, band-def,
band-011x-posprovedall subs proved and-notempty, and-notempty-06, and-pos, and-rec-02, and-rec, and-rec-04, band-associativity, band-def,
band-011x-negprovedall subs proved and-011x-neg, and-notempty, and-first, band-commutativity, band-associativity, band-def,
intshiftright-def-unboundedprovedall subs proved band-commutativity, shiftrsign-01, intshiftrsign,
intshiftleft-numprovedall subs proved band-commutativity, intshiftleft,
intshiftleft-is-shiftleftprovedall subs proved band-commutativity, intshiftleft, shiftleft-01,
bor-256-plus-01provedall subs proved bor-def, bor-2pot-plus-02,
cast-mult-add-h-01provedall subs proved cast-add-2pot-h, cast-mult-pos,
cast-mult-add-hprovedall subs proved cast-mult-2pot, cast-zero, cast-add-2pot-h, cast-mult-neg,
cast-law-and-oneprovedall subs proved bitsand-cast-01, and-sgn, and-notempty, and-notempty-09, cast-def, band-def,
cast-mult-neg-01provedall subs proved cast-mult-2pot,
bitsand-cast-05provedall subs proved and-notone-01, and-notempty-02, bitsand-app-true, and-com, bitsand-first-samesize, bitsand-app-false, bitsand-app-zeros-01, bitsand-app-ones, bitsand-cast-04,
bxor-def-logicprovedall subs proved bitsxor-is-orand, bitsor-com, bitsor-bi-sgn, and-com, and-sgn, and-notempty, bor-def, band-def, bcompl-def, bxor-def,
bor-2pot-plus-02provedall subs proved bor-def, bor-2pot-plus-01, bor-2pot-plus,
band-notneg-01provedall subs proved and-first, and-notempty-09, band-def,
band-maxprovedall subs proved and-first, and-notempty-09, bitsand-oner, bitsand-zeror, and-rec, and-rec-02, and-rec-01, and-rec-04, band-def,
and-posprovedall subs proved and-first,
band-commutativityprovedall subs proved and-com, band-associativity, band-def,
cast-ifprovedall subs proved cast-size-fits-01, cast-mod-neg-high, cast-mod-neg-low, cast-mod-pos-high, cast-mod-pos-low,
bor-65536-plusprovedall subs proved bor-2pot-plus-01, bor-2pot-plus,
bor-256-plusprovedall subs proved bor-def, bor-2pot-plus,
bitsand-castprovedall subs proved add-ones-lelen-01, and-zero-02, and-onel-01, bitsand-zeros-01, bitsand-zeros, and-notone, and-notempty, bitsand-len-false, and-notempty-01, bitsand-len-true, add-ones-grlen-02, add-ones-grlen, add-ones-lelen, bitsand-app, and-com, and-first, and-notempty-02, bitsand-app-true, bitsand-app-false,
and-one-01provedall subs proved and-notone-01, and-com, and-notone-03,
and-notone-02provedall subs proved and-notone, and-notempty-01,
shiftzero-not-negprovedall subs proved shiftright-not-neg, shiftrzero-def-01, shiftzero-pos,
cast-add-2pot-hprovedall subs proved cast-mod-pos-low, cast-mod-pos-high, cast-mod-neg-high, cast-mod-neg-low,
cast-mult-negprovedall subs proved cast-mod-neg-low, cast-mod-neg-high,
bitsand-cast-01provedall subs proved and-notempty-01, bitsand-len-true, bitsand-len-false, bitsand-app, and-com, bitsand-app-true, bitsand-app-false, bitsand-fillsgn,
cast-mult-posprovedall subs proved cast-mod-pos-low, cast-mod-pos-high,
cast-mult-2potprovedall subs proved cast-mod-neg-high, cast-mod-pos-low,
cast-size-fits-01provedall subs proved cast-zero, cast-size-fits,
and-bits2int-sgnprovedall subs proved and-sgn,
bitsor-bi-sgnprovedall subs proved bitsor-empty, bitsor-com, bitsor-first, bitsor-first-02, bitsor-first-01, bitsor-sgn-in, bitsor-bi-ones, bitsor-bi-zeroes, bitsor-zerol, or-rec-04, or-rec-03, or-rec-02, or-rec-01, or-rec,
bor-2pot-plus-01provedall subs proved add-ones-grlen-01, and-notempty, add-ones-lelen-01, and-size-one-01, and-size-one, and-com, and-rec-01, or-invandinv, bor-def,
bor-2pot-plusprovedall subs proved add-ones-grlen-01, and-notempty, add-ones-lelen-01, and-size-one-01, and-size-one, and-com, and-onel-01, or-invandinv, bor-def,
bitsand-cast-04provedall subs proved bitsand-app-zeros, and-com, bitsand-app-ones, bitsand-app-false,
bitsand-app-zeros-01provedall subs proved and-notempty-08, bitsand-onein, and-notempty-02, bitsand-zero-in, bitsand-zeros-02, and-zero-02, and-rec-02, and-rec-01, and-rec,
band-associativityprovedall subs proved and-ass, and-com, and-sgn, and-notempty, and-notempty-09, band-def,
and-firstprovedall subs proved and-rec-04, and-rec-03, and-rec-02, and-rec-01, and-rec, and-notempty-06,
and-notone-03provedall subs proved and-notone-01,
and-notoneprovedall subs proved and-notone-01, and-notempty-01,
shiftzero-max-negprovedall subs proved shiftzero-zero, shiftzero-by-one-01, shiftright-not-ls-01, shiftright-rec-pos, shiftzero-minus-one, shiftzero-rec-neg-shorter, shiftzero-rec-neg-longer,
shiftright-shiftprovedall subs proved shiftright-not-neg, shiftright-rec-neg, rightshift-zero, shiftright-pos-div,
shiftright-not-leprovedall subs proved shiftright-not-ls-01, shiftright-rec-pos-01, rightshift-zero, shiftright-zero,
bxor-flip-one-bitprovedall subs proved bitsxor-zeros-01, bitsxor-first, bitsxor-rec-02, bitsxor-rec-01, bitsxor-append-same-size, bitsxor-zerol, bitsxor-empty, bxor-def,
band-negprovedall subs proved and-false, and-notempty-09, band-def,
shiftright-not-ls-01provedall subs proved shiftright-is-le,
shiftright-not-negprovedall subs proved shiftright-pos-div-01,
cast-size-fitsprovedall subs proved cast-mod-in,
cast-zeroprovedall subs proved cast-mod-in,
cast-mod-neg-lowprovedall subs proved cast-def, cast-mod-in,
cast-mod-neg-highprovedall subs proved cast-def, cast-mod-in,
cast-mod-pos-highprovedall subs proved cast-def, cast-mod-in,
cast-mod-pos-lowprovedall subs proved cast-def, cast-mod-in,
bitsxor-firstprovedall subs proved bitsxor-bit, bitsxor-append-same-size,
band-minus-oneprovedall subs proved bitsand-true, band-def,
band-bitlengthprovedall subs proved bitsand-len-true, bitsand-len-false, and-com, and-notempty-09, band-def,
add-ones-grlen-01provedall subs proved add-ones-grlen, and-com,
bitsor-bi-zeroesprovedall subs proved bitsor-zeroes-samelen, or-rec-02, bitsor-app, bitsor-zeroes-false, bitsor-zeroes-true,
bitsor-bi-onesprovedall subs proved bitsor-ones-samelen, or-rec-01, bitsor-app, bitsor-ones-true, bitsor-ones-false,
bitsor-sgn-inprovedall subs proved bitsor-zeroes-samelen, or-rec-02, bitsor-zeroes-false, bitsor-zeroes-true, or-rec-04, bitsor-ones-samelen, or-rec-01, bitsor-app, bitsor-ones-true, bitsor-ones-false, or-rec-03, bitsor-mklist-in,
bitsor-first-01provedall subs proved bitsor-com, bitsor-first, bitsor-first-02, bitsor-empty,
bitsand-app-onesprovedall subs proved add-ones-lelen, add-ones-grlen-02, and-onel-02, and-rec-02, and-rec,
bitsand-app-zerosprovedall subs proved and-notempty, bitsand-onein, and-notempty-05, bitsand-zero-in, bitsand-zeros-01, and-rec-06, bitsand-zeros, and-zero-01, and-rec-02, and-rec-01, and-rec,
bitsand-fillsgnprovedall subs proved and-notempty, bitsand-app, add-ones-lelen, add-ones-grlen, and-onel-01, bitsand-zeros, bitsand-zeros-01, and-zero-02, and-rec-03, and-rec-02, and-zero-03, and-rec-01, and-rec,
bitsand-zeros-02provedall subs proved bitsand-zeros-01, bitsand-zeros,
and-falseprovedall subs proved and-notempty-05, and-oner, and-onel-02, and-rec,
band-idempotent-01provedall subs proved bitsand-idempotent, band-def,
and-011x-negprovedall subs proved and-notempty-05, and-oner-01, and-zero-01, and-rec,
add-ones-lelen-01provedall subs proved add-ones-lelen, and-com,
and-notone-01provedall subs proved and-notempty-05, and-zero-01, and-rec-03, and-zero-03, and-rec,
and-notempty-06provedall subs proved and-notempty-05,
and-sgnprovedall subs proved and-notempty, and-insgn, and-onesin, and-zerosin, bitsand-zerol, and-onel-01, and-zero-02, and-rec-04, and-rec-03, and-rec-02, and-rec-01, and-rec,
shiftright-rec-8provedall subs proved shiftright-pos-div-01,
shiftright-not-lsprovedall subs proved shiftright-is-le,
cast-nlsprovedall subs proved cast-min,
band-minprovedall subs proved and-notempty-09, and-rec, and-onel-01, and-zero-02, band-def,
and-trueprovedall subs proved and-notempty-05, and-rec-04, and-rec-03, and-rec-02, and-rec-01, and-rec, and-oner-01, and-onel-01,
shiftright-pos-div-01provedall subs proved shiftright-pos-div, shiftright-abs,
shiftright-is-leprovedall subs proved shiftright-zero, shiftright-not-pos-01, rightshift-zero, shiftright-rec-pos-01,
and-twoprovedall subs proved and-one, and-rec,
cast-minprovedall subs proved cast-length, cast-one, cast-max,
cast-mod-inprovedall subs proved cast-mod-ls-most, cast-mod-ls,
bitsxor-zeros-01provedall subs proved bitsxor-zeros,
bitsxor-is-orandprovedall subs proved bitsxor-empty, bitsor-empty, bitsxor-rec-01, and-notempty, or-rec, bitsxor-rec-01-01, bitsxor-rec-02, and-onel-01, bitsxor-rec-04, or-rec-02, bitsxor-rec-03, or-rec-04, and-zero-02, and-rec-03, and-rec-02, and-rec-01, and-rec,
and-size-oneprovedall subs proved and-rec-03, and-onel-01, and-rec,
and-size-one-01provedall subs proved and-one, and-onel-01, and-rec,
bitsxor-append-same-sizeprovedall subs proved bitsxor-bit, bitsxor-rec-01,
bitsor-zeroes-samelenprovedall subs proved bitsor-zeroes-false, bitsor-zeroes-true,
bitsor-first-02provedall subs proved bitsor-empty, or-rec-04, or-rec-02, or-rec,
bitsor-firstprovedall subs proved bitsor-empty, or-rec-03, or-rec-02, or-rec-01, or-rec,
bitsor-comprovedall subs proved or-last, or-rec-04, or-rec-03, or-rec-02, or-rec-01, or-rec,
bitsor-ones-samelenprovedall subs proved bitsor-ones-true, bitsor-ones-false,
bitsand-app-trueprovedall subs proved and-rec-01, and-oner-01, and-rec,
bitsand-appprovedall subs proved and-one, and-rec,
and-notempty-02provedall subs proved and-notempty,
and-notempty-08provedall subs proved and-notempty,
bitsand-zerosprovedall subs proved and-zero-01, and-rec-03, and-oner-01, and-rec,
bitsand-zeros-01provedall subs proved and-zero-03, and-rec,
bitsand-zero-inprovedall subs proved and-zero-02, and-rec-03, and-rec-02, and-rec-01, and-rec, and-onesin,
bitsand-oneinprovedall subs proved and-zerosin, and-zero-02, and-rec-02, and-rec-01, and-rec,
bitsand-trueprovedall subs proved and-onel-01,
bitsand-idempotentprovedall subs proved and-one, and-rec-01, and-rec,
bitsand-len-falseprovedall subs proved and-zero-03, and-rec,
bitsand-len-trueprovedall subs proved and-oner-01, and-rec,
and-notempty-09provedall subs proved and-notempty,
and-assprovedall subs proved bitsand-onel, bitsand-zerol, and-notempty, and-rec-02, and-rec-01, and-oner-01, and-zero-03, and-zero-02, and-rec-03, and-rec,
bitsand-app-falseprovedall subs proved and-rec-02, and-zero-03, and-rec,
bitsand-first-samesizeprovedall subs proved and-one, and-zero-03, and-rec-01, and-rec,
and-insgnprovedall subs proved and-onesin, and-zerosin, bitsand-zerol, and-onel-01, and-zero-02, and-rec-04, and-rec-03, and-rec-02, and-rec-01, and-rec,
and-notempty-01provedall subs proved and-notempty,
and-onerprovedall subs proved and-oner-01,
and-notempty-05provedall subs proved and-notempty,
add-ones-lelenprovedall subs proved and-onel-02, and-rec,
and-comprovedall subs proved and-onel-01, and-zero-02, and-oner-01, and-zero-03, and-rec-04, and-rec-03, and-rec-02, and-rec-01, and-rec,
add-ones-grlenprovedall subs proved and-rec-01, and-onel-02, and-oner-01, and-rec,
shiftzero-max-neg-01provedall subs proved shiftzero-by-one-01, shiftright-pos-div, shiftzero-minus-one, shiftzero-rec-neg-shorter, shiftzero-rec-neg-longer,
shiftright-rec-8-negprovedall subs proved shiftright-rec-neg, shiftright-neg-mone, shiftright-neg-div, rightshift-zero,
shiftright-neg-div-02provedall subs proved shiftright-neg-div,
shiftright-neg-div-01provedall subs proved shiftright-neg-div,
or-two-08provedall subs proved or-last,
or-two-07provedall subs proved or-last,
or-two-06provedall subs proved or-last,
or-two-05provedall subs proved or-last,
or-two-04provedall subs proved or-last,
or-two-03provedall subs proved or-last,
cast-nls-01provedall subs proved cast-max,
and-two-09provedall subs proved and-rec-08,
and-two-08provedall subs proved and-rec-08,
and-two-07provedall subs proved and-rec-08,
and-two-06provedall subs proved and-rec-08,
and-two-05provedall subs proved and-rec-07,
and-two-04provedall subs proved and-rec-07,
and-two-03provedall subs proved and-rec-07,
and-two-02provedall subs proved and-rec-07,
and-onesprovedall subs proved and-onel-02, and-zero-03, and-rec,
and-notempty-07provedall subs proved and-notempty,
and-notempty-04provedall subs proved and-notempty,
and-notempty-03provedall subs proved and-notempty,
shiftzero-by-one-01provedall subs proved shiftzero-by-one,
shiftright-neg-divprovedall subs proved rightshift-zero, shiftright-rec-neg, shiftright-abs,
shiftright-rec-pos-01provedall subs proved shiftright-rec-pos, shiftright-abs,
shiftzero-zeroprovedall subs proved rightshift-zero, shiftrzero-def-01, shiftzero-pos,
shiftright-pos-divprovedall subs proved shiftright-zero, rightshift-zero, shiftright-rec-pos,
cast-mod-lsprovedall subs proved cast-mod-ls-neg, cast-mod-ls-pos,
cast-maxprovedall subs proved cast-length, cast-one,
cast-castprovedall subs proved cast-law-absorption,
bcompl-sizeprovedall subs proved bcompl-size-01,
bcompl-absorptionprovedall subs proved compl-def,
or-invandinvprovedall subs proved and-rec, and-rec-02, and-rec-01, and-rec-04, and-rec-03, or-rec-04, or-rec-03, or-rec-02, or-rec-01, or-rec,
bitsxor-zerosprovedall subs proved bitsxor-rec-02, bitsxor-rec-01,
bitsxor-emptyprovedall subs proved bitsxor-rec-04, bitsxor-rec-03, bitsxor-rec-02, bitsxor-rec-01-01, bitsxor-rec-01,
bitsxor-bitprovedall subs proved bitsxor-rec-02, bitsxor-rec-01-01,
bitsor-mklist-inprovedall subs proved bitsor-onel, or-rec-04, bitsor-zerol, or-rec-03, or-rec-02, or-rec-01, or-rec,
or-lastprovedall subs proved or-rec,
bitsor-zeroes-trueprovedall subs proved or-rec-04, or-rec-01, or-rec,
bitsor-zeroes-falseprovedall subs proved or-rec-04, or-rec-02, or-rec-01, or-rec,
bitsor-emptyprovedall subs proved or-rec-04, or-rec-03, or-rec-02, or-rec-01, or-rec,
bitsor-ones-falseprovedall subs proved or-rec-03, or-rec-02, or-rec-04, or-rec,
bitsor-ones-trueprovedall subs proved or-rec-03, or-rec-01, or-rec,
bitsor-appprovedall subs proved or-rec-02, or-rec-01, or-rec,
and-rec-06provedall subs proved and-rec,
add-ones-grlen-02provedall subs proved and-rec-02, and-rec-01, and-rec,
band-zeroprovedall subs proved and-rec-04, band-def,
and-rec-08provedall subs proved and-rec,
and-rec-07provedall subs proved and-rec,
and-oneprovedall subs proved and-rec-02, and-rec-01,
and-zerosinprovedall subs proved and-rec-04, and-rec-03, and-rec-02, and-rec-01, and-rec,
and-onesinprovedall subs proved and-rec-04, and-rec-03, and-rec-02, and-rec-01, and-rec,
and-onel-01provedall subs proved and-rec-03,
and-zero-02provedall subs proved and-rec-04,
and-zero-03provedall subs proved and-rec-02,
and-notemptyprovedall subs proved and-rec-04, and-rec-03, and-rec-02, and-rec-01, and-rec,
and-zero-01provedall subs proved and-rec-04,
and-oner-01provedall subs proved and-rec-01,
and-onel-02provedall subs proved and-rec-03,
shiftzero-zero-size-01provedall subs proved shiftzero-zero-size,
shiftright-not-posprovedall subs proved shiftright-not-pos-01,
or-two-02provedall subs proved or-rec,
or-two-01provedall subs proved or-rec,
cast-law-commprovedall subs proved cast-help-comm,
bitsand-false-01provedall subs proved and-rec-02,
bitsand-falseprovedall subs proved and-rec-04,
and-rec-09provedall subs proved and-rec,
shiftzero-zero-sizeprovedall subs proved shiftrsign-01, shiftrzero-def-01,
shiftzero-rec-neg-longerprovedall subs proved shiftrzero-def-01,
shiftzero-rec-neg-shorterprovedall subs proved shiftrzero-def-01,
shiftzero-minus-oneprovedall subs proved shiftrsign-01, shiftrzero-def-01,
shiftzero-by-oneprovedall subs proved shiftrzero-def-01,
shiftright-neg-moneprovedall subs proved shiftrsign-01,
shiftright-rec-posprovedall subs proved shiftrsign-01,
shiftright-absprovedall subs proved shiftrsign-01,
shiftright-rec-negprovedall subs proved shiftrsign-01,
rightshift-zeroprovedall subs proved shiftrsign-01,
shiftright-not-pos-01provedall subs proved shiftrsign-01,
shiftright-zeroprovedall subs proved shiftrsign-01,
intshiftrsign-ifprovedall subs proved intshiftrsign,
and-rec-10provedall subs proved bitsand-rec,
shiftzero-posprovedall subs proved shiftrsign-01, shiftrzero-def-01,
cast-mod-ls-posprovedall subs proved cast-def,
cast-mod-ls-negprovedall subs proved cast-def,
cast-mod-ls-mostprovedall subs proved cast-def,
cast-oneprovedall subs proved cast-def,
cast-lengthprovedall subs proved cast-def,
cast-help-commprovedall subs proved cast-def,
cast-law-absorptionprovedall subs proved cast-def,
bcompl-numprovedall subs proved bcompl-def,
bitsxor-rec-03provedall subs proved bitsxor-onel,
bitsxor-rec-04provedall subs proved bitsxor-zerol,
bitsxor-rec-01-01provedall subs proved bitsxor-oner,
bitsxor-rec-02provedall subs proved bitsxor-zeror,
bitsxor-rec-01provedall subs proved bitsxor-rec,
or-rec-03provedall subs proved bitsor-onel,
or-rec-04provedall subs proved bitsor-zerol,
or-recprovedall subs proved bitsor-rec,
or-rec-01provedall subs proved bitsor-oner,
or-rec-02provedall subs proved bitsor-zeror,
bcompl-size-01provedall subs proved bcompl-def,
compl-defprovedall subs proved bcompl-def,
and-rec-04provedall subs proved bitsand-zerol,
and-rec-03provedall subs proved bitsand-onel,
and-rec-02provedall subs proved bitsand-zeror,
and-recprovedall subs proved bitsand-rec,
and-rec-01provedall subs proved bitsand-oner,
shiftright-minus-oneprovedall subs proved shiftrsign-01,
or-twoprovedall subs proved bitsor-rec,
or-rec-08provedall subs proved bitsor-rec,
or-rec-07provedall subs proved bitsor-rec,
or-rec-06provedall subs proved bitsor-rec,
or-rec-05provedall subs proved bitsor-rec,
longshiftzero-zeroprovedall subs proved longshiftrzero-def,
compl-zeroprovedall subs proved bcompl-def,
bxor-numprovedall subs proved bxor-def,
bor-numprovedall subs proved bor-def,
bits2int-is-cast-01provedall subs proved cast-def,
bits2int-is-castprovedall subs proved cast-def,
and-rec-12provedall subs proved bitsand-rec,
and-rec-11provedall subs proved bitsand-rec,
and-rec-05provedall subs proved bitsand-rec,
bitsor-zeroraxiom
bitsor-oneraxiom
bitsor-recaxiom
longshiftrzero-defaxiom
longshiftrsignaxiom
shiftrzero-def-01axiom
shiftrsign-01axiom
shiftleft-01axiom
intshiftrzero-defaxiom
intshiftrsignaxiom
intshiftleftaxiom
bxor-defaxiom
bor-defaxiom
bitsxor-zerolaxiom
bitsxor-onelaxiom
bitsxor-zeroraxiom
bitsxor-oneraxiom
bitsxor-recaxiom
bitsor-onelaxiom
bitsor-zerolaxiom
cast-defaxiom
bcompl-defaxiom
band-defaxiom
bitsand-zeroraxiom
bitsand-oneraxiom
bitsand-recaxiom
bitsand-zerolaxiom
bitsand-onelaxiom