[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 bytes

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:
setShortInt-theoremprovedall subs proved setShort-theorem-01,
setShort-theorem-01provedall subs proved fillsgn-len-short, setShort-theorem, fillsgn-not-empty,
fillsgn-len-shortprovedall subs proved int2bytes-len-ls-01, int2bytes-len-ls-neg-01, int2bytes-len-ls-neg, int2bytes-len-ls, int2bytes-empty, fillsgn-length-02,
int2bytes-len-ls-neg-01provedall subs proved int2bytes-len-le-neg-03,
rightshift-8-01-01provedall subs proved bytes2int-first-gez, bytes2int-mklist-mones-01, bytes2int-first-lez, bytes2int-mklist-zeros-01, fillsgn-longer, int2bytes-byte, int2bytes-len-le-neg-03, int2bytes-len-le-neg-02, bytes2int-mklist-mones, int2bytes-len-ls-upper, int2bytes-len-le-upper, bytes2int-mklist-zeros, fillsgn-pos, int2bytes-empty, int2int, fillsgn-neg, rightshift-8-01,
int2bytes-len-ls-neg-03provedall subs proved int2bytes-len-le-neg-01,
int2bytes-len-eq-neg-01provedall subs proved int2bytes-empty, int2bytes-len-le-neg-03, int2bytes-len-le-neg-01,
fillsgn-shortprovedall subs proved fillsgn-pos, fillsgn-neg, int2bytes-byte-01, bytes2int-one, bytes2bytes-fillsgn, fillsgn-length-01, fillsgn-longer, int2bytes-empty, fillsgn-length,
setShort-theoremprovedall subs proved fillsgn-pos, bytes2int-one, fillsgn-neg, int2bytes-byte-01, fillsgn-longer, int2bytes-len-one, int2bytes-len-one-01, int2bytes-empty, int2bytes-fillsgn-rec,
int2bytes-len-ls-upperprovedall subs proved int2bytes-len-ls,
int2bytes-len-le-neg-01provedall subs proved no-leading-zero-04, int2bytes-byte, int2bytes-minus-one, int2bytes-empty, int2int, bytes2int-size-05, bytes2int-size-07,
int2bytes-len-le-neg-03provedall subs proved no-leading-zero-04, int2bytes-byte, int2bytes-minus-one, int2bytes-empty, int2int, bytes2int-size-07, bytes2int-size-05,
bytes2bytes-fillsgnprovedall subs proved bytes2bytes-identity-01, bytes2bytes-fix, fillsgn-fix, fillsgn-longer,
setInt-theoremprovedall subs proved fillsgn-longer, int2int, int2bytes-byte, int2bytes-rec-shift, int2bytes-empty, int2bytes-fillsgn-rec, fillsgn-pos, bytes2int-one, fillsgn-neg, int2bytes-byte-01, int2bytes-len-one, int2bytes-len-one-01,
int2bytes-index-rightshift-02provedall subs proved int2bytes-index-rightshift-01, int2bytes-empty,
int2bytes-fillsgn-recprovedall subs proved bytes2int-first-gez, bytes2int-pos, bytes2int-first-lez, bytes2int-neg, fillsgn-pos, int2int, fillsgn-neg, fillsgn-longer, int2bytes-byte, int2bytes-rec-shift, int2bytes-empty,
no-leading-zero-04provedall subs proved int2bytes-not-neg-01, int2bytes-minus-256-01, int2bytes-byte-neg, int2bytes-byte, int2bytes-minus-one, int2bytes-last-01, int2bytes-rec-neg-256-01, int2bytes-rec-neg-256,
int2bytes-index-rightshift-01provedall subs proved int2bytes-index-rightshift, int2bytes-empty,
int2bytes-len-lsprovedall subs proved int2bytes-len-le,
int2bytes-len-ls-negprovedall subs proved int2bytes-len-le-neg-02,
bytes2bytes-identity-01provedall subs proved bytes2bytes-identity, bytes2bytes-length,
int2bytes-len-ls-neg-02provedall subs proved int2bytes-len-le-neg,
int2bytes-len-ls-03provedall subs proved int2bytes-len-le,
int2bytes-len-eq-negprovedall subs proved int2bytes-empty, int2bytes-len-le-neg-02, int2bytes-len-le-neg,
int2bytes-bytes2int-lengthprovedall subs proved bytes2bytes-identity,
int2bytes-len-one-01provedall subs proved int2bytes-byte-01, int2bytes-byte, int2bytes-empty, int2bytes-last-01, int2bytes-rec-case, int2bytes-len-one,
int2bytes-not-neg-01provedall subs proved int2bytes-not-neg,
int2bytes-len-leprovedall subs proved bytes2int-size-02, int2int, int2bytes-empty, bytes2int-first-lez, bytes2int-size-03,
int2bytes-len-le-negprovedall subs proved bytes2int-size-04, int2int, int2bytes-empty, bytes2int-first-lez, bytes2int-size-06,
int2bytes-len-le-neg-02provedall subs proved bytes2int-size-04, int2int, int2bytes-empty, bytes2int-first-lez, bytes2int-size-06,
int2bytes-index-rightshiftprovedall subs proved bytes2int-i2b, rightshift-8-01, int2bytes-empty,
int2bytes-rec-shiftprovedall subs proved int2bytes-butlast, int2bytes-last-01, int2bytes-empty,
bytes2int-first-gezprovedall subs proved int2int, int2bytes-empty, bytes2int-first-pos, bytes2int-first-lez,
bytes2bytes-identityprovedall subs proved bytes2int-zero-04, no-leading-zero-01, bytes2bytes-zero, bytes2bytes-length, bytes2int-mone, int2bytes-byte-01, bytes2int-one, bytes2bytes-mone, bytes2bytes-other,
rightshift-8-02provedall subs proved fillsgn-longer, int2bytes-byte, int2bytes-byte-neg, int2bytes-minus-256, int2bytes-rec-neg-256, int2bytes-rec-neg-256-01, bytes2int-one, int2bytes-last-01, int2bytes-rec-pos, bytes2int-zero, fillsgn-pos, int2int, fillsgn-neg, int2bytes-empty, rightshift-8,
no-leading-zerosprovedall subs proved int2bytes-leading-zeros, int2bytes-byte, bytes2int-zero, bytes2int-append, bytes2int-zero-02,
intrightshift-8provedall subs proved rightshift-8, int2bytes-empty,
int2bytes-one-02provedall subs proved int2bytes-one,
int2bytes-one-01provedall subs proved int2bytes-one,
int2bytes-len-eq-posprovedall subs proved bytes2int-size-01, int2int, no-leading-zero-01, int2bytes-byte, int2bytes-zero, int2bytes-empty, bytes2int-size,
int2bytes-firstprovedall subs proved bytes2int-first-lez,
int2bytes-leading-zerosprovedall subs proved int2bytes-empty, int2bytes-le127, int2bytes-le255, int2bytes-rec-pos, int2bytes-first-neg-01,
rightshift-8provedall subs proved bytes2int-one, int2bytes-byte, int2int, bytes2int-zero, int2bytes-last-01, int2bytes-rec-case, int2bytes-empty,
int2bytes-butlastprovedall subs proved int2bytes-byte, int2bytes-minus-one, int2bytes-zero, int2bytes-empty, int2bytes-last-01, int2bytes-rec-case,
int2bytes-oneprovedall subs proved int2bytes-empty, int2bytes-last-01, int2bytes-rec-case, int2bytes-byte, int2bytes-le127,
int2bytes-not-negprovedall subs proved int2bytes-empty, int2bytes-last-01, int2bytes-rec-case,
int2bytes-len-oneprovedall subs proved int2bytes-byte-01, int2bytes-empty, int2bytes-last-01, int2bytes-rec-case, int2bytes-byte,
rightshift-8-01provedall subs proved bytes2int-zero, int2bytes-le127, int2bytes-le255, int2bytes-rec-pos, int2bytes-minus-256, int2bytes-rec-neg-256, int2bytes-last-01, bytes2int-one, int2bytes-byte, int2bytes-byte-neg, int2bytes-rec-neg-256-01, int2int, int2bytes-empty,
bytes2int-first-lezprovedall subs proved int2int, int2bytes-empty, bytes2int-first-neq, int2bytes-first-neg,
no-leading-zero-01provedall subs proved int2bytes-zero, int2bytes-rec255-neg, int2bytes-byte, int2bytes-le255, int2bytes-rec-pos,
int2bytes-first-neg-01provedall subs proved int2bytes-empty, int2bytes-byte, int2bytes-rec255-neg,
int2bytes-last-01provedall subs proved int2bytes-le255, int2bytes-le127, int2bytes-byte-neg, int2bytes-byte, int2bytes-rec-case,
int2bytes-zeroprovedall subs proved int2bytes-empty, int2bytes-rec255-neg, int2bytes-le255, int2bytes-rec-pos, int2bytes-byte,
int2bytes-first-negprovedall subs proved int2bytes-byte, int2bytes-rec255-neg, int2bytes-empty,
int2bytes-rec255-negprovedall subs proved int2bytes-empty, int2bytes-len-neg256, fix-two, int2bytes-byte, int2int, fix-neg, fix-longer, int2bytes-rec-neg-06,
int2bytes-rec-caseprovedall subs proved int2bytes-rec-pos, int2bytes-rec-neg-256-01, int2bytes-minus-256, int2bytes-rec-neg-256, int2bytes-byte-neg, int2bytes-le255, int2bytes-byte,
bytes2bytes-fixprovedall subs proved fix-rec-neg, bytes2int-mone, bytes2bytes-mone, fix-length-01, bytes2bytes-length, bytes2bytes-first-neg, int2bytes-empty, fix-rec-pos, bytes2int-zero-04, fix-one, int2bytes-byte-01, bytes2int-one, bytes2bytes-zero, bytes2bytes-other,
fix-butlast-longerprovedall subs proved bytes2int-ge-zero, fillsgn-pos, bytes2int-neg-01, fillsgn-neg, fillsgn-rec, fillsgn-empty, fillsgn-butlast, fix-fillsgn,
bytes2int-int2bytes-len-eqprovedall subs proved int2bytes-le127, int2bytes-rec-neg-256-01, int2bytes-rec-neg-256, int2bytes-minus-256-01, int2bytes-byte-neg, int2bytes-byte, int2bytes-le255, int2bytes-rec-pos, int2bytes-byte-01, bytes2int-one, bytes2int-rec-01,
int2bytes-rec-neg-06provedall subs proved int2bytes-rec-neg-04, int2bytes-byte, int2bytes-rec-neg-05,
bytes2int-neg-01provedall subs proved bytes2int-neg, bytes2int-ge-zero,
int2bytes-rec-neg-256-01provedall subs proved int2bytes-empty, fix2rest-last, int2bytes-rec-neg-02,
fix-rec-negprovedall subs proved fix-neg-le, bytes2int-ge-zero, fix-neg,
int2bytes-rec-neg-03provedall subs proved int2bytes-rec-neg-01, int2bytes-byte, int2bytes-rec-neg-02,
fix-butlastprovedall subs proved fillsgn-butlast, fix-longer, fix-fillsgn,
bytes2int-zero-05provedall subs proved bytes2int-zero-06,
bytes2int-len-one-02provedall subs proved bytes2int-zero-02, bytes2int-zero-03, bytes2int-le-zero, bytes2int-rec-01, bytes2int-zero, bytes2int-rec,
bytes2int-ge-zero-01provedall subs proved bytes2int-ge-zero,
bytes2int-fillsgn-zeroprovedall subs proved fillsgn-longer, bytes2int-zero, fillsgn-pos, bytes2int-zero-06,
int2bytes-rec-neg-05provedall subs proved bits2bytes-mklist-02, fix-bits2bytes-01, bits2bits-inj, bytes2int, fix-neg, bits2bytes-empty, bits2bytes-app, bits2bytes-len-02, bits2bytes-rec-02, bits2bytes-len-01, bits2bytes-base, bits2bytes-rec-01, fix-longer, int2bytes-byte, int2bytes,
int2bytes-rec-neg-02provedall subs proved bits2bytes-rec-02, fix-bits2bytes-01, bits2bits-inj, bytes2int, bits2bytes-len-01, fix-neg, bits2bytes-base, bits2bytes-rec-01, bits2bytes-empty, bits2bytes-len-02, fix-longer, int2bytes-byte, bits2bytes-app, int2bytes,
fillsgn-recprovedall subs proved bytes2int-neg, bytes2int-pos, fillsgn-longer, fillsgn-pos, fillsgn-neg,
fillsgn-butlastprovedall subs proved bytes2int-neg, bytes2int-pos, fillsgn-pos, fillsgn-neg, fillsgn-longer,
bytes2int-le-zeroprovedall subs proved bytes2int-neg,
bytes2int-ge-zeroprovedall subs proved bytes2int-neg,
bytes2int-first-neqprovedall subs proved bytes2int-neg,
bytes2int-zero-06provedall subs proved bytes2int-one, bytes2int-rec-01, bytes2int-zero-03,
fix-rec-posprovedall subs proved fix-pos-le, bytes2int-neg, fix-pos,
no-leading-zeroprovedall subs proved int2bytes-le255, int2bytes-le127, byte2bits, byte2bits-empty, bytes2bits-rec, bytes2int, bytes2int-neg, int2bytes-rec-pos, int2bytes-byte, bytes2int-zero, bytes2int-rec,
bytes2int-size-val-07provedall subs proved bytes2int-1011x,
bytes2int-first-pos-01provedall subs proved bytes2int-first-pos,
bytes2int-mklist-zeros-01provedall subs proved bytes2int-mklist-zeros, bytes2int-rec, bytes2int-one, bytes2int-rec-01,
bytes2int-mklist-mones-01provedall subs proved bytes2int-mklist-mones, bytes2int-rec, bytes2int-one, bytes2int-rec-01,
fix-bits2bytes-01provedall subs proved bits2bytes-mklist-02, bits2bytes-base, bits2bytes-rec-02, bits2bytes-mklist, bits2bytes-app, bits2bytes-fill, bits2bytes-empty, fix-longer, bits2bytes-len-02, bits2bytes-len-01, bits2int-pos, fix-pos, bits2int-neg, fix-neg,
bytes2int-size-07provedall subs proved bytes2int-one, bytes2int-rec-01,
bytes2int-size-05provedall subs proved bytes2int-one, bytes2int-rec-01,
bytes2int-size-06provedall subs proved bytes2int-one, bytes2int-rec-01,
bytes2int-size-04provedall subs proved bytes2int-one, bytes2int-rec-01,
bytes2int-size-03provedall subs proved bytes2int-one, bytes2int-rec-01,
bytes2int-size-02provedall subs proved bytes2int-one, bytes2int-rec-01,
bytes2int-sizeprovedall subs proved bytes2int-zero, bytes2int-rec-01,
bytes2int-size-01provedall subs proved bytes2int-zero, bytes2int-rec-01,
bytes2int-1011xprovedall subs proved bytes2int-rec, bytes2int-one, bytes2int-rec-01,
bytes2int-zero-03provedall subs proved bytes2int-one, bytes2int-rec-01,
int2bytes-rec-neg-256provedall subs proved fix-two, int2bytes-rec-neg-01, int2bytes-byte,
bytes2int-negprovedall subs proved bytes2int-one, bytes2int-rec-01,
bytes2int-first-posprovedall subs proved bytes2int-one, bytes2int-rec-01,
short-2bytes-02provedall subs proved short-2bytes-03,
short-2bytes-01provedall subs proved short-2bytes,
int2int-posprovedall subs proved int2int,
int2int-fillsgnprovedall subs proved int2bytes-empty, fix-value, int2int, fillsgn-longer, fillsgn-fix,
int2bytes-len-ls-04provedall subs proved int2bytes-len-le-01,
getInt-theoremprovedall subs proved bytes2int-one, bytes2int-rec, bytes2int-rec-bor,
fix-bits2bytesprovedall subs proved bits2bytes-mklist-02, bits2bytes-fill, bits2bytes-mklist, bits2bytes-app, bits2bytes-len-02, bits2bytes-len-01, bits2int-pos, fix-pos, bits2int-neg, fix-neg,
bytes2int-size-val-06provedall subs proved bytes2int-011x-02,
bytes2int-size-val-05provedall subs proved bytes2int-100x-03,
bytes2int-size-val-04provedall subs proved bytes2int-100x-02,
bytes2int-size-val-03provedall subs proved bytes2int-100x-01,
bytes2int-size-val-02provedall subs proved bytes2int-011x-01,
bytes2int-size-val-01provedall subs proved bytes2int-100x,
bytes2int-size-valprovedall subs proved bytes2int-011x,
bytes2int-rec-first-zeroprovedall subs proved bytes2int-zero, bytes2int-rec, bytes2int-rec-01,
bytes2int-leading-zeroprovedall subs proved bytes2int-zero, bytes2int-rec-01,
bytes2int-diffprovedall subs proved bytes2int-one, bytes2int-rec-01,
bytes2bytes-first-posprovedall subs proved bytes2bytes-first-neg,
short-2bytes-03provedall subs proved bytes2int-one, bytes2int-rec,
short-2bytesprovedall subs proved bytes2int-one, bytes2int-rec,
int2bytes-len-le-upperprovedall subs proved int2bytes-len-ls-01,
bytes2int-appendprovedall subs proved bytes2bits-nle, bytes2bits-nls, bytes2bits-length, bytes2bits-empty-01, bytes2bits-append, bytes2int,
fix-twoprovedall subs proved bytes2int-zero, fix-pos,
int2bytes-rec-neg-04provedall subs proved bytes2int-zero, fix-pos, bits2bytes-mklist, bits2bytes-app, int2bytes, int2bytes-byte,
int2bytes-rec-neg-01provedall subs proved bytes2int-zero, fix-pos, bits2bytes-mklist, bits2bytes-app, int2bytes, int2bytes-byte,
int2bytes-len-le-01provedall subs proved int2bytes-len-ls-01,
bytes2int-i2bprovedall subs proved bytes2int-one, bytes2int-rec,
bytes2int-rec-borprovedall subs proved bytes2int-rec,
bits2int-negprovedall subs proved bits2int-pos,
bytes2int-011x-02provedall subs proved bytes2int-rec, bytes2int-one,
bytes2int-100x-03provedall subs proved bytes2int-rec, bytes2int-one,
bytes2int-100x-02provedall subs proved bytes2int-rec, bytes2int-one,
bytes2int-100x-01provedall subs proved bytes2int-rec, bytes2int-one,
bytes2int-011x-01provedall subs proved bytes2int-rec, bytes2int-one,
bytes2int-100xprovedall subs proved bytes2int-zero, bytes2int-rec,
bytes2int-011xprovedall subs proved bytes2int-rec, bytes2int-zero,
bytes2int-mklist-zerosprovedall subs proved bytes2int-zero, bytes2int-rec, bytes2bits-empty, bytes2int,
bytes2int-mklist-monesprovedall subs proved bytes2int-rec, bytes2int-one,
int2intprovedall subs proved bits2bits-sgn, bytes2int, int2bytes,
bytes2int-rec-01provedall subs proved bytes2int-rec,
bytes2bytes-lengthprovedall subs proved bytes2int-mone, bytes2int-one, bytes2bytes-mone, bytes2int-zero-04, int2bytes-byte, bytes2int-zero, bytes2bytes-zero, bytes2bytes-other, int2bytes-empty,
bytes2bytes-first-negprovedall subs proved bytes2int-mone, bytes2bytes-mone, bytes2int-zero-04, bytes2bytes-zero, bytes2bytes-other, int2bytes-byte-01, bytes2int-one,
no-leading-zero-02provedall subs proved bytes2bytes-other,
bytes2int-zero-01provedall subs proved bytes2int-zero, bytes2int-rec,
bytes2int-len-one-01provedall subs proved byte2bits, bytes2bits-rec, bytes2bits-empty-01, bytes2int, bytes2int-rec,
bytes2int-2-le-32767provedall subs proved bytes2int-one, bytes2int-rec,
bits2int-2potprovedall subs proved bits2bits-sgn, bytes2int,
band-65535-posprovedall subs proved bytes2int-range,
band-65535-negprovedall subs proved bytes2int-range,
fix-valueprovedall subs proved bytes2bits-mklist-01, bytes2bits-empty-01, bytes2bits-mklist, bytes2bits-append, bytes2int, fix-pos, fix-neg, fix-longer,
int2bytes-len-ls-01provedall subs proved int2bytes-len-adjust, int2bytes-first-zerobyte, int2bytes-byte,
bytes2int-posprovedall subs proved byte2bits-first, byte2bits-empty, bytes2bits-rec, bytes2bits-empty, bytes2bits-empty-01, bytes2int,
bytes2bits-nlsprovedall subs proved bytes2bits-length, bytes2bits-empty-01,
bytes2bits-nleprovedall subs proved bytes2bits-length,
bytes2int-recprovedall subs proved byte2bits-val, byte2bits-value, byte2bits-first, byte2bits-empty, byte2bits-length, bytes2bits-empty-01, bytes2bits-one, bytes2bits-append, bytes2int,
bytes2int-zeroprovedall subs proved bytes2int-one,
bytes2bytes-otherprovedall subs proved byte2bits-empty, byte2bits-value, byte2bits-length, bits2bytes-rec, bits2bytes-base, byte2bits, bytes2bits-empty, bytes2bits-one, bytes2bits-append, bytes2bits-empty-01, int2bytes, bytes2int,
bytes2bytes-moneprovedall subs proved bytes2bits-empty, byte2bits-value, bits2bytes-base, byte2bits-length, bits2bytes-rec, byte2bits-first, byte2bits-empty, byte2bits, bytes2bits-one, bytes2bits-append, bytes2bits-empty-01, int2bytes, bytes2int,
bits2int-posprovedall subs proved bytes2int-one, byte2bits, bytes2bits-rec, bits2bytes-rec-01, bits2bits-inj, bytes2int, bits2bytes-base,
bits2bits-sgnprovedall subs proved byte2bits8, byte2bits-first, byte2bits-empty, bits2bytes-empty, bytes2bits-empty-01, bits2bits-in, bytes2bits-append, byte2bits, bytes2bits-one, bits2bytes-base, bits2bytes-rec,
bytes2int-rangeprovedall subs proved bytes2bits-length, bytes2bits-empty-01, bytes2int,
no-leading-zero-03provedall subs proved bytes2bytes-zero,
int2bytes-rec-pos-anyprovedall subs proved bits2bytes-mklist, bytes2int-one, bits2bytes-rec-02, bits2bits-inj, bytes2bits-empty-01, bits2int-zero-ls, bytes2int, bits2bytes-len-01, fix-neg, fix-pos, bits2bytes-base, bits2bytes-rec-01, bits2bytes-empty, bits2bytes-len-02, fix-longer, bits2bytes-app, int2bytes,
int2bytes-rec-pos-04provedall subs proved bytes2int-one, fix-pos, int2bytes-le127, fix-two-01, int2bytes-le255, int2bytes-rec-pos-03, int2bytes-rec-pos-02,
int2bytes-len-pos-01provedall subs proved int2bytes-len-fits, int2bytes-len-adjust,
int2bytes-len-posprovedall subs proved int2bytes-len-fits, int2bytes-len-adjust,
int2bytes-len-neg-01provedall subs proved int2bytes-len-fits, int2bytes-len-adjust,
int2bytes-len-negprovedall subs proved int2bytes-len-fits, int2bytes-len-adjust,
int2bytes-len-defprovedall subs proved int2bytes-len-adjust, int2bytes-len-fits,
int2bytes-first-zerobyte-01provedall subs proved int2bytes-first-zerobyte,
int2bytes-bytes2int-length-01provedall subs proved bytes2bits-length, bits2bytes-len-02, bits2bytes-len-01, bits2bytes-empty, bytes2bits-empty-01, int2bytes, bytes2int, int2bytes-empty,
fix-two-04provedall subs proved fix-length, fix-empty,
fix-two-03provedall subs proved fix-length, fix-empty,
bytes2bytesprovedall subs proved bytes2bits-empty-01, int2bytes, bytes2int,
fillsgn-not-emptyprovedall subs proved fillsgn-longer, int2bytes-empty, fillsgn-length-02,
int2bytes-len-neg256provedall subs proved bits2bytes-len-02, int2bytes,
int2bytes-rec-pos-02provedall subs proved int2bytes-le127, int2bytes-rec-pos,
int2bytes-rec-pos-03provedall subs proved int2bytes-le255, int2bytes-rec-pos,
int2bytes-len-fitsprovedall subs proved bits2bytes-len-01, int2bytes,
int2bytes-len-adjustprovedall subs proved bits2bytes-len-02, int2bytes,
int2bytes-first-zerobyteprovedall subs proved int2bytes-byte, int2bytes-empty, int2bytes-le255, int2bytes-le127, int2bytes-rec-pos,
bytes2bits-mklistprovedall subs proved byte2bits, bytes2bits-one, bytes2bits-append, bytes2bits-empty,
bytes2bits-mklist-01provedall subs proved byte2bits, bytes2bits-one, bytes2bits-append, bytes2bits-empty,
fix-emptyprovedall subs proved fillsgn-empty, fix-fillsgn, fix-longer,
bits2bytes-fillprovedall subs proved bits2bytes-rec-01, bits2bytes-base, bits2bytes-rec-02,
bytes2int-zero-02provedall subs proved byte2bits, bytes2bits-one, bytes2bits-append, bytes2int,
int2bytes-byte-negprovedall subs proved bits2bytes-base, bits2bytes-true, bits2bytes-rec-01, int2bytes,
int2bytes-minus-256-01provedall subs proved int2bytes-minus-256,
bytes2bytes-zeroprovedall subs proved byte2bits-value, byte2bits-length, bits2bytes-base, bits2bytes-rec, byte2bits, bytes2bits-empty, byte2bits-empty, int2bytes, bytes2bits-one, bytes2bits-append, bytes2int,
bytes2bits-lengthprovedall subs proved byte2bits-length, bytes2bits-one, bytes2bits-append, bytes2bits-empty,
bits2bits-injprovedall subs proved byte2bits8, bytes2bits-one, bytes2bits-append, bits2bytes-rec, bits2bytes-base,
bytes2int-oneprovedall subs proved byte2bits-value, bytes2bits-one, bytes2int,
bits2bits-inprovedall subs proved bytes2bits-append, byte2bits, bytes2bits-one, bits2bytes-base, bits2bytes-rec,
bytes2bits-empty-01provedall subs proved byte2bits-empty, bytes2bits-one, bytes2bits-append, bytes2bits-empty,
int2bytes-rec-pos-01provedall subs proved int2bytes-byte, int2bytes-rec-pos,
bits2bytes-mklist-03provedall subs proved bits2bytes-mklist-02, bits2bytes-base, bits2bytes-rec-01,
bits2int-zero-lsprovedall subs proved byte2bits-first, byte2bits-empty, byte2bits-value, bytes2bits-empty, bytes2bits-rec,
fix2rest-lastprovedall subs proved fix-longer, fix-pos-le, fix-neg-le,
int2bytes-minus-256provedall subs proved bits2bytes-true, bits2bytes-rec, int2bytes,
int2bytes-minus-oneprovedall subs proved bits2bytes-empty, bits2bytes-rec, bits2bytes-base, int2bytes, int2bytes-byte,
fix-fillsgnprovedall subs proved fillsgn-fix,
bits2bytes-len-01provedall subs proved bits2bytes-len,
bits2bytes-len-02provedall subs proved bits2bytes-len,
fillsgn-length-01provedall subs proved fix-length, fillsgn-fix,
fillsgn-length-02provedall subs proved fix-length, fillsgn-length-03, fillsgn-fix,
byte2bits-valprovedall subs proved byte2bits-value, byte2bits, byte2bits-empty, byte2bits-first,
int2bytes-rec-posprovedall subs proved int2bytes-le127, int2bytes-le255, bits2bytes-rec, int2bytes,
int2bytes-byte-01provedall subs proved int2bytes-byte,
bytes2int-zero-04provedall subs proved byte2bits-first, byte2bits-empty, byte2bits-zero, bytes2bits-rec, bytes2int,
bytes2int-moneprovedall subs proved byte2bits-first, byte2bits-empty, byte2bits-mone, bytes2bits-rec, bytes2int,
bits2bytes-rec-01provedall subs proved bits2bytes-empty, bits2bytes-app,
bytes2bits-oneprovedall subs proved bytes2bits-append, bytes2bits-rec,
int2bytes-lastprovedall subs proved int2bytes-le127,
fix-one-01provedall subs proved int2bytes-empty, fix-longer,
fix-lastprovedall subs proved fix-pos-le, fix-neg-le, fix-longer,
bits2bytes-mklist-01provedall subs proved bits2bytes-mklist, bits2bytes-base, bits2bytes-app,
fix-two-01provedall subs proved fix-longer,
bits2bytes-trueprovedall subs proved bits2bytes-base,
fix-neg-leprovedall subs proved fix-neg, fix-longer,
fix-pos-leprovedall subs proved fix-pos, fix-longer,
fillsgn-emptyprovedall subs proved fillsgn-neg, fillsgn-pos, fillsgn-longer,
fillsgn-lengthprovedall subs proved fillsgn-pos, fillsgn-neg, fillsgn-longer,
fillsgn-length-03provedall subs proved fillsgn-longer,
fix-lengthprovedall subs proved fix-pos, fix-neg, fix-longer,
byte2bits-zeroprovedall subs proved byte2bits,
byte2bits-moneprovedall subs proved byte2bits,
int2bytes-le255provedall subs proved bits2bytes-base, bits2bytes-rec, int2bytes,
int2bytes-le127provedall subs proved bits2bytes-base, int2bytes,
int2bytes-byteprovedall subs proved bits2bytes-rec, bits2bytes-base, int2bytes,
fix-oneprovedall subs proved fix-longer,
int2bytes-emptyprovedall subs proved bits2bytes-base, bits2bytes-rec, int2bytes,
fix-length-01provedall subs proved fix-longer,
fillsgn-fixprovedall subs proved fix-neg, fix-pos, fillsgn-pos, fillsgn-neg,
byte2bits-lengthprovedall subs proved byte2bits,
byte2bits-valueprovedall subs proved byte2bits,
bits2bytes-mklist-02provedall subs proved bits2bytes-base, bits2bytes-rec,
bits2bytes-appprovedall subs proved bits2bytes-base, bits2bytes-rec,
bits2bytes-mklistprovedall subs proved bits2bytes-base, bits2bytes-rec,
bits2bytes-lenprovedall subs proved bits2bytes-rec, bits2bytes-base,
bits2bytes-rec-02provedall subs proved bits2bytes-base, bits2bytes-rec,
bits2bytes-emptyprovedall subs proved bits2bytes-rec, bits2bytes-base,
byte2bits-emptyprovedall subs proved byte2bits,
byte2bits-firstprovedall subs proved byte2bits,
byte2bits8provedall subs proved byte2bits,
bytes2bits-appendprovedall subs proved bytes2bits-rec, bytes2bits-empty,
fix-two-02provedall subs proved fix-longer,
bits2bytes-2potprovedall subs proved bits2bytes-rec, bits2bytes-base,
fix-longeraxiom
fix-posaxiom
fix-negaxiom
fillsgn-negaxiom
fillsgn-posaxiom
fillsgn-longeraxiom
int2bytesaxiom
bytes2bits-emptyaxiom
bytes2bits-recaxiom
bytes2intaxiom
bits2bytes-recaxiom
bits2bytes-baseaxiom
byte2bitsaxiom