[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 int2bits
Status:
Proved!
Axioms: 11, User Theorems: 311 (Proved: 311, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 2710, Interactions: 1390
bits2bits-2pot(1,0)
bits2int-nls(17,9)
bits2int16-02(2,1)
bits2uint-zero-01(5,3)
int2bits-first-04(2,1)
int2bits-leneq-neg(21,11)
int2bits-one-bit(6,4)
int2int-lastn-pospos(20,10)
uint2bits-eq(2,1)
uint2bits-rec(0,0)
bits2bits-2pot-01(1,0)
bits2int-nls-01(6,3)
bits2int16-03(2,1)
bits2uint-zeros(10,5)
int2bits-first-05(1,0)
int2bits-leneq-pos(17,9)
int2bits-ones(12,7)
int2int-neg(39,21)
uint2bits-expos0(12,4)
uint2bits-rec-01(2,1)
bits2bits-def(26,12)
bits2int-nls-02(2,1)
bits2int8(2,1)
bits2uint-zeros-01(2,1)
int2bits-first-06(1,0)
int2bits-less-2pot(7,3)
int2bits-pos(0,0)
int2int-rest(2,2)
uint2bits-expos1(6,3)
uint2bits-rest(2,1)
bits2bits-invert(2,1)
bits2int-one(1,1)
bits2int8-01(2,1)
bits2uint-zeros-02(6,3)
int2bits-inj(3,2)
int2bits-less-2pot-01(8,4)
int2bits-pos-num(2,1)
int2int-rest-01(13,9)
uint2bits-false(4,2)
uint2bits-restsgn(126,81)
bits2bits-mone(1,0)
bits2int-one-01(1,0)
bits2int8-02(4,2)
bits2uint-zeros-03(1,1)
int2bits-inv-first(4,1)
int2bits-less-2pot-02(6,3)
int2bits-pred(5,3)
int2uint-fill(5,3)
uint2bits-falsein(17,9)
uint2bits-second(13,7)
bits2bits-zeros(1,0)
bits2int-ones(2,1)
bits2int8-03(4,2)
bits2uint-zeros-04(1,1)
int2bits-leading-sgn(10,5)
int2bits-lslen(8,2)
int2bits-pred-intro(4,3)
int2uint-inv(2,2)
uint2bits-falsein-01(25,15)
uint2bits-sgn(12,6)
bits2int-011x(2,1)
bits2int-ones-01(1,1)
bits2ubits(2,1)
int2bits-011x(1,0)
int2bits-lelen(12,7)
int2bits-lslen-01(1,1)
int2bits-rec-2pot-neg-01(4,2)
int2uint-inv-01(1,1)
uint2bits-first(8,4)
uint2bits-sgn-01(4,2)
bits2int-2pot(1,0)
bits2int-ones-02(13,7)
bits2uint-2pot(5,2)
int2bits-256-neg-mone(4,3)
int2bits-lelen-01(2,1)
int2bits-lslen-02(1,1)
int2bits-rec-2pot-neg-02(82,48)
int2uint-neg(16,9)
uint2bits-first-01(4,2)
uint2bits-sgn-02(4,2)
bits2int-base(0,0)
bits2int-pos(0,0)
bits2uint-2pot-01(3,2)
int2bits-2pot(1,1)
int2bits-lelen-02(2,1)
int2bits-lslen-03(4,2)
int2bits-rec-2pot-neg-03(4,4)
int2uint-pos(2,1)
uint2bits-first-02(1,0)
uint2bits-sgn-2pot(12,6)
bits2int-fill(3,2)
bits2int-pos-01(2,0)
bits2uint-2pot-02(1,1)
int2bits-2pot-01(1,1)
int2bits-lelen-03(4,2)
int2bits-lslen-04(1,1)
int2bits-rec-2pot-pos(3,2)
int2uint-pos-01(2,1)
uint2bits-first-03(2,1)
uint2bits-sgn-2pot-01(1,1)
bits2int-first(4,1)
bits2int-pos-02(2,0)
bits2uint-base(0,0)
int2bits-2pot-02(3,2)
int2bits-lelen-04(1,1)
int2bits-lslen-05(10,3)
int2bits-rec-neg(21,11)
int2unit-inv-rest(10,3)
uint2bits-first-04(4,1)
uint2bits-sgn-false(4,2)
bits2int-first-01(2,0)
bits2int-range(18,6)
bits2uint-inv-neg(18,9)
int2bits-2pot-03(7,4)
int2bits-lelen-05(10,5)
int2bits-lslen-06(10,3)
int2bits-rec-neg-01(4,2)
ubits2bits(22,12)
uint2bits-first-05(2,1)
uint2bits-sgn-false-01(2,1)
bits2int-ge-zero(1,0)
bits2int-rec(2,0)
bits2uint-inv-pos(4,1)
int2bits-2pot-04(25,12)
int2bits-lelen-06(10,3)
int2bits-lslen-07(31,18)
int2bits-rec-neg-02(4,2)
ubits2ubits-def(28,16)
uint2bits-firstpos(1,0)
uint2bits-sgn-first(9,4)
bits2int-inj(2,1)
bits2int-rec-01(2,0)
bits2uint-ls(2,1)
int2bits-2pot-05(4,3)
int2bits-lelen-07(14,6)
int2bits-lslen-08(25,13)
int2bits-rec-neg-03(4,2)
ubits2ubits-neg(4,1)
uint2bits-inj(15,8)
uint2bits-succ(18,10)
bits2int-inv(10,3)
bits2int-rec-03(8,4)
bits2uint-mklist(1,1)
int2bits-2pot-neg-mone(6,3)
int2bits-len-2-32-1(1,0)
int2bits-lslen-09(3,2)
int2bits-rec-pos(5,3)
ubits2ubits-pos(4,1)
uint2bits-inv(2,1)
uint2bits-succ-intro(2,1)
bits2int-lasteq(38,10)
bits2int-rec-04(4,2)
bits2uint-mone(3,2)
int2bits-add-high(59,30)
int2bits-len-abs(8,4)
int2bits-lslen-10(4,3)
int2bits-rec-pos-01(2,1)
uint2bits-2pot(13,7)
uint2bits-len(17,8)
uint2bits-truein(5,3)
bits2int-le8(16,9)
bits2int-rec-false(6,1)
bits2uint-nle(4,2)
int2bits-add-low(60,36)
int2bits-len-abs-01(2,1)
int2bits-lslen-11(2,1)
int2bits-rest(21,11)
uint2bits-2pot-01(11,5)
uint2bits-len-01(21,10)
uint2bits-zero(0,0)
bits2int-le8-01(11,6)
bits2int-rec-true(4,2)
bits2uint-nle-01(4,2)
int2bits-bits2unit(3,2)
int2bits-len-add(11,7)
int2bits-lslen-12(6,3)
int2bits-restsgn(15,7)
uint2bits-2pot-02(14,7)
uint2bits-len-add(12,6)
uint2bits-zero-01(2,1)
bits2int-lez(1,0)
bits2int-sgn(7,3)
bits2uint-not-neg(10,6)
int2bits-bits2unit-01(5,3)
int2bits-len-eq(12,6)
int2bits-mod2(2,1)
int2bits-sgn(4,3)
uint2bits-2pot-03(4,3)
uint2bits-len-max(6,3)
uint2int-01(2,1)
bits2int-mklist(1,1)
bits2int-sgn-intro(1,0)
bits2uint-not-neg-01(2,1)
int2bits-eq(6,3)
int2bits-len-eq-01(3,2)
int2bits-mod2-len(8,5)
int2bits-sgn-02(8,4)
uint2bits-2pot-04(8,5)
uint2bits-len-min(6,3)
uint2int-invsucc(3,2)
bits2int-mklist-01(4,4)
bits2int-sign(19,5)
bits2uint-not-zero(8,4)
int2bits-exneg(12,6)
int2bits-len-mod2pot(6,3)
int2bits-mod2-neg(8,4)
int2bits-succ(5,3)
uint2bits-2pot-05(12,7)
uint2bits-len-mon(10,5)
uint2int-rest(18,10)
bits2int-mklist-02(3,1)
bits2int-split(5,2)
bits2uint-not-zero-01(2,1)
int2bits-expos(5,3)
int2bits-len-mon(32,17)
int2bits-mod256(4,3)
int2bits-succ-intro(4,3)
uint2bits-2pot-06(3,2)
uint2bits-len-mon-01(2,1)
uint2uint-inv(8,5)
bits2int-mklist-03(1,1)
bits2int-split-01(16,7)
bits2uint-one(0,0)
int2bits-falsein(2,1)
int2bits-len-neg(30,19)
int2bits-mod2pot(10,5)
int2bits-true(8,4)
uint2bits-2pot-neg-mone(16,8)
uint2bits-len-mon-02(2,1)
uint2uint-inv-01(4,2)
bits2int-mklist-04(1,1)
bits2int-zero(1,1)
bits2uint-one-01(2,1)
int2bits-falsein-01(50,27)
int2bits-len-neg-01(6,3)
int2bits-mone(1,0)
int2bits-truein(8,4)
uint2bits-2potrec(18,9)
uint2bits-len-pos(2,1)
uint2uint-neg(2,1)
bits2int-mklist-05(2,1)
bits2int-zero-01(6,1)
bits2uint-one-02(1,1)
int2bits-falsein-02(11,4)
int2bits-len-neg-02(7,3)
int2bits-mone-01(1,0)
int2bits-truein-01(19,10)
uint2bits-add-high(122,67)
uint2bits-mod2pot(64,30)
uint2uint-pos(8,5)
bits2int-mklist-06(2,1)
bits2int-zero-02(12,4)
bits2uint-one-03(1,1)
int2bits-falsein-03(6,2)
int2bits-len-one(4,2)
int2bits-mone-02(1,0)
int2bits-truetrue(5,2)
uint2bits-add-high-01(11,7)
uint2bits-mod2pot-01(6,3)
bits2int-neg(0,0)
bits2int-zero-03(1,0)
bits2uint-ones(8,4)
int2bits-fill-rest(4,2)
int2bits-len-pos(3,2)
int2bits-neg(0,0)
int2bits-truetrue-01(4,2)
uint2bits-add-high-02(25,11)
uint2bits-not-one(2,1)
bits2int-neg-01(2,0)
bits2int-zeros(3,1)
bits2uint-rec(2,1)
int2bits-fillfirst(2,1)
int2bits-len-pos-01(6,3)
int2bits-neg-01(2,1)
int2bits-zero(1,0)
uint2bits-add-low(42,23)
uint2bits-one(0,0)
bits2int-neg-02(2,0)
bits2int-zeros-01(7,2)
bits2uint-rec-01(2,1)
int2bits-fillsgn(6,3)
int2bits-len-pos-02(6,3)
int2bits-neg-02(6,2)
int2int-inj(29,13)
uint2bits-add-low-01(17,10)
uint2bits-onein(6,3)
bits2int-neg-03(2,0)
bits2int-zeros-02(1,0)
bits2uint-rec-02(1,0)
int2bits-first(7,3)
int2bits-len-pos-03(3,2)
int2bits-neg-03(38,20)
int2int-lastn-2pot(5,2)
uint2bits-div2pot(20,9)
uint2bits-onein-01(2,1)
bits2int-neg-1bit(2,2)
bits2int-zeros-03(2,1)
bits2uint-split(16,8)
int2bits-first-01(2,1)
int2bits-len-pos-pred(8,4)
int2bits-neg-04(4,1)
int2int-lastn-negneg(23,12)
uint2bits-div2pot-01(7,3)
uint2bits-pos-num(3,1)
bits2int-neg-1bit-01(2,2)
bits2int16(2,1)
bits2uint-succ(8,4)
int2bits-first-02(4,1)
int2bits-len-pos-suc(2,1)
int2bits-neg-num(3,1)
int2int-lastn-negpos(26,14)
uint2bits-empty(2,1)
uint2bits-pred(16,9)
bits2int-nle(6,3)
bits2int16-01(2,1)
bits2uint-zero(0,0)
int2bits-first-03(2,1)
int2bits-len-range(20,10)
int2bits-not-empty(4,2)
int2int-lastn-posneg(17,8)
uint2bits-empty-01(1,0)
uint2bits-pred-intro(4,2)