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

Theorem base summary for Specification byte

Byte-and-range(1,0)bint-num(2,0)byte-in(2,1)byte-not-max(12,7)inbint(0,0)longin-mult(2,1)shiftright-byte-8-pos(4,2)short-law-sub(2,2)short-range(2,1)ubyte-pos-03(5,3)
b2i-i2b-same(1,1)bint-num-01(2,0)byte-is-cast(2,2)byte-range(2,1)inbyte(0,0)longin-mult-01(27,17)shiftright-byte-8-pos-01(9,5)short-law-sub-one(4,4)short-shift-pos(3,2)ubyte-zero(1,0)
band-011x(1,1)bint-num-02(2,0)byte-is-cast-01(6,5)byte-short-neq(12,10)inbyte-bib(4,2)longin-mult-mod(2,1)short-011x-neg(8,5)short-law-sub-one-01(4,4)short-size(12,7)ubyte-zero-01(4,2)
band-011x-01(2,1)bint-num-03(2,0)byte-law-add(4,3)byte-sis(4,4)inlong(0,0)longin-mult-mod-01(2,1)short-011x-pos(1,0)short-law-xor-one(4,4)short-size-01(3,2)unsigned-byte(0,0)
band-bib(2,1)bint-num-04(2,0)byte-law-add-one(19,10)byte-size(8,5)inshort(0,0)mfive(1,0)short-32767(3,2)short-ls(1,1)short-size-02(8,4)unsigned-short(0,0)
band-ff(1,1)bint-num-in(3,2)byte-law-add-pos(8,3)byte-size-01(5,4)inshort-01(2,1)minus-five(1,0)short-add-max(2,1)short-mask(1,1)short-sub-pos(2,1)ushort-abs(1,0)
band-sis(5,3)bint-pred(4,1)byte-law-and-one(190,111)byte-succ(3,1)inshort-byte(1,1)minus-five-01(1,0)short-add-max-01(4,3)short-max(1,0)short-succ(2,1)ushort-band(5,3)
bcompl-bib(2,1)bint-pred-01(4,1)byte-law-compl(4,3)byte-unsigned(4,3)inshort-le-num(2,0)minus-four(1,0)short-add-min(6,5)short-max-01(2,1)short-succ-01(2,1)ushort-band-01(33,21)
bcompl-sis(3,2)bint-pred-02(4,1)byte-law-div-not(2,1)byte2bint(0,0)inshort-mult(1,0)minus-four-01(1,0)short-add-min-01(2,2)short-max-02(2,1)short-succ-pos(2,1)ushort-band-02(2,2)
bib-64(1,0)bint-short(1,1)byte-law-leftshift(8,4)byte2int-in(0,0)inshort-neg(2,1)minus-four-02(1,0)short-add-min-02(4,3)short-max-03(2,1)short-zero(2,1)ushort-band-03(1,1)
bib-bitlength(3,2)bint-succ-notin(4,2)byte-law-ls-not(1,0)byte2short(0,0)inshort-num(2,0)minus-three(1,0)short-add-min-03(4,3)short-max-04(3,2)short2bint(0,0)ushort-band-shift(83,54)
bib-in(0,0)bint-trans-pos(1,0)byte-law-mult(3,3)cast-b2i(1,1)inshort-sis(4,2)minus-three-01(1,0)short-add-pos(2,1)short-max-05(2,1)short2byte(0,0)ushort-band-shift-01(6,4)
bib-in-01(1,1)bint-trans-pos-01(1,0)byte-law-mult-one(29,19)cast-b2i-01(20,11)int2bint-out(0,0)minus-two(1,0)short-add-pos-01(2,1)short-max-06(1,0)short2int-in(0,0)ushort-inj(15,7)
bib-lower(6,3)bint-trans-pos-02(2,1)byte-law-neg(37,24)div-inshort(42,24)int2byte-out(0,0)mod-inshort(14,8)short-add-pos-02(2,1)short-max-07(1,0)shortOverflow(0,0)ushort-max(2,1)
bib-ls-same(11,6)bint-trans-pos-03(2,1)byte-law-righthift-not(101,42)ex256(1,0)int2long-out(0,0)mthree(1,0)short-add2(3,2)short-max-08(1,0)sis-01(1,1)ushort-max-01(1,1)
bib-ls-same-01(18,9)bint-trans-pos-04(1,0)byte-law-sub(3,2)fits-law-add(9,6)int2short-out(0,0)mthree-01(1,0)short-byte(1,1)short-max-09(1,0)sis-03(4,2)ushort-max-02(7,5)
bib-neg-high(55,32)bint-unsigned(5,3)byte-law-sub-one(3,3)fits-law-band(9,5)isi(0,0)mtwo(1,0)short-div-max(2,1)short-max-10(1,0)sis-05(2,1)ushort-max-03(6,5)
bib-neg-low(42,25)bint-unsigned-01(3,2)byte-law-sub-one-01(5,5)fits-law-band-01(14,7)issi-ubyte(3,2)notequal(5,3)short-div-max-01(2,1)short-max-11(11,8)sis-06(1,1)ushort-max-04(3,2)
bib-on-bits(36,19)bint2int-in(0,0)byte-le(1,0)fits-law-band-02(15,7)l2i-bint(2,1)notequal-01(5,3)short-div-ngr(9,6)short-min(3,2)sis-bitlength(3,2)ushort-max-05(5,4)
bib-pos-high(42,24)bor-bib(2,1)byte-le-256(1,0)fits-law-bor(11,8)lib-in(0,0)num-i2b-equal(3,1)short-div256(3,2)short-min-01(2,1)sis-in(0,0)ushort-max-06(1,0)
bib-pos-low(21,10)bor-sis(5,3)byte-len(2,1)fits-law-bor-01(12,8)lil-carry(13,7)num-i2b-neg(3,1)short-equal(4,4)short-min-02(1,0)sis-ls-same(11,6)ushort-max-07(1,0)
bib-upper(2,1)byte(1,0)byte-length(4,2)fits-law-bor-02(11,8)lil-num(2,1)num-i2b-pos(3,1)short-ge(1,0)short-min-03(1,0)sis-ls-same-01(12,6)ushort-neg(10,5)
biibi-in(0,0)byte-01(1,0)byte-ls-127(1,1)fits-law-bxor(14,10)long-automatic(71,3)num-i2bi-neg(2,1)short-in(6,3)short-mod(5,3)sis-neg-high(38,23)ushort-nlsz(2,1)
bint-2pot31(1,1)byte-011x-ib(1,1)byte-ls-256(1,0)fits-law-bxor-01(14,10)long-automatic-01(3,2)num-i2bi-pos(3,1)short-inj(1,1)short-mod-01(8,4)sis-neg-low(31,18)ushort-plus(21,11)
bint-and-011x-bits2unit(13,7)byte-011x-neg(1,0)byte-min(1,0)fits-law-bxor-02(14,10)long-automatic-02(5,3)num-i2l-neg(6,3)short-inrange(2,1)short-mod-add(4,2)sis-neg-lower(6,3)ushort-plus-01(7,4)
bint-band-011x(7,5)byte-011x-pos(1,0)byte-mod-100x(1,1)fits-law-compl(5,4)long-automatic-03(3,2)num-i2l-pos(6,3)short-is-cast(2,2)short-mod-add-01(5,3)sis-on-bits(35,19)ushort-pos(2,1)
bint-band-011x-neg(7,5)byte-011x-pos-01(2,1)byte-mod-100x-01(1,1)fits-law-compl-01(5,3)long-band-11x(1,1)num-i2s-neg(2,1)short-is-cast-01(3,3)short-mod-add-02(2,1)sis-pos-high(33,21)ushort-pos-01(10,5)
bint-band-and-nlsz(2,1)byte-011x-pos-02(2,0)byte-mult(5,4)fits-law-div(11,6)long-band-add(8,5)num-i2s-pos(3,1)short-larger(15,4)short-mod-max(3,2)sis-pos-low(24,14)ushort-pos-02(16,8)
bint-band-one(1,1)byte-011x-unsgn(5,3)byte-mult-01(3,2)fits-law-div-stronger(20,13)long-eq(7,6)num-ibbi(3,1)short-law-add(3,3)short-mod-ngr(5,3)sis-pos-upper(2,1)ushort-short(11,8)
bint-band-one-01(1,1)byte-02(1,0)byte-mult-256(71,44)fits-law-mod(12,6)long-eq-01(1,0)num-illi(4,2)short-law-add-one(4,4)short-mult-65536(5,5)sis-sub-2pot(10,4)ushort-zero(2,1)
bint-band-zero(4,2)byte-03(1,0)byte-mult-256-01(3,3)fits-law-mod-01(12,6)long-is-cast(21,11)num-issi(3,1)short-law-and-one(4,4)short-mult-65536-01(1,1)ubyte-abs(1,0)ushort-zero-01(4,2)
bint-byte(1,1)byte-04(1,0)byte-mult-neg(12,7)fits-law-mul(25,17)long-is-cast-01(5,5)out-test-01(1,0)short-law-compl(9,6)short-neq(2,1)ubyte-band(1,1)ushort-zero-02(2,1)
bint-carry(2,1)byte-127(3,2)byte-mult-pos(4,3)fits-law-neg(11,6)long-min(1,0)out-test-02(1,0)short-law-div-not(1,0)short-neq-01(17,11)ubyte-div-lsz(2,1)zero-bint(0,0)
bint-carry-01(7,4)byte-add-256(3,3)byte-neq(2,0)fits-law-shr(28,17)long-min-01(3,2)out-test-03(1,0)short-law-leftshift(4,4)short-neq-02(8,5)ubyte-inj(11,7)zero-byte(0,0)
bint-div2(2,1)byte-add-256-01(4,3)byte-nge(3,1)fits-law-shr-01(15,9)long-mod-neg-high(4,2)out-test-04(1,0)short-law-ls-not(1,0)short-ngr(3,2)ubyte-max(2,1)zero-long(0,0)
bint-div2-01(2,1)byte-and-255(2,1)byte-ngr(2,0)fits-law-sub(8,4)long-mod-neg-low(4,2)out-test-05(1,0)short-law-mult(3,3)short-nle(3,2)ubyte-max-01(3,2)zero-short(0,0)
bint-eq(1,0)byte-and-le-256(1,0)byte-ngr-01(2,1)getShort-isi(37,23)long-mod-pos-high(4,2)out-test-06(1,0)short-law-mult-one(4,4)short-nle-01(2,1)ubyte-max-02(2,1)
bint-equal(1,0)byte-and-lsz(1,0)byte-nle(4,2)getsetShort-theorem(68,35)long-mod-pos-low(4,2)out-test-07(1,0)short-law-neg(5,4)short-nle-02(1,0)ubyte-mod(2,1)
bint-fillsgn-len(8,4)byte-bitlength(1,0)byte-nle-01(4,2)i2b-equal(1,0)long-on-bits(3,2)out-test-08(1,0)short-law-or-one(4,4)short-nle-03(3,2)ubyte-mult(5,4)
bint-is-cast(21,11)byte-bitlength-01(1,0)byte-nle-02(2,0)i2b-noteq(1,0)long-shiftzero-in(23,13)s144(1,0)short-law-righthift-not(24,12)short-nls(6,4)ubyte-neg(8,4)
bint-is-cast-01(6,5)byte-equal(4,3)byte-nls(2,1)ibi(0,0)long-shzr(3,2)s2i-switch(1,0)short-law-shift-snd-l(2,2)short-nls-01(3,2)ubyte-pos(2,1)
bint-mod(14,7)byte-equal-01(1,0)byte-nls-01(2,0)ibii(0,0)long2int-in(0,0)shiftright-byte-8-neg(6,3)short-law-shift-snd-r(3,2)short-not-max(1,0)ubyte-pos-01(2,1)
bint-mult2(4,2)byte-gr-127(2,1)byte-nls-02(5,3)ili(0,0)longin-mod(4,2)shiftright-byte-8-neg-01(7,3)short-law-shift-snd-rz(2,2)short-overflow(2,1)ubyte-pos-02(2,1)