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: |
|---|
| byte-law-sub | proved | all subs proved
| byte-law-sub-one-01,
byte-law-sub-one,
|
| byte-law-compl | proved | all subs proved
| byte-law-sub-one-01,
i2b-noteq,
|
| byte-law-sub-one | proved | all subs proved
| byte-law-add-one,
|
| byte-law-sub-one-01 | proved | all subs proved
| byte-law-add-one,
byte-law-neg,
|
| fits-law-bxor | proved | all subs proved
| inbyte,
bcompl-bib,
byte2int-in,
band-bib,
inbyte-bib,
bor-bib,
|
| byte-law-add | proved | all subs proved
| byte-law-add-one,
|
| bor-bib | proved | all subs proved
| bib-in-01,
fits-law-bor,
inbyte,
|
| byte-law-neg | proved | all subs proved
| byte,
num-i2b-equal,
bib-pos-low,
bib-upper,
byte-equal,
bib-pos-high,
i2b-equal,
byte-add-256-01,
bib-neg-low,
bib-neg-high,
bib-in-01,
|
| byte-law-add-one | proved | all subs proved
| byte-in,
bib-upper,
byte,
byte-mult,
byte-add-256,
bib-in-01,
bib-lower,
byte-mult-256,
byte-law-add-pos,
|
| band-011x | proved | all subs proved
| byte-011x-pos-02,
|
| byte-add-256-01 | proved | all subs proved
| byte-mult-256-01,
|
| byte-law-add-pos | proved | all subs proved
| byte-add-256,
byte-mult-256,
bib-pos-low,
bib-pos-high,
|
| fits-law-bor | proved | all subs proved
| byte2int-in,
band-bib,
inbyte-bib,
bcompl-bib,
|
| byte-011x-pos-02 | proved | all subs proved
| byte-equal,
byte-011x-pos,
byte-011x-pos-01,
|
| ubyte-pos-02 | proved | all subs proved
| ubyte-pos-01,
ubyte-zero-01,
ubyte-zero,
|
| ubyte-mult | proved | all subs proved
| ubyte-max-01,
ubyte-pos-01,
|
| ubyte-mod | proved | all subs proved
| ubyte-max-02,
ubyte-zero,
|
| issi-ubyte | proved | all subs proved
| ubyte-max-01,
short-max-10,
ubyte-pos-01,
num-issi,
|
| fits-law-bxor-02 | proved | all subs proved
| inshort,
bcompl-sis,
short2int-in,
band-sis,
inshort-sis,
bor-sis,
|
| fits-law-bxor-01 | proved | all subs proved
| inshort,
inshort-byte,
bcompl-sis,
short2int-in,
band-sis,
inshort-sis,
bor-sis,
|
| fits-law-band-01 | proved | all subs proved
| byte-nge,
short-max-01,
byte-size-01,
short-size-01,
short-inrange,
|
| byte-law-mult | proved | all subs proved
| byte-law-mult-one,
|
| byte-and-255 | proved | all subs proved
| byte-equal-01,
ubyte-zero-01,
ubyte-zero,
band-ff,
byte,
|
| byte-011x-ib | proved | all subs proved
| ibi,
byte-add-256,
byte-mod-100x-01,
byte-011x-pos,
|
| ubyte-max-01 | proved | all subs proved
| ubyte-max,
|
| bor-sis | proved | all subs proved
| num-issi,
fits-law-bor-02,
inshort,
|
| bcompl-bib | proved | all subs proved
| bib-in-01,
fits-law-compl,
inbyte,
|
| band-bib | proved | all subs proved
| bib-in-01,
fits-law-band,
inbyte,
|
| byte-size-01 | proved | all subs proved
| byte-size,
|
| byte-law-mult-one | proved | all subs proved
| byte-in,
bib-upper,
num-i2b-equal,
byte,
byte-mult,
bib-in-01,
bib-lower,
byte-mult-256,
|
| ubyte-zero | proved | all subs proved
| ubyte-zero-01,
ubyte-pos-01,
|
| byte-mult-256-01 | proved | all subs proved
| byte-mult-256,
|
| byte-011x-pos-01 | proved | all subs proved
| byte-nls,
byte-011x-neg,
byte-equal,
byte-011x-pos,
|
| byte-add-256 | proved | all subs proved
| byte-mult-256,
|
| ushort-max-07 | proved | all subs proved
| ushort-max-06,
|
| ushort-max-05 | proved | all subs proved
| ushort-max-03,
|
| ubyte-div-lsz | proved | all subs proved
| ubyte-pos-01,
|
| ubyte-band | proved | all subs proved
| ubyte-pos-03,
|
| ubyte-abs | proved | all subs proved
| ubyte-pos-01,
|
| short-overflow | proved | all subs proved
| short-add-max,
short-mod-add-02,
sis-pos-high,
|
| getsetShort-theorem | proved | all subs proved
| bib-pos-high,
bib-pos-low,
bib-ls-same-01,
byte-neq,
byte,
byte-mult,
bib-neg-low,
bib-neg-high,
ubyte-pos,
ubyte-neg,
ubyte-pos-03,
byte-mult-256,
inbyte,
bib-in,
band-ff,
inshort,
|
| byte-011x-unsgn | proved | all subs proved
| bib-upper,
num-ibbi,
byte-011x-neg,
byte-011x-pos,
|
| ushort-max-06 | proved | all subs proved
| ushort-max-04,
|
| ushort-max-03 | proved | all subs proved
| ushort-max-04,
ushort-nlsz,
|
| ubyte-max-02 | proved | all subs proved
| byte-ngr,
ubyte-pos,
ubyte-neg,
|
| ubyte-max | proved | all subs proved
| byte-ngr,
ubyte-neg,
ubyte-pos,
|
| short-mod-add-02 | proved | all subs proved
| short-mod-add-01,
|
| ubyte-pos-01 | proved | all subs proved
| byte-ls-256,
ubyte-neg,
ubyte-pos,
|
| ubyte-pos-03 | proved | all subs proved
| byte-in,
bib-upper,
ubyte-neg,
ubyte-pos,
|
| byte-size | proved | all subs proved
| byte-bitlength-01,
|
| band-ff | proved | all subs proved
| ubyte-neg,
byte-equal,
ubyte-pos,
byte-mod-100x,
byte-011x-neg,
|
| ubyte-zero-01 | proved | all subs proved
| byte-neq,
ubyte-pos,
ubyte-neg,
|
| byte-mult-256 | proved | all subs proved
| byte-in,
num-i2b-neg,
num-i2b-equal,
byte-mult,
bib-upper,
num-ibbi,
bib-lower,
bib-in-01,
byte-mult-neg,
byte-equal,
i2b-equal,
byte-mult-pos,
i2b-noteq,
|
| byte-011x-pos | proved | all subs proved
| byte-equal,
byte-mod-100x,
|
| fits-law-bor-02 | proved | all subs proved
| short2int-in,
band-sis,
inshort-sis,
bcompl-sis,
|
| fits-law-compl | proved | all subs proved
| byte-bitlength-01,
byte-is-cast,
|
| fits-law-band | proved | all subs proved
| byte-bitlength-01,
byte-is-cast,
|
| ushort-max-01 | proved | all subs proved
| short-max-08,
ushort-pos,
ushort-max-04,
ushort-neg,
|
| ubyte-inj | proved | all subs proved
| byte-nle-02,
byte-range,
byte-equal,
ubyte-pos,
ubyte-neg,
|
| shiftright-byte-8-neg-01 | proved | all subs proved
| byte-nle-02,
byte-mod-100x,
|
| shiftright-byte-8-neg | proved | all subs proved
| byte-nle-02,
byte-mod-100x,
|
| fits-law-bor-01 | proved | all subs proved
| inshort-byte,
short2int-in,
band-sis,
inshort-sis,
bcompl-sis,
|
| byte-mult-01 | proved | all subs proved
| byte-mult,
|
| band-011x-01 | proved | all subs proved
| byte-nge,
byte-mod-100x,
|
| ushort-max-04 | proved | all subs proved
| ushort-max,
|
| short-mod-add-01 | proved | all subs proved
| short-mod-add,
|
| bib-ls-same-01 | proved | all subs proved
| bib-pos-low,
bib-pos-high,
bib-neg-low,
bib-neg-high,
|
| band-sis | proved | all subs proved
| num-issi,
fits-law-band-02,
inshort,
|
| byte-bitlength-01 | proved | all subs proved
| byte-len,
|
| byte-mult-neg | proved | all subs proved
| byte-equal,
bib-neg-low,
bib-neg-high,
i2b-equal,
|
| bib-lower | proved | all subs proved
| bib-neg-high,
bib-neg-low,
|
| byte-mult | proved | all subs proved
| byte,
bib-pos-low,
bib-neg-high,
bib-in-01,
i2b-equal,
|
| byte-011x-neg | proved | all subs proved
| byte-mod-100x-01,
|
| ubyte-neg | proved | all subs proved
| byte-len,
unsigned-byte,
|
| byte-mod-100x | proved | all subs proved
| byte-nle,
|
| ushort-short | proved | all subs proved
| short-min-02,
short-nle,
short-ngr,
short-mod,
ushort-pos,
ushort-neg,
ushort-max,
ushort-nlsz,
sis-pos-high,
num-issi,
short-equal,
|
| ushort-plus-01 | proved | all subs proved
| num-issi,
ushort-pos,
ushort-plus,
|
| ushort-max-02 | proved | all subs proved
| ushort-max,
|
| ushort-band-shift-01 | proved | all subs proved
| ushort-max,
ushort-abs,
ushort-nlsz,
ushort-band-shift,
|
| ushort-band-03 | proved | all subs proved
| short-equal,
ushort-pos,
short-mod,
ushort-neg,
short-011x-neg,
|
| short-mult-65536-01 | proved | all subs proved
| short-mult-65536,
|
| short-mod-max | proved | all subs proved
| short-add-max,
short-add-min-01,
short-add-min,
|
| short-div-max-01 | proved | all subs proved
| short-div-ngr,
|
| short-011x-pos | proved | all subs proved
| short-mod,
|
| byte-bitlength | proved | all subs proved
| byte-len,
|
| bib-ls-same | proved | all subs proved
| bib-pos-low,
bib-pos-high,
bib-neg-low,
bib-neg-high,
|
| ushort-plus | proved | all subs proved
| short-add-min-03,
short-add-max-01,
short-add-min-02,
num-issi,
ushort-pos-01,
ushort-pos,
ushort-neg,
|
| ushort-abs | proved | all subs proved
| ushort-nlsz,
|
| ushort-max | proved | all subs proved
| short-max,
ushort-pos,
ushort-neg,
|
| short-mult-65536 | proved | all subs proved
| short-is-cast-01,
|
| short-add-min-01 | proved | all subs proved
| short-add-min,
|
| short-mod-add | proved | all subs proved
| short-add-max,
short-add-min,
|
| short-div-ngr | proved | all subs proved
| short-nle-01,
short-max,
|
| short-mod | proved | all subs proved
| short-max,
short-nle-01,
short-range,
|
| bcompl-sis | proved | all subs proved
| num-issi,
fits-law-compl-01,
inshort,
|
| byte-nle | proved | all subs proved
| byte-nle-02,
byte-le-256,
byte-le,
byte-range,
|
| byte-len | proved | all subs proved
| byte-length,
|
| byte-mod-100x-01 | proved | all subs proved
| byte-nle-01,
|
| bib-neg-high | proved | all subs proved
| bib-bitlength,
byte,
num-i2b-neg,
num-ibbi,
|
| fits-law-band-02 | proved | all subs proved
| short-max-01,
short-size-01,
short-inrange,
|
| ushort-zero-02 | proved | all subs proved
| ushort-pos,
ushort-neg,
ushort-zero-01,
ushort-nlsz,
|
| ushort-zero | proved | all subs proved
| ushort-nlsz,
|
| ushort-inj | proved | all subs proved
| short-nle,
short-range,
short-equal,
ushort-pos,
ushort-neg,
|
| ushort-band-02 | proved | all subs proved
| ushort-nlsz,
ushort-band-01,
|
| ushort-band | proved | all subs proved
| ushort-pos-01,
|
| short-succ-01 | proved | all subs proved
| short-succ,
|
| short-nle-03 | proved | all subs proved
| short-ngr,
short-nle,
|
| short-neq-02 | proved | all subs proved
| short-neq-01,
ushort-pos,
ushort-neg,
ushort-zero-01,
|
| short-law-sub | proved | all subs proved
| short-law-sub-one,
short-law-sub-one-01,
|
| short-law-neg | proved | all subs proved
| short-is-cast,
short-is-cast-01,
|
| short-law-mult | proved | all subs proved
| short-law-mult-one,
|
| short-law-leftshift | proved | all subs proved
| short-is-cast,
short-is-cast-01,
|
| short-law-compl | proved | all subs proved
| short-is-cast-01,
short-is-cast,
|
| short-law-add | proved | all subs proved
| short-law-add-one,
|
| short-larger | proved | all subs proved
| sis-sub-2pot,
sis-pos-low,
sis-pos-high,
short-inj,
|
| short-add-pos-02 | proved | all subs proved
| short-add-pos,
|
| short-add-pos-01 | proved | all subs proved
| short-add-pos,
|
| shiftright-byte-8-pos | proved | all subs proved
| byte-le-256,
|
| fits-law-shr | proved | all subs proved
| fits-law-div-stronger,
byte-nls,
bib-in-01,
num-ibbi,
byte-equal,
ibi,
|
| fits-law-div | proved | all subs proved
| byte-nls-01,
byte-ngr,
inbyte-bib,
short-max-10,
inbyte,
bib-in,
num-issi,
fits-law-div-stronger,
|
| cast-b2i | proved | all subs proved
| cast-b2i-01,
|
| ushort-band-shift | proved | all subs proved
| short-min-02,
ushort-neg,
ushort-pos,
|
| ushort-band-01 | proved | all subs proved
| short-min-02,
ushort-pos,
ushort-neg,
|
| ushort-pos-01 | proved | all subs proved
| sis-pos-high,
short-max-10,
num-issi,
ushort-pos,
ushort-neg,
|
| ushort-nlsz | proved | all subs proved
| short-min-02,
ushort-pos,
ushort-neg,
|
| short-succ | proved | all subs proved
| sis-pos-upper,
short-32767,
short-min-02,
num-issi,
|
| short-nle | proved | all subs proved
| short-min-03,
|
| ushort-zero-01 | proved | all subs proved
| short-neq,
ushort-neg,
ushort-pos,
|
| short-law-sub-one-01 | proved | all subs proved
| short-is-cast,
|
| short-law-sub-one | proved | all subs proved
| short-is-cast,
|
| short-law-mult-one | proved | all subs proved
| short-is-cast,
|
| short-is-cast-01 | proved | all subs proved
| short-is-cast,
short-inj,
|
| short-law-add-one | proved | all subs proved
| short-is-cast,
|
| sis-sub-2pot | proved | all subs proved
| sis-neg-high,
sis-neg-lower,
sis-pos-upper,
num-issi,
|
| short-max | proved | all subs proved
| short-max-07,
|
| short-nle-01 | proved | all subs proved
| short-nle-02,
|
| short-add-pos | proved | all subs proved
| short-add-min-02,
num-issi,
|
| short-add-min | proved | all subs proved
| short-min-01,
short-min-03,
|
| fits-law-div-stronger | proved | all subs proved
| byte-gr-127,
bib-pos-high,
byte-min,
byte-ngr-01,
bib-in-01,
|
| inshort-byte | proved | all subs proved
| byte-equal,
short-byte,
inshort-sis,
|
| short-size-01 | proved | all subs proved
| short-size,
|
| cast-b2i-01 | proved | all subs proved
| byte-nls-02,
byte-nge,
|
| byte-le-256 | proved | all subs proved
| byte-nge,
|
| byte-nle-01 | proved | all subs proved
| byte-nle-02,
byte-nge,
byte-le,
byte-range,
|
| byte-length | proved | all subs proved
| byte-nge,
byte-nls,
byte-le,
byte-range,
|
| bib-bitlength | proved | all subs proved
| byte-is-cast,
|
| fits-law-compl-01 | proved | all subs proved
| short-size-02,
short-is-cast,
|
| ushort-pos-02 | proved | all subs proved
| sis-neg-low,
sis-neg-high,
num-issi,
ushort-pos,
ushort-neg,
|
| sis-ls-same-01 | proved | all subs proved
| num-issi,
sis-neg-low,
sis-neg-high,
short-max-07,
|
| sis-bitlength | proved | all subs proved
| short-is-cast,
|
| short-shift-pos | proved | all subs proved
| short-max-07,
short-min-02,
short-inrange,
|
| short-nls-01 | proved | all subs proved
| short-ngr,
short-min-02,
|
| short-mod-ngr | proved | all subs proved
| short-min-02,
short-max-06,
|
| short-max-11 | proved | all subs proved
| short-min-01,
short-max-06,
short-neq-01,
short-max-01,
|
| short-law-xor-one | proved | all subs proved
| short-is-cast,
|
| short-law-shift-snd-rz | proved | all subs proved
| short-is-cast,
|
| short-law-shift-snd-r | proved | all subs proved
| short-is-cast,
|
| short-law-shift-snd-l | proved | all subs proved
| short-is-cast,
|
| short-law-or-one | proved | all subs proved
| short-is-cast,
|
| short-law-and-one | proved | all subs proved
| short-is-cast,
|
| shiftright-byte-8-pos-01 | proved | all subs proved
| byte-nge,
|
| long-automatic-03 | proved | all subs proved
| num-i2l-pos,
|
| long-automatic-02 | proved | all subs proved
| num-i2l-pos,
|
| long-automatic-01 | proved | all subs proved
| num-i2l-neg,
|
| long-automatic | proved | all subs proved
| long-eq,
|
| inshort-neg | proved | all subs proved
| short-ls,
inshort-le-num,
inshort,
|
| fits-law-sub | proved | all subs proved
| byte-equal,
byte-nge,
byte-nls-01,
byte-ngr,
short-inrange,
|
| fits-law-neg | proved | all subs proved
| byte-ngr,
byte-nle-02,
short-is-cast,
|
| fits-law-mul | proved | all subs proved
| byte-nle-02,
byte-min,
byte-nge,
byte-ls-256,
byte-ngr,
short-inrange,
|
| fits-law-mod-01 | proved | all subs proved
| short-min-01,
short-min-02,
short-max-06,
short-max-10,
num-issi,
|
| fits-law-mod | proved | all subs proved
| byte-ngr-01,
byte-nls-01,
byte-ngr,
byte-nls,
num-ibbi,
|
| fits-law-add | proved | all subs proved
| byte-le,
byte-nge,
byte-nls,
byte-nls-01,
short-inrange,
|
| div-inshort | proved | all subs proved
| short-min-03,
inshort-le-num,
short-ls,
short-ngr,
short-max-06,
short-min-01,
inshort,
|
| byte-sis | proved | all subs proved
| byte-is-cast-01,
short-is-cast,
|
| byte-short-neq | proved | all subs proved
| short-is-cast,
short-inj,
byte-is-cast-01,
|
| byte-law-leftshift | proved | all subs proved
| byte-is-cast,
byte-is-cast-01,
|
| byte-law-div-not | proved | all subs proved
| byte-unsigned,
bib-pos-high,
bib-upper,
num-i2b-equal,
bib-pos-low,
|
| bint-short | proved | all subs proved
| short-max-07,
short-min-02,
bint-num-in,
|
| bint-byte | proved | all subs proved
| byte-nge,
byte-nls-01,
bint-num-in,
|
| short-neq | proved | all subs proved
| short-min-01,
|
| short-add-min-03 | proved | all subs proved
| short-min-01,
|
| sis-neg-lower | proved | all subs proved
| sis-neg-high,
sis-neg-low,
|
| short-size | proved | all subs proved
| short-max-01,
short-min-01,
|
| short-nle-02 | proved | all subs proved
| short-min-01,
|
| ushort-neg | proved | all subs proved
| short-min-01,
unsigned-short,
|
| short-add-max | proved | all subs proved
| short-max-01,
|
| short-neq-01 | proved | all subs proved
| short-min-01,
short-max-01,
|
| short-add-min-02 | proved | all subs proved
| short-min-01,
|
| num-i2l-pos | proved | all subs proved
| long-is-cast-01,
|
| num-i2l-neg | proved | all subs proved
| long-is-cast-01,
|
| long-eq | proved | all subs proved
| long-is-cast,
long-eq-01,
long-is-cast-01,
|
| short-byte | proved | all subs proved
| byte-ngr,
byte-nls-01,
num-issi,
|
| byte-ls-256 | proved | all subs proved
| byte-nls-01,
|
| byte-ngr-01 | proved | all subs proved
| byte-nls,
byte-ngr,
|
| short-size-02 | proved | all subs proved
| short-max-01,
short-min-01,
|
| inshort-sis | proved | all subs proved
| short-min-01,
short-max-10,
num-issi,
inshort,
|
| short-ls | proved | all subs proved
| short-min-01,
|
| short-min-03 | proved | all subs proved
| short-min-01,
|
| byte-nls-02 | proved | all subs proved
| byte-nls,
byte-le,
byte-range,
|
| short-is-cast | proved | all subs proved
| sis-on-bits,
|
| byte-is-cast-01 | proved | all subs proved
| bib-on-bits,
i2b-equal,
|
| byte-unsigned | proved | all subs proved
| bib-upper,
num-ibbi,
byte-equal,
|
| short-min-02 | proved | all subs proved
| short-min-01,
|
| short-max-07 | proved | all subs proved
| short-max-01,
|
| byte-is-cast | proved | all subs proved
| bib-on-bits,
|
| byte-nge | proved | all subs proved
| byte-ngr,
|
| sis-ls-same | proved | all subs proved
| sis-pos-low,
sis-pos-high,
sis-neg-low,
sis-neg-high,
|
| short-succ-pos | proved | all subs proved
| inshort-01,
sis-in,
|
| short-nls | proved | all subs proved
| short-max-01,
|
| short-mod-01 | proved | all subs proved
| short-ngr,
short-max-10,
short-min-01,
num-issi,
|
| short-max-05 | proved | all subs proved
| short-max-04,
|
| short-law-ls-not | proved | all subs proved
| sis-01,
sis-pos-upper,
num-issi,
|
| short-law-div-not | proved | all subs proved
| sis-pos-high,
num-issi,
short-zero,
sis-pos-upper,
notequal-01,
sis-pos-low,
|
| short-in | proved | all subs proved
| sis-pos-high,
sis-pos-low,
|
| short-div256 | proved | all subs proved
| short-max-01,
|
| out-test-01 | proved | all subs proved
| bib-upper,
|
| mod-inshort | proved | all subs proved
| short-ngr,
short-min-01,
inshort,
|
| long-shzr | proved | all subs proved
| long-shiftzero-in,
lib-in,
|
| fits-law-shr-01 | proved | all subs proved
| short-min-01,
short-ngr,
short-max-10,
num-issi,
|
| byte-succ | proved | all subs proved
| byte-127,
byte-in,
|
| byte-law-ls-not | proved | all subs proved
| bib-upper,
num-ibbi,
|
| byte-law-and-one | proved | all subs proved
| bib-on-bits,
byte-equal,
i2b-equal,
i2b-noteq,
|
| short-max-08 | proved | all subs proved
| short-max-10,
|
| sis-neg-high | proved | all subs proved
| sis-06,
num-i2s-neg,
num-issi,
|
| sis-neg-low | proved | all subs proved
| sis-pos-high,
num-i2s-neg,
num-issi,
|
| inshort-01 | proved | all subs proved
| short-ngr,
short-32767,
inshort,
|
| short-max-04 | proved | all subs proved
| short-max-06,
|
| sis-pos-upper | proved | all subs proved
| sis-pos-high,
|
| short-zero | proved | all subs proved
| isi,
sis-06,
|
| sis-on-bits | proved | all subs proved
| short-max-10,
num-issi,
inshort,
sis-in,
int2short-out,
|
| sis-pos-low | proved | all subs proved
| sis-06,
num-i2s-pos,
num-issi,
|
| long-shiftzero-in | proved | all subs proved
| long2int-in,
long-min,
inlong,
|
| long-is-cast-01 | proved | all subs proved
| long-is-cast,
ili,
|
| byte-neq | proved | all subs proved
| byte-nls,
|
| byte-min | proved | all subs proved
| byte-nls,
|
| inbyte-bib | proved | all subs proved
| byte-gr-127,
byte-nls,
bib-in-01,
inbyte,
|
| short-max-01 | proved | all subs proved
| short-range,
|
| short-min-01 | proved | all subs proved
| short-range,
|
| inshort-le-num | proved | all subs proved
| short-max-06,
|
| byte-127 | proved | all subs proved
| byte-gr-127,
|
| byte-nle-02 | proved | all subs proved
| byte-nls,
|
| byte-ngr | proved | all subs proved
| byte-gr-127,
|
| byte-mult-pos | proved | all subs proved
| byte-equal,
bib-pos-low,
bib-pos-high,
i2b-equal,
|
| byte-le | proved | all subs proved
| byte-gr-127,
|
| num-i2b-equal | proved | all subs proved
| bib-in-01,
byte-equal,
|
| bib-on-bits | proved | all subs proved
| bib-in-01,
inbyte,
bib-in,
int2byte-out,
|
| bib-upper | proved | all subs proved
| bib-pos-high,
|
| byte-nls-01 | proved | all subs proved
| byte-nls,
|
| sis-03 | proved | all subs proved
| short-max-10,
inshort,
sis-in,
|
| short-sub-pos | proved | all subs proved
| short-max-03,
num-issi,
|
| short-not-max | proved | all subs proved
| short-32767,
|
| short-max-09 | proved | all subs proved
| short-max-10,
|
| short-max-02 | proved | all subs proved
| short-max-03,
|
| short-law-righthift-not | proved | all subs proved
| num-i2s-pos,
notequal-01,
sis-pos-high,
|
| s2i-switch | proved | all subs proved
| short-inrange,
isi,
|
| out-test-08 | proved | all subs proved
| bib-pos-low,
|
| out-test-07 | proved | all subs proved
| bib-pos-high,
|
| out-test-06 | proved | all subs proved
| byte,
num-i2b-neg,
|
| longin-mult-mod-01 | proved | all subs proved
| longin-mult-mod,
inbint,
|
| long-on-bits | proved | all subs proved
| long-is-cast,
|
| long-mod-pos-low | proved | all subs proved
| long-is-cast,
|
| long-mod-pos-high | proved | all subs proved
| long-is-cast,
|
| long-mod-neg-low | proved | all subs proved
| long-is-cast,
|
| long-mod-neg-high | proved | all subs proved
| long-is-cast,
|
| lil-carry | proved | all subs proved
| long-band-add,
num-illi,
|
| l2i-bint | proved | all subs proved
| lil-num,
inbint,
|
| getShort-isi | proved | all subs proved
| byte-gr-127,
byte-range,
byte-and-lsz,
byte-and-le-256,
num-issi,
|
| byte-ls-127 | proved | all subs proved
| byte-nls,
|
| byte-law-righthift-not | proved | all subs proved
| num-i2b-pos,
notequal,
bib-pos-high,
|
| bint-unsigned | proved | all subs proved
| bint-unsigned-01,
bint-equal,
|
| bint-succ-notin | proved | all subs proved
| bint-unsigned-01,
inbint,
|
| bint-pred-02 | proved | all subs proved
| bint-num-in,
inbint,
|
| bint-pred | proved | all subs proved
| bint-num-in,
inbint,
|
| bint-div2-01 | proved | all subs proved
| bint-div2,
biibi-in,
|
| bint-band-one-01 | proved | all subs proved
| bint-band-one,
biibi-in,
|
| bint-2pot31 | proved | all subs proved
| bint-unsigned-01,
|
| short-add-max-01 | proved | all subs proved
| short-ngr,
|
| short-011x-neg | proved | all subs proved
| short-min,
|
| sis-06 | proved | all subs proved
| num-issi,
sis-in,
|
| short-max-03 | proved | all subs proved
| short-ngr,
|
| short-range | proved | all subs proved
| short-min,
short-ngr,
|
| sis-01 | proved | all subs proved
| num-issi,
sis-in,
|
| notequal-01 | proved | all subs proved
| isi,
num-issi,
|
| sis-pos-high | proved | all subs proved
| num-i2s-pos,
num-issi,
|
| longin-mult-mod | proved | all subs proved
| longin-mult-01,
longin-mod,
|
| long-min | proved | all subs proved
| long-min-01,
|
| long-is-cast | proved | all subs proved
| num-illi,
inlong,
lib-in,
int2long-out,
|
| long-band-add | proved | all subs proved
| num-illi,
|
| lil-num | proved | all subs proved
| num-illi,
|
| short-32767 | proved | all subs proved
| short-ngr,
|
| short-max-10 | proved | all subs proved
| short-ngr,
|
| short-inrange | proved | all subs proved
| num-issi,
|
| short-max-06 | proved | all subs proved
| short-ngr,
|
| short-inj | proved | all subs proved
| short-equal,
|
| notequal | proved | all subs proved
| ibi,
byte-equal,
num-ibbi,
|
| byte-in | proved | all subs proved
| num-ibbi,
|
| i2b-equal | proved | all subs proved
| byte-equal,
|
| byte-gr-127 | proved | all subs proved
| byte-range,
|
| byte-nls | proved | all subs proved
| byte-range,
|
| bint-div2 | proved | all subs proved
| bint-num-02,
bint-num-04,
inbint,
|
| bint-num-in | proved | all subs proved
| bint-is-cast,
|
| bint-band-one | proved | all subs proved
| bint-num-02,
bint-num-04,
|
| bint-unsigned-01 | proved | all subs proved
| bint-is-cast,
|
| byte | proved | all subs proved
| num-ibbi,
|
| bib-pos-high | proved | all subs proved
| num-i2b-pos,
num-ibbi,
|
| bib-pos-low | proved | all subs proved
| num-i2b-pos,
num-ibbi,
|
| bib-neg-low | proved | all subs proved
| num-i2b-pos,
num-i2b-neg,
num-ibbi,
|
| ubyte-pos | proved | all subs proved
| byte-equal,
unsigned-byte,
|
| bib-in-01 | proved | all subs proved
| num-ibbi,
|
| sis-05 | proved | all subs proved
| num-issi,
|
| short-ge | proved | all subs proved
| short-ngr,
|
| short-div-max | proved | all subs proved
| short-ngr,
|
| short-add2 | proved | all subs proved
| short-ngr,
|
| s144 | proved | all subs proved
| num-issi,
|
| out-test-05 | proved | all subs proved
| num-ibbi,
num-i2b-neg,
|
| out-test-04 | proved | all subs proved
| num-ibbi,
|
| out-test-03 | proved | all subs proved
| num-ibbi,
|
| out-test-02 | proved | all subs proved
| num-ibbi,
num-i2b-neg,
|
| mtwo | proved | all subs proved
| num-ibbi,
|
| mthree-01 | proved | all subs proved
| num-ibbi,
|
| mthree | proved | all subs proved
| num-ibbi,
|
| minus-two | proved | all subs proved
| num-issi,
|
| minus-three-01 | proved | all subs proved
| num-issi,
|
| minus-three | proved | all subs proved
| num-issi,
|
| minus-four-02 | proved | all subs proved
| num-ibbi,
|
| minus-four-01 | proved | all subs proved
| num-ibbi,
|
| minus-four | proved | all subs proved
| num-issi,
|
| minus-five-01 | proved | all subs proved
| num-ibbi,
|
| minus-five | proved | all subs proved
| num-ibbi,
|
| mfive | proved | all subs proved
| num-issi,
|
| longin-mult | proved | all subs proved
| longin-mult-01,
inbint,
|
| long-band-11x | proved | all subs proved
| num-illi,
|
| byte-04 | proved | all subs proved
| num-ibbi,
|
| byte-03 | proved | all subs proved
| num-ibbi,
|
| byte-02 | proved | all subs proved
| num-ibbi,
|
| byte-01 | proved | all subs proved
| num-ibbi,
|
| bint-trans-pos-04 | proved | all subs proved
| bint-trans-pos,
|
| bint-mult2 | proved | all subs proved
| bint-trans-pos,
biibi-in,
|
| bint-is-cast-01 | proved | all subs proved
| bint-is-cast,
ibii,
|
| bint-band-zero | proved | all subs proved
| bint-band-011x-neg,
bint-band-011x,
inbint,
|
| bint-and-011x-bits2unit | proved | all subs proved
| bint-fillsgn-len,
bint-band-011x,
inbint,
|
| bib-64 | proved | all subs proved
| num-ibbi,
|
| b2i-i2b-same | proved | all subs proved
| ibi,
byte-equal-01,
|
| num-i2s-neg | proved | all subs proved
| inshort,
int2short-out,
|
| ushort-pos | proved | all subs proved
| unsigned-short,
|
| num-i2s-pos | proved | all subs proved
| inshort,
int2short-out,
|
| short-equal | proved | all subs proved
| isi,
|
| short-min | proved | all subs proved
| inshort,
short2int-in,
|
| longin-mod | proved | all subs proved
| inlong,
|
| longin-mult-01 | proved | all subs proved
| inlong,
inbint,
|
| long-min-01 | proved | all subs proved
| inlong,
long2int-in,
|
| num-illi | proved | all subs proved
| inlong,
lib-in,
|
| short-ngr | proved | all subs proved
| inshort,
short2int-in,
|
| byte-range | proved | all subs proved
| byte2int-in,
inbyte,
|
| bint-equal | proved | all subs proved
| ibii,
|
| bint-trans-pos | proved | all subs proved
| inbint,
|
| bint-is-cast | proved | all subs proved
| inbint,
biibi-in,
int2bint-out,
|
| bint-band-011x-neg | proved | all subs proved
| inbint,
|
| bint-num-04 | proved | all subs proved
| inbint,
|
| bint-num-02 | proved | all subs proved
| inbint,
|
| bint-band-011x | proved | all subs proved
| inbint,
|
| bint-fillsgn-len | proved | all subs proved
| inbint,
|
| num-i2b-pos | proved | all subs proved
| inbyte,
int2byte-out,
|
| num-i2b-neg | proved | all subs proved
| inbyte,
int2byte-out,
|
| num-ibbi | proved | all subs proved
| inbyte,
bib-in,
|
| num-issi | proved | all subs proved
| inshort,
sis-in,
|
| byte-equal | proved | all subs proved
| ibi,
|
| byte-equal-01 | proved | all subs proved
| ibi,
|
| num-i2bi-pos | proved | all subs proved
| inbint,
int2bint-out,
|
| num-i2bi-neg | proved | all subs proved
| inbint,
int2bint-out,
|
| inshort-num | proved | all subs proved
| inshort,
|
| inshort-mult | proved | all subs proved
| inshort,
|
| bint-trans-pos-03 | proved | all subs proved
| inbint,
|
| bint-trans-pos-02 | proved | all subs proved
| inbint,
|
| bint-trans-pos-01 | proved | all subs proved
| inbint,
|
| bint-pred-01 | proved | all subs proved
| inbint,
|
| bint-num-03 | proved | all subs proved
| inbint,
|
| bint-num-01 | proved | all subs proved
| inbint,
|
| bint-num | proved | all subs proved
| inbint,
|
| bint-mod | proved | all subs proved
| inbint,
|
| bint-carry-01 | proved | all subs proved
| inbint,
|
| bint-carry | proved | all subs proved
| inbint,
|
| unsigned-short | axiom | | |
| unsigned-byte | axiom | | |
| sis-in | axiom | | |
| int2short-out | axiom | | |
| isi | axiom | | |
| long2int-in | axiom | | |
| ili | axiom | | |
| int2long-out | axiom | | |
| lib-in | axiom | | |
| inlong | axiom | | |
| long-eq-01 | proved | all subs proved
| |
| byte-and-le-256 | proved | all subs proved
| |
| byte-and-lsz | proved | all subs proved
| |
| short2int-in | axiom | | |
| byte2int-in | axiom | | |
| i2b-noteq | proved | all subs proved
| |
| int2bint-out | axiom | | |
| ibii | axiom | | |
| biibi-in | axiom | | |
| inbint | axiom | | |
| int2byte-out | axiom | | |
| bib-in | axiom | | |
| inshort | axiom | | |
| inbyte | axiom | | |
| ibi | axiom | | |