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: |
|---|
| int2bits-add-high | proved | all subs proved
| int2bits-truein,
int2bits-neg-num,
int2bits-exneg,
uint2bits-2pot-02,
uint2bits-falsein-01,
uint2bits-truein,
uint2bits-empty,
uint2bits-zero,
uint2bits-sgn-02,
uint2bits-one,
uint2bits-pos-num,
uint2bits-2pot-01,
uint2bits-2pot,
int2bits-2pot,
int2bits-2pot-02,
int2bits-len-pos-suc,
uint2bits-add-high-02,
int2bits-lelen-07,
int2bits-pos,
int2bits-len-add,
int2bits-neg-03,
|
| uint2bits-add-high-02 | proved | all subs proved
| uint2bits-sgn-02,
int2bits-eq,
int2bits-first,
int2bits-truetrue-01,
int2bits-true,
int2bits-truein,
int2bits-not-empty,
uint2bits-add-high,
uint2bits-zero,
uint2bits-add-high-01,
|
| uint2bits-add-high-01 | proved | all subs proved
| uint2bits-one,
int2bits-neg-num,
int2bits-lslen-05,
int2bits-not-empty,
uint2bits-add-high,
uint2bits-zero,
uint2bits-mod2pot-01,
|
| int2bits-neg-04 | proved | all subs proved
| int2bits-neg-02,
|
| int2bits-len-pos-03 | proved | all subs proved
| int2bits-len-pos-02,
|
| int2bits-add-low | proved | all subs proved
| int2bits-lelen,
int2bits-neg-num,
int2bits-sgn-02,
int2bits-len-pos-pred,
int2bits-2pot,
int2bits-2pot-01,
int2bits-2pot-02,
int2bits-neg-02,
uint2bits-empty,
int2bits-lelen-04,
int2bits-len-add,
int2bits-zero,
uint2bits-add-low-01,
int2bits-eq,
int2bits-first-02,
int2bits-lslen-09,
int2bits-len-neg-01,
int2bits-not-empty,
uint2bits-pos-num,
uint2bits-one,
int2bits-pos-num,
int2bits-lelen-02,
int2bits-pos,
int2bits-neg-03,
|
| uint2bits-add-high | proved | all subs proved
| int2bits-zero,
int2bits-falsein-01,
uint2bits-zero-01,
int2bits-truein-01,
int2bits-not-empty,
uint2bits-2pot-02,
int2bits-neg-num,
int2bits-rec-neg,
int2bits-2pot-01,
uint2bits-zero,
int2bits-2pot,
int2bits-succ,
int2bits-2pot-02,
int2bits-neg-03,
uint2bits-one,
uint2bits-rec-01,
|
| int2bits-len-pos-02 | proved | all subs proved
| uint2bits-len-pos,
int2bits-pos,
|
| uint2bits-add-low-01 | proved | all subs proved
| uint2bits-one,
int2bits-neg-num,
int2bits-lslen-05,
int2bits-not-empty,
uint2bits-mod2pot-01,
uint2bits-add-low,
uint2bits-zero,
|
| int2bits-neg-02 | proved | all subs proved
| int2bits-restsgn,
int2bits-neg-03,
|
| int2bits-lslen-10 | proved | all subs proved
| int2bits-lelen-07,
|
| int2bits-lelen-05 | proved | all subs proved
| int2bits-leneq-neg,
int2bits-not-empty,
int2bits-lslen-02,
|
| int2bits-fill-rest | proved | all subs proved
| int2bits-first-01,
uint2bits-one,
int2bits-neg-num,
int2bits-lslen-05,
int2bits-not-empty,
|
| int2bits-restsgn | proved | all subs proved
| uint2bits-restsgn,
int2bits-len-pos,
uint2bits-one,
uint2bits-pos-num,
int2bits-zero,
int2bits-less-2pot-02,
int2bits-pos,
|
| uint2bits-len-pos | proved | all subs proved
| uint2bits-len-add,
|
| int2bits-leneq-neg | proved | all subs proved
| int2bits-len-neg,
int2bits-lslen-02,
int2bits-mone-02,
int2bits-lelen-02,
int2bits-not-empty,
|
| int2bits-lslen-05 | proved | all subs proved
| int2bits-first-01,
int2bits-not-empty,
uint2bits-one,
int2bits-neg-num,
int2bits-lslen-02,
|
| int2bits-neg-03 | proved | all subs proved
| int2bits-sgn,
uint2bits-zero,
uint2bits-eq,
uint2bits-onein,
uint2bits-empty,
int2bits-less-2pot,
uint2bits-one,
uint2bits-rec-01,
int2bits-neg,
int2bits-pos,
int2bits-not-empty,
bits2int-inj,
int2int-neg,
|
| int2bits-len-add | proved | all subs proved
| uint2bits-len-add,
int2bits-pos,
|
| int2bits-lelen-07 | proved | all subs proved
| int2bits-2pot-01,
int2bits-2pot,
int2bits-len-eq,
int2bits-len-neg-02,
int2bits-not-empty,
int2bits-len-eq-01,
int2bits-lelen-04,
|
| int2int-lastn-negneg | proved | all subs proved
| bits2int-nle,
bits2int-first-01,
bits2int-first,
bits2uint-inv-pos,
int2bits-first,
bits2int-split-01,
uint2bits-one,
int2bits-neg-num,
int2bits-lelen-02,
int2bits-first-01,
int2int-inj,
int2bits-not-empty,
|
| int2bits-rec-2pot-neg-03 | proved | all subs proved
| int2bits-inj,
int2bits-rec-2pot-neg-01,
int2bits-rec-2pot-neg-02,
|
| int2bits-len-abs-01 | proved | all subs proved
| int2bits-len-abs,
int2bits-not-empty,
|
| uint2bits-add-low | proved | all subs proved
| int2bits-zero,
int2bits-not-empty,
uint2bits-2pot-02,
int2bits-rec-neg,
int2bits-neg-num,
uint2bits-one,
uint2bits-pos-num,
|
| int2bits-less-2pot-02 | proved | all subs proved
| int2bits-less-2pot,
|
| int2bits-rec-2pot-neg-02 | proved | all subs proved
| int2int-inj,
uint2int-01,
bits2int-inv,
int2bits-neg-01,
uint2bits-len-max,
bits2int-sgn,
bits2int-inj,
uint2bits-first-05,
uint2bits-empty-01,
uint2bits-first-04,
uint2bits-one,
uint2bits-zero,
uint2bits-onein,
uint2bits-truein,
uint2bits-onein-01,
uint2bits-empty,
uint2bits-2potrec,
int2bits-neg,
|
| int2int-neg | proved | all subs proved
| uint2bits-one,
uint2bits-pos-num,
uint2bits-2pot-01,
uint2bits-len-01,
uint2bits-2pot,
uint2bits-len,
uint2bits-empty-01,
int2bits-not-empty,
uint2bits-zero,
uint2int-rest,
int2bits-less-2pot,
int2int-inj,
int2bits-pos,
|
| uint2bits-len-add | proved | all subs proved
| int2bits-zero,
int2bits-lslen-06,
int2bits-not-empty,
int2bits-pos,
uint2bits-empty,
uint2bits-mod2pot-01,
|
| int2bits-len-abs | proved | all subs proved
| int2bits-zero,
int2bits-2pot,
int2bits-2pot-01,
int2bits-len-neg-02,
int2bits-not-empty,
|
| int2bits-lslen-02 | proved | all subs proved
| int2bits-lelen-03,
|
| int2bits-lelen-02 | proved | all subs proved
| int2bits-lelen-03,
|
| int2bits-lelen-04 | proved | all subs proved
| uint2bits-one,
int2bits-neg-num,
int2bits-lelen-03,
|
| int2bits-rec-neg-03 | proved | all subs proved
| int2bits-inj,
uint2bits-one,
int2bits-neg-num,
int2bits-rec-neg,
|
| int2bits-rec-neg-02 | proved | all subs proved
| int2bits-inj,
int2bits-rec-neg,
|
| int2bits-rec-neg-01 | proved | all subs proved
| int2bits-true,
int2bits-eq,
uint2bits-one,
int2bits-neg-num,
int2bits-rec-neg,
|
| int2bits-one-bit | proved | all subs proved
| int2bits-eq,
int2bits-true,
int2bits-not-empty,
int2bits-mone-02,
int2bits-rec-neg,
int2bits-zero,
|
| int2bits-mod2-neg | proved | all subs proved
| int2bits-true,
uint2bits-one,
int2bits-neg-num,
int2bits-rec-neg,
int2bits-zero,
|
| int2bits-lslen-11 | proved | all subs proved
| int2bits-lslen-06,
|
| int2bits-lslen-04 | proved | all subs proved
| uint2bits-one,
int2bits-neg-num,
int2bits-lelen-03,
|
| int2bits-less-2pot-01 | proved | all subs proved
| int2bits-first-01,
int2bits-2pot,
int2bits-not-empty,
int2bits-len-mon,
int2bits-less-2pot,
|
| int2bits-len-pos-01 | proved | all subs proved
| int2bits-eq,
int2bits-first-02,
int2bits-len-range,
int2bits-not-empty,
|
| int2bits-len-mod2pot | proved | all subs proved
| int2bits-zero,
int2bits-lslen-06,
int2bits-not-empty,
|
| bits2uint-zero-01 | proved | all subs proved
| int2bits-truein,
int2bits-not-empty,
bits2uint-zeros,
bits2uint-not-zero,
int2uint-fill,
|
| bits2int8-02 | proved | all subs proved
| bits2int8,
|
| bits2int-nls | proved | all subs proved
| bits2uint-2pot,
ubits2ubits-neg,
ubits2ubits-pos,
bits2int-first-01,
bits2int-neg-03,
int2bits-pos,
int2bits-2pot,
int2bits-len-mon,
|
| bits2int-neg-1bit-01 | proved | all subs proved
| bits2int-inj,
bits2int-neg,
bits2int-sgn,
bits2int-sgn-intro,
|
| int2bits-rec-neg | proved | all subs proved
| uint2bits-falsein,
uint2bits-succ-intro,
uint2bits-rec-01,
int2bits-neg,
|
| int2bits-less-2pot | proved | all subs proved
| uint2bits-zero-01,
int2bits-pos,
uint2bits-empty,
uint2bits-zero,
int2bits-zero,
int2bits-eq,
int2bits-first-02,
uint2bits-2pot,
int2bits-not-empty,
uint2bits-len-mon,
|
| int2bits-len-range | proved | all subs proved
| int2bits-len-neg-01,
int2bits-len-pos,
int2bits-zero,
int2bits-not-empty,
|
| int2bits-lslen-06 | proved | all subs proved
| int2bits-eq,
int2bits-first-02,
int2bits-not-empty,
int2bits-lslen-01,
|
| int2bits-len-eq-01 | proved | all subs proved
| int2bits-len-eq,
|
| int2bits-len-neg-02 | proved | all subs proved
| int2bits-len-pos-pred,
int2bits-len-neg-01,
|
| int2bits-lelen-03 | proved | all subs proved
| int2bits-lelen,
int2bits-len-neg-01,
|
| int2bits-lslen-09 | proved | all subs proved
| int2bits-lslen-08,
int2bits-not-empty,
|
| uint2bits-truein | proved | all subs proved
| int2bits-truein-01,
int2bits-pos,
|
| int2uint-fill | proved | all subs proved
| int2int-inj,
bits2int-fill,
int2bits-first-02,
int2bits-not-empty,
bits2int-pos-02,
|
| bits2int8 | proved | all subs proved
| bits2int-le8,
|
| int2bits-len-mon | proved | all subs proved
| int2bits-len-neg-01,
uint2bits-len-mon-02,
uint2bits-empty,
int2bits-pos,
int2bits-not-empty,
|
| bits2int-inj | proved | all subs proved
| bits2bits-def,
int2bits-inj,
|
| int2uint-pos | proved | all subs proved
| int2int-inj,
int2bits-first-02,
int2bits-not-empty,
bits2uint-inv-neg,
|
| int2uint-inv-01 | proved | all subs proved
| int2uint-inv,
|
| int2int-lastn-pospos | proved | all subs proved
| bits2int-pos-02,
bits2uint-nle-01,
int2bits-first,
bits2uint-not-neg-01,
bits2uint-zeros-03,
int2bits-first-03,
bits2int-split,
int2bits-lelen-01,
int2bits-first-02,
int2int-inj,
int2bits-not-empty,
|
| int2int-lastn-posneg | proved | all subs proved
| ubits2bits,
bits2uint-nle-01,
int2bits-first,
bits2uint-not-neg-01,
bits2uint-zeros-03,
int2bits-first-03,
bits2int-split,
int2bits-first-02,
int2int-inj,
int2bits-not-empty,
|
| int2bits-succ-intro | proved | all subs proved
| uint2bits-succ-intro,
int2bits-pos,
|
| int2bits-pred-intro | proved | all subs proved
| uint2bits-pred-intro,
int2bits-pos,
|
| int2bits-lslen-03 | proved | all subs proved
| int2bits-lslen,
int2bits-len-neg-01,
|
| int2bits-leading-sgn | proved | all subs proved
| uint2bits-false,
uint2bits-zero,
uint2bits-zero-01,
uint2bits-firstpos,
uint2bits-empty,
int2bits-truetrue-01,
int2bits-mone-02,
int2bits-true,
int2bits-truein,
int2bits-first-06,
int2bits-pos,
int2bits-not-empty,
int2bits-first-02,
|
| int2bits-inv-first | proved | all subs proved
| int2bits-first-03,
int2bits-truein,
int2bits-not-empty,
|
| int2bits-fillsgn | proved | all subs proved
| int2bits-first-02,
int2bits-not-empty,
int2bits-inj,
|
| int2bits-fillfirst | proved | all subs proved
| int2bits-first-01,
int2bits-not-empty,
int2bits-first-02,
|
| int2bits-falsein-03 | proved | all subs proved
| int2bits-not-empty,
int2bits-falsein-02,
|
| int2bits-succ | proved | all subs proved
| uint2bits-succ,
int2bits-pos,
|
| int2bits-truein-01 | proved | all subs proved
| uint2bits-onein,
uint2bits-expos0,
int2bits-first,
int2int-inj,
bits2int-2pot,
int2bits-truein,
int2bits-not-empty,
int2bits-pos,
int2bits-2pot-01,
int2bits-zero,
|
| int2uint-inv | proved | all subs proved
| int2int-inj,
int2bits-first-01,
bits2int-neg-02,
int2bits-not-empty,
bits2uint-succ,
|
| uint2bits-succ-intro | proved | all subs proved
| uint2bits-pred,
|
| uint2int-01 | proved | all subs proved
| int2int-inj,
int2bits-pos,
|
| uint2bits-pred-intro | proved | all subs proved
| uint2bits-succ,
|
| int2bits-lslen-08 | proved | all subs proved
| int2bits-2pot-02,
int2bits-len-pos,
int2bits-zero,
uint2bits-pos-num,
uint2bits-one,
int2bits-neg-num,
int2bits-len-neg,
int2bits-not-empty,
|
| int2bits-len-eq | proved | all subs proved
| int2bits-len-pos,
int2bits-zero,
uint2bits-one,
int2bits-neg-num,
int2bits-len-neg,
|
| int2bits-first-03 | proved | all subs proved
| int2bits-first-04,
int2bits-truein,
|
| int2bits-falsein-02 | proved | all subs proved
| uint2bits-zero,
uint2bits-falsein-01,
uint2bits-one,
int2bits-neg-num,
int2bits-falsein-01,
int2bits-pos,
|
| int2bits-len-neg-01 | proved | all subs proved
| int2bits-len-neg,
int2bits-len-pos,
int2bits-zero,
uint2bits-one,
int2bits-neg-num,
|
| int2bits-first-02 | proved | all subs proved
| uint2bits-first-01,
int2bits-pos,
int2bits-not-empty,
int2bits-first-01,
|
| bits2int-le8 | proved | all subs proved
| bits2int-first-01,
bits2bits-def,
int2bits-len-neg,
|
| int2bits-inj | proved | all subs proved
| int2int-inj,
|
| uint2int-invsucc | proved | all subs proved
| int2int-inj,
int2bits-neg-01,
bits2int-sgn,
|
| int2int-rest-01 | proved | all subs proved
| bits2uint-one-03,
bits2uint-zeros-03,
bits2uint-split,
int2uint-neg,
bits2int-pos,
int2bits-truein,
uint2bits-one,
int2bits-neg-num,
int2bits-exneg,
|
| int2int-lastn-negpos | proved | all subs proved
| bits2bits-def,
int2bits-lelen-01,
bits2int-first,
bits2int-first-01,
bits2uint-inv-neg,
bits2uint-inv-pos,
int2bits-first,
bits2int-split-01,
int2bits-first-01,
int2int-inj,
int2bits-not-empty,
|
| int2bits-pred | proved | all subs proved
| uint2bits-pred,
int2bits-pos,
|
| int2bits-lslen-07 | proved | all subs proved
| int2bits-2pot,
int2bits-len-pos,
int2bits-pos-num,
int2bits-2pot-01,
int2bits-zero,
uint2bits-one,
int2bits-neg-num,
int2bits-len-neg,
int2bits-not-empty,
|
| int2bits-first-05 | proved | all subs proved
| int2bits-first-04,
|
| int2bits-bits2unit | proved | all subs proved
| int2bits-first-01,
int2bits-not-empty,
int2bits-bits2unit-01,
|
| int2bits-256-neg-mone | proved | all subs proved
| int2bits-2pot-neg-mone,
|
| bits2int-rec-true | proved | all subs proved
| bits2int-rec-04,
bits2int-rec,
|
| bits2int-neg-1bit | proved | all subs proved
| int2int-inj,
int2bits-sgn,
int2bits-first-01,
int2bits-not-empty,
bits2int-neg,
bits2int-sgn,
bits2int-sgn-intro,
|
| int2uint-neg | proved | all subs proved
| uint2uint-inv-01,
uint2bits-2pot-03,
bits2uint-2pot,
uint2bits-onein-01,
uint2bits-expos0,
uint2bits-sgn-2pot-01,
int2bits-neg,
|
| uint2bits-succ | proved | all subs proved
| uint2bits-sgn-false,
uint2bits-rec,
uint2bits-zero,
uint2bits-one,
uint2bits-pos-num,
uint2bits-rec-01,
|
| uint2bits-restsgn | proved | all subs proved
| uint2bits-2pot,
uint2bits-pos-num,
uint2bits-2pot-05,
uint2bits-false,
uint2bits-2pot-04,
uint2bits-first-01,
uint2bits-empty,
uint2bits-one,
uint2bits-rec-01,
|
| uint2bits-pred | proved | all subs proved
| uint2bits-sgn-false-01,
uint2bits-rec,
uint2bits-pos-num,
uint2bits-one,
uint2bits-zero,
uint2bits-rec-01,
|
| int2bits-first-06 | proved | all subs proved
| int2bits-first,
|
| int2bits-truetrue-01 | proved | all subs proved
| uint2bits-first-01,
int2bits-neg,
int2bits-pos,
int2bits-truein,
|
| int2bits-first-04 | proved | all subs proved
| uint2bits-first-01,
int2bits-pos,
int2bits-truein,
|
| int2bits-falsein-01 | proved | all subs proved
| uint2bits-false,
uint2bits-2pot-05,
uint2bits-first-05,
uint2bits-onein-01,
int2bits-neg,
|
| int2bits-sgn-02 | proved | all subs proved
| uint2bits-sgn-02,
uint2bits-falsein,
int2bits-neg,
int2bits-pos,
|
| int2bits-2pot-neg-mone | proved | all subs proved
| uint2bits-2pot-neg-mone,
int2bits-pos-num,
|
| bits2int-rec-04 | proved | all subs proved
| bits2int-ones,
bits2int-rec-03,
|
| int2bits-first-01 | proved | all subs proved
| int2bits-first,
int2bits-not-empty,
|
| int2int-inj | proved | all subs proved
| uint2bits-firstpos,
uint2bits-first-01,
uint2bits-empty,
bits2int-pos-02,
uint2uint-pos,
uint2bits-2pot-03,
bits2uint-2pot,
uint2bits-onein-01,
uint2bits-expos0,
int2bits-neg,
int2bits-first,
int2bits-not-empty,
bits2int-neg-01,
int2bits-pos,
|
| int2bits-len-neg | proved | all subs proved
| uint2bits-2pot,
uint2bits-len,
uint2bits-2pot-03,
uint2bits-onein-01,
uint2bits-expos1,
uint2bits-sgn-2pot-01,
int2bits-neg,
|
| int2unit-inv-rest | proved | all subs proved
| int2int-rest,
uint2bits-false,
uint2bits-firstpos,
uint2bits-eq,
int2bits-pos,
bits2uint-base,
int2bits-not-empty,
bits2uint-inv-pos,
|
| int2bits-truetrue | proved | all subs proved
| uint2bits-first-01,
int2bits-neg,
int2bits-pos,
int2bits-truein,
|
| bits2int8-03 | proved | all subs proved
| bits2int8-01,
|
| bits2int-zero-02 | proved | all subs proved
| bits2uint-ls,
bits2uint-one-03,
bits2uint-split,
bits2uint-not-zero,
bits2int-pos,
bits2ubits,
bits2int-zero-01,
|
| bits2int-mklist-03 | proved | all subs proved
| int2bits-not-empty,
bits2int-ones,
|
| bits2bits-mone | proved | all subs proved
| uint2bits-one,
int2bits-neg-num,
bits2int-ones,
|
| uint2bits-sgn-false | proved | all subs proved
| uint2bits-zero,
uint2bits-sgn,
uint2bits-first,
uint2bits-empty,
|
| uint2bits-sgn-false-01 | proved | all subs proved
| uint2bits-sgn,
uint2bits-onein,
|
| int2int-rest | proved | all subs proved
| uint2int-rest,
int2bits-pos,
|
| bits2int-fill | proved | all subs proved
| bits2int-sgn,
|
| bits2int-nle | proved | all subs proved
| bits2int-range,
|
| uint2bits-first-04 | proved | all subs proved
| uint2bits-first-01,
uint2bits-onein-01,
uint2bits-empty-01,
|
| uint2bits-sgn-2pot-01 | proved | all subs proved
| uint2bits-2pot,
uint2bits-sgn-2pot,
|
| int2bits-true | proved | all subs proved
| uint2bits-not-one,
uint2bits-falsein,
int2bits-neg,
int2bits-pos,
uint2bits-one,
int2bits-neg-num,
|
| int2bits-first | proved | all subs proved
| uint2bits-onein-01,
uint2bits-expos0,
int2bits-neg,
|
| uint2bits-first-05 | proved | all subs proved
| uint2bits-first-01,
uint2bits-onein-01,
|
| uint2bits-2pot-05 | proved | all subs proved
| uint2bits-zero,
uint2bits-2pot-02,
uint2bits-2pot-04,
uint2bits-zero-01,
uint2bits-firstpos,
uint2bits-first-01,
|
| uint2bits-sgn-02 | proved | all subs proved
| uint2bits-onein,
uint2bits-one,
uint2bits-expos1,
|
| int2bits-exneg | proved | all subs proved
| uint2bits-onein-01,
uint2bits-expos1,
int2bits-neg,
|
| uint2bits-2pot-neg-mone | proved | all subs proved
| uint2bits-inj,
uint2bits-zero,
uint2bits-one,
uint2bits-rec-01,
|
| int2bits-truein | proved | all subs proved
| uint2bits-onein,
uint2bits-onein-01,
int2bits-neg,
int2bits-pos,
int2bits-zero,
|
| bits2int8-01 | proved | all subs proved
| bits2int-le8-01,
|
| bits2uint-ls | proved | all subs proved
| bits2uint-nle-01,
|
| bits2int-sgn-intro | proved | all subs proved
| bits2int-sgn,
|
| int2bits-sgn | proved | all subs proved
| uint2bits-zero,
uint2bits-sgn,
int2bits-neg,
int2bits-pos,
|
| bits2int-ones | proved | all subs proved
| bits2int-one,
bits2int-sgn,
|
| int2bits-rest | proved | all subs proved
| uint2bits-one,
int2bits-neg-num,
int2bits-zero,
uint2bits-rest,
uint2bits-onein-01,
uint2bits-empty,
uint2bits-rec,
int2bits-neg,
int2bits-pos,
|
| int2bits-rec-2pot-pos | proved | all subs proved
| int2bits-zero,
int2bits-mod2pot,
|
| int2bits-ones | proved | all subs proved
| uint2bits-firstpos,
uint2bits-zero,
uint2bits-expos0,
uint2bits-onein-01,
uint2bits-expos1,
int2bits-neg,
int2bits-pos,
uint2bits-one,
int2bits-neg-num,
|
| int2bits-mod256 | proved | all subs proved
| int2bits-mod2pot,
|
| int2bits-lslen-12 | proved | all subs proved
| int2bits-lelen-06,
int2bits-lslen,
|
| int2bits-falsein | proved | all subs proved
| uint2bits-falsein,
int2bits-pos,
|
| int2bits-2pot-03 | proved | all subs proved
| uint2bits-2pot-02,
uint2bits-2pot-04,
uint2bits-empty,
uint2bits-first,
uint2bits-firstpos,
uint2bits-zero,
uint2bits-expos0,
int2bits-pos,
|
| bits2int16-03 | proved | all subs proved
| bits2int-range,
|
| bits2int16-02 | proved | all subs proved
| bits2int-range,
|
| bits2int16-01 | proved | all subs proved
| bits2int-range,
|
| bits2int16 | proved | all subs proved
| bits2int-range,
|
| bits2int-nls-02 | proved | all subs proved
| bits2int-range,
|
| bits2int-nls-01 | proved | all subs proved
| bits2int-range,
|
| bits2int-mklist-05 | proved | all subs proved
| bits2int-mklist-01,
|
| bits2bits-invert | proved | all subs proved
| bits2int-sgn,
bits2bits-def,
|
| uint2bits-sgn-2pot | proved | all subs proved
| uint2bits-2pot,
bits2uint-2pot-01,
uint2bits-firstpos,
uint2uint-pos,
uint2bits-onein,
uint2bits-expos0,
|
| uint2bits-mod2pot-01 | proved | all subs proved
| uint2bits-2potrec,
|
| uint2bits-inj | proved | all subs proved
| uint2bits-empty,
uint2bits-firstpos,
uint2bits-one,
uint2bits-zero-01,
uint2bits-zero,
uint2bits-rec-01,
|
| uint2int-rest | proved | all subs proved
| bits2uint-one-03,
bits2uint-split,
uint2uint-inv,
uint2bits-onein,
uint2bits-expos0,
bits2uint-zeros-03,
bits2uint-succ,
uint2bits-rest,
uint2bits-second,
bits2int-neg-01,
|
| bits2int-split | proved | all subs proved
| bits2uint-split,
bits2uint-zeros-03,
bits2int-pos-02,
|
| bits2uint-inv-neg | proved | all subs proved
| bits2uint-base,
bits2uint-zero,
bits2uint-one,
bits2uint-rec-01,
bits2int-pos-02,
|
| uint2bits-sgn | proved | all subs proved
| uint2bits-onein,
uint2bits-zero-01,
uint2bits-second,
uint2bits-empty,
uint2bits-first,
|
| int2bits-rec-2pot-neg-01 | proved | all subs proved
| int2bits-2pot-04,
int2bits-zero,
|
| bits2int-inv | proved | all subs proved
| bits2uint-zeros-03,
bits2uint-succ,
bits2int-neg,
bits2int-pos,
bits2int-pos-02,
|
| int2bits-mod2pot | proved | all subs proved
| uint2bits-2potrec,
int2bits-pos,
|
| int2bits-lelen-06 | proved | all subs proved
| int2bits-not-empty,
int2bits-lslen-01,
|
| uint2bits-2pot-03 | proved | all subs proved
| uint2uint-pos,
bits2uint-2pot-01,
uint2bits-firstpos,
uint2bits-2pot,
|
| uint2bits-falsein | proved | all subs proved
| uint2bits-false,
uint2bits-zero-01,
uint2bits-zero,
uint2bits-one,
uint2bits-rec-01,
uint2bits-firstpos,
uint2bits-not-one,
uint2bits-onein,
uint2bits-empty,
|
| uint2bits-expos1 | proved | all subs proved
| uint2bits-zero-01,
uint2bits-zero,
uint2bits-one,
uint2bits-rec-01,
uint2bits-onein,
uint2bits-firstpos,
uint2bits-expos0,
|
| uint2bits-onein-01 | proved | all subs proved
| uint2bits-onein,
|
| uint2bits-2pot-04 | proved | all subs proved
| uint2bits-2pot-02,
bits2uint-ones,
bits2uint-zeros-03,
uint2uint-pos,
uint2bits-firstpos,
|
| bits2uint-nle-01 | proved | all subs proved
| bits2uint-nle,
|
| bits2int-le8-01 | proved | all subs proved
| bits2bits-def,
int2bits-len-pos,
|
| bits2int-range | proved | all subs proved
| bits2uint-not-neg-01,
bits2uint-nle,
bits2uint-zeros-03,
bits2uint-succ,
bits2int-neg,
bits2int-pos-02,
|
| bits2int-mklist-01 | proved | all subs proved
| bits2int-neg,
bits2int-sign,
|
| bits2int-sgn | proved | all subs proved
| bits2int-sign,
|
| uint2uint-neg | proved | all subs proved
| uint2uint-pos,
|
| uint2bits-sgn-first | proved | all subs proved
| uint2bits-onein,
uint2bits-expos0,
|
| uint2bits-sgn-01 | proved | all subs proved
| uint2bits-firstpos,
uint2bits-zero,
uint2bits-expos0,
|
| int2uint-pos-01 | proved | all subs proved
| uint2uint-pos,
int2bits-pos,
|
| int2int-lastn-2pot | proved | all subs proved
| bits2int-zeros-03,
bits2int-zero,
int2bits-zero,
int2bits-2pot-04,
|
| int2bits-leneq-pos | proved | all subs proved
| int2bits-len-pos,
int2bits-lelen-01,
int2bits-lslen-01,
int2bits-not-empty,
int2bits-len-one,
|
| int2bits-expos | proved | all subs proved
| int2bits-pos,
uint2bits-onein,
uint2bits-expos0,
|
| int2bits-2pot-05 | proved | all subs proved
| int2bits-2pot-04,
|
| bits2int-rec-false | proved | all subs proved
| bits2int-pos,
bits2uint-zeros-03,
bits2uint-zero,
bits2int-neg,
bits2int-pos-02,
|
| bits2int-ones-01 | proved | all subs proved
| bits2int-neg,
bits2int-sign,
|
| bits2int-mklist-06 | proved | all subs proved
| bits2int-mklist-02,
|
| bits2int-mklist | proved | all subs proved
| bits2int-sign,
|
| bits2int-lez | proved | all subs proved
| bits2int-first,
bits2int-first-01,
|
| bits2int-lasteq | proved | all subs proved
| bits2uint-one,
bits2uint-succ,
bits2int-pos,
bits2uint-zeros-03,
bits2int-pos-02,
bits2uint-zero,
bits2int-pos-01,
bits2int-rec-01,
bits2int-neg,
bits2int-rec,
|
| bits2int-ge-zero | proved | all subs proved
| bits2int-first-01,
bits2int-first,
|
| bits2uint-2pot-01 | proved | all subs proved
| bits2uint-2pot,
bits2uint-zeros-03,
|
| bits2int-split-01 | proved | all subs proved
| bits2uint-ones,
bits2uint-zeros,
bits2uint-succ,
bits2uint-split,
bits2uint-zeros-03,
bits2int-neg,
|
| bits2uint-inv-pos | proved | all subs proved
| bits2uint-succ,
bits2int-neg,
bits2uint-zeros-03,
|
| uint2uint-pos | proved | all subs proved
| bits2uint-zero,
bits2uint-rec-02,
bits2uint-one-02,
uint2bits-zero,
bits2uint-one-03,
bits2uint-zeros-03,
uint2bits-one,
uint2bits-rec-01,
|
| uint2bits-2potrec | proved | all subs proved
| uint2bits-empty,
uint2bits-len-min,
uint2bits-div2pot,
uint2bits-zero,
uint2bits-one,
uint2bits-2pot,
uint2bits-mod2pot,
|
| int2bits-lslen | proved | all subs proved
| int2bits-not-empty,
int2bits-lelen,
|
| int2bits-lelen-01 | proved | all subs proved
| int2bits-lelen,
|
| int2bits-lslen-01 | proved | all subs proved
| int2bits-lelen,
|
| uint2bits-false | proved | all subs proved
| uint2bits-zero,
uint2bits-second,
|
| uint2bits-onein | proved | all subs proved
| uint2bits-zero-01,
uint2bits-empty,
uint2bits-second,
|
| int2bits-bits2unit-01 | proved | all subs proved
| ubits2ubits-def,
bits2uint-not-neg-01,
int2bits-pos,
int2bits-neg,
|
| int2bits-len-pos-suc | proved | all subs proved
| int2bits-len-pos-pred,
|
| int2bits-2pot-04 | proved | all subs proved
| int2bits-pos,
uint2bits-2pot-01,
uint2bits-2pot-06,
int2bits-neg,
int2bits-pos-num,
|
| uint2bits-expos0 | proved | all subs proved
| uint2bits-zero-01,
uint2bits-second,
uint2bits-first,
uint2bits-empty,
|
| uint2bits-firstpos | proved | all subs proved
| uint2bits-first-01,
|
| bits2ubits | proved | all subs proved
| ubits2bits,
|
| bits2int-rec-03 | proved | all subs proved
| bits2uint-one-03,
bits2uint-succ,
bits2uint-base,
bits2uint-ones,
bits2uint-2pot,
bits2uint-zeros-03,
bits2uint-one,
bits2int-neg,
bits2int-one,
|
| bits2uint-nle | proved | all subs proved
| ubits2ubits-def,
uint2bits-2pot,
uint2bits-len-mon,
|
| ubits2ubits-pos | proved | all subs proved
| ubits2ubits-def,
bits2uint-zeros-03,
|
| ubits2ubits-neg | proved | all subs proved
| ubits2ubits-def,
|
| bits2int-mklist-02 | proved | all subs proved
| bits2int-zero,
bits2uint-zeros-04,
bits2int-one,
bits2uint-one-03,
bits2uint-mklist,
bits2int-neg,
bits2int-pos-01,
|
| bits2int-sign | proved | all subs proved
| bits2uint-zeros-02,
bits2uint-zeros-03,
bits2int-pos,
bits2int-neg-01,
bits2int-neg,
bits2int-pos-01,
|
| bits2int-rec-01 | proved | all subs proved
| bits2uint-one,
bits2uint-zeros-03,
bits2int-neg,
|
| bits2int-pos-02 | proved | all subs proved
| bits2uint-zeros-03,
bits2int-pos,
|
| bits2int-first | proved | all subs proved
| bits2uint-mone,
bits2uint-zeros-03,
bits2uint-succ,
bits2uint-not-neg,
bits2int-neg,
|
| bits2bits-def | proved | all subs proved
| bits2uint-not-neg-01,
int2bits-pos,
bits2uint-one,
ubits2ubits-def,
bits2uint-zeros,
bits2uint-not-zero,
int2bits-zero,
bits2uint-not-neg,
int2bits-neg,
bits2int-neg,
bits2int-pos-01,
|
| uint2bits-inv | proved | all subs proved
| uint2bits-first-01,
|
| bits2int-zeros-02 | proved | all subs proved
| bits2uint-zeros-03,
bits2int-pos,
|
| bits2int-zeros-01 | proved | all subs proved
| bits2uint-zeros-03,
bits2uint-zeros-02,
bits2int-neg,
bits2int-pos-01,
bits2int-pos,
|
| bits2int-zeros | proved | all subs proved
| bits2uint-mklist,
bits2int-pos-01,
bits2int-pos,
|
| bits2int-ones-02 | proved | all subs proved
| bits2uint-zeros-03,
bits2uint-zeros-02,
bits2uint-2pot,
bits2int-pos,
bits2int-neg-03,
bits2int-neg,
|
| bits2int-mklist-04 | proved | all subs proved
| int2bits-not-empty,
bits2int-zeros-03,
|
| bits2bits-2pot-01 | proved | all subs proved
| int2bits-2pot-01,
bits2uint-2pot-02,
bits2int-neg,
|
| bits2bits-2pot | proved | all subs proved
| int2bits-2pot-01,
bits2int-2pot,
|
| uint2bits-second | proved | all subs proved
| uint2bits-zero-01,
uint2bits-not-one,
uint2bits-empty,
uint2bits-one,
uint2bits-rec-01,
|
| uint2bits-mod2pot | proved | all subs proved
| uint2bits-zero-01,
uint2bits-len-min,
uint2bits-pos-num,
uint2bits-2pot-01,
uint2bits-2pot,
uint2bits-zero,
uint2bits-empty,
uint2bits-one,
uint2bits-rec-01,
|
| uint2uint-inv-01 | proved | all subs proved
| uint2uint-inv,
uint2bits-empty,
bits2uint-succ,
|
| uint2bits-rest | proved | all subs proved
| uint2bits-eq,
uint2bits-empty,
|
| uint2bits-len-mon-02 | proved | all subs proved
| uint2bits-len-mon,
uint2bits-empty,
|
| uint2bits-first-01 | proved | all subs proved
| uint2bits-first,
|
| int2bits-eq | proved | all subs proved
| uint2bits-zero-01,
int2bits-neg,
int2bits-pos,
int2bits-zero,
|
| int2bits-len-pos-pred | proved | all subs proved
| int2bits-len-pos,
int2bits-zero,
uint2bits-one,
int2bits-neg-num,
|
| int2bits-lelen | proved | all subs proved
| int2bits-len-pos,
int2bits-zero,
|
| uint2bits-2pot-06 | proved | all subs proved
| uint2bits-2pot-01,
|
| ubits2bits | proved | all subs proved
| bits2uint-base,
bits2uint-zero,
bits2uint-one,
bits2uint-rec,
bits2uint-succ,
bits2int-neg-03,
|
| bits2int-zeros-03 | proved | all subs proved
| bits2int-zero-01,
|
| bits2uint-mklist | proved | all subs proved
| bits2uint-zeros-02,
|
| bits2int-first-01 | proved | all subs proved
| bits2uint-not-neg-01,
bits2int-pos,
|
| bits2uint-zeros-03 | proved | all subs proved
| bits2uint-zeros-02,
|
| bits2uint-mone | proved | all subs proved
| bits2uint-not-neg-01,
|
| ubits2ubits-def | proved | all subs proved
| uint2bits-one,
uint2bits-empty,
bits2uint-not-neg-01,
bits2uint-zeros,
bits2uint-not-zero,
bits2uint-not-neg,
uint2bits-rec,
bits2uint-zero,
bits2uint-rec-02,
uint2bits-zero,
bits2uint-base,
|
| bits2uint-2pot-02 | proved | all subs proved
| bits2uint-2pot,
|
| bits2int-2pot | proved | all subs proved
| bits2uint-2pot,
bits2int-neg,
|
| uint2bits-len-mon-01 | proved | all subs proved
| uint2bits-len-mon,
uint2bits-empty,
|
| uint2bits-first-03 | proved | all subs proved
| uint2bits-first,
|
| uint2bits-first-02 | proved | all subs proved
| uint2bits-first,
|
| uint2bits-div2pot-01 | proved | all subs proved
| uint2bits-2pot-01,
uint2bits-div2pot,
|
| bits2int-one-01 | proved | all subs proved
| bits2int-one,
|
| bits2bits-zeros | proved | all subs proved
| int2bits-zero,
bits2int-zero-01,
|
| uint2uint-inv | proved | all subs proved
| bits2uint-rec-02,
bits2uint-one-03,
bits2uint-zero,
uint2bits-one,
uint2bits-rec-01,
|
| uint2bits-len-min | proved | all subs proved
| uint2bits-len,
uint2bits-zero,
|
| uint2bits-not-one | proved | all subs proved
| uint2bits-empty,
uint2bits-zero,
uint2bits-one,
uint2bits-rec-01,
|
| uint2bits-empty-01 | proved | all subs proved
| uint2bits-empty,
|
| uint2bits-len-max | proved | all subs proved
| uint2bits-len,
uint2bits-zero,
uint2bits-empty,
|
| uint2bits-eq | proved | all subs proved
| uint2bits-empty,
uint2bits-one,
uint2bits-rec-01,
|
| int2bits-len-one | proved | all subs proved
| uint2bits-empty,
uint2bits-one,
uint2bits-rec,
int2bits-pos,
int2bits-zero,
|
| uint2bits-zero-01 | proved | all subs proved
| uint2bits-empty,
uint2bits-one,
uint2bits-rec-01,
uint2bits-zero,
|
| int2bits-2pot-02 | proved | all subs proved
| uint2bits-zero,
uint2bits-2pot-02,
int2bits-pos,
|
| uint2bits-falsein-01 | proved | all subs proved
| uint2bits-empty,
uint2bits-one,
uint2bits-rec-01,
|
| uint2bits-2pot-01 | proved | all subs proved
| uint2bits-rec,
uint2bits-one,
uint2bits-2pot,
uint2bits-rec-01,
|
| uint2bits-first | proved | all subs proved
| uint2bits-empty,
uint2bits-zero,
uint2bits-one,
uint2bits-rec-01,
|
| uint2bits-len-mon | proved | all subs proved
| uint2bits-one,
uint2bits-zero,
uint2bits-rec-01,
uint2bits-empty,
|
| bits2uint-zeros-02 | proved | all subs proved
| bits2uint-zeros,
bits2uint-base,
bits2uint-split,
|
| int2bits-2pot | proved | all subs proved
| uint2bits-2pot,
int2bits-pos,
|
| int2bits-not-empty | proved | all subs proved
| uint2bits-empty,
int2bits-neg,
int2bits-pos,
|
| bits2int-one | proved | all subs proved
| bits2uint-one-03,
bits2int-neg,
|
| bits2uint-zeros-04 | proved | all subs proved
| bits2uint-not-zero,
bits2uint-zeros,
|
| int2bits-len-pos | proved | all subs proved
| uint2bits-len,
int2bits-pos,
|
| bits2uint-succ | proved | all subs proved
| bits2uint-base,
bits2uint-one-03,
bits2uint-zero,
bits2uint-one,
|
| bits2uint-2pot | proved | all subs proved
| bits2uint-zeros,
bits2uint-one-03,
bits2uint-split,
|
| bits2int-zero-01 | proved | all subs proved
| bits2uint-zeros,
bits2int-neg,
bits2int-pos-01,
|
| bits2uint-not-neg-01 | proved | all subs proved
| bits2uint-not-neg,
|
| int2bits-2pot-01 | proved | all subs proved
| uint2bits-2pot,
int2bits-neg,
|
| int2bits-mod2 | proved | all subs proved
| int2bits-zero,
uint2bits-one,
int2bits-neg-num,
|
| bits2uint-zeros-01 | proved | all subs proved
| bits2uint-zeros,
|
| bits2uint-not-zero-01 | proved | all subs proved
| bits2uint-not-zero,
|
| uint2bits-div2pot | proved | all subs proved
| uint2bits-zero,
uint2bits-rec,
uint2bits-one,
uint2bits-rec-01,
|
| uint2bits-len-01 | proved | all subs proved
| uint2bits-one,
uint2bits-rec-01,
|
| uint2bits-len | proved | all subs proved
| uint2bits-one,
uint2bits-rec-01,
|
| int2bits-mone-02 | proved | all subs proved
| uint2bits-one,
int2bits-neg-num,
|
| uint2bits-empty | proved | all subs proved
| uint2bits-zero,
uint2bits-one,
uint2bits-rec-01,
|
| uint2bits-2pot-02 | proved | all subs proved
| uint2bits-one,
uint2bits-rec-01,
|
| uint2bits-2pot | proved | all subs proved
| uint2bits-zero,
uint2bits-one,
uint2bits-rec-01,
|
| bits2uint-split | proved | all subs proved
| bits2uint-one,
bits2uint-base,
bits2uint-zero,
bits2uint-rec-02,
|
| bits2uint-one-03 | proved | all subs proved
| bits2uint-one-01,
|
| bits2uint-not-neg | proved | all subs proved
| bits2uint-zero,
bits2uint-rec-02,
bits2uint-base,
|
| int2bits-zero | proved | all subs proved
| uint2bits-zero,
int2bits-pos-num,
|
| bits2uint-not-zero | proved | all subs proved
| bits2uint-zero,
bits2uint-base,
bits2uint-rec,
|
| bits2uint-zeros | proved | all subs proved
| bits2uint-zero,
bits2uint-base,
bits2uint-rec,
|
| int2bits-rec-pos-01 | proved | all subs proved
| int2bits-rec-pos,
|
| int2bits-mone-01 | proved | all subs proved
| uint2bits-one,
int2bits-neg-num,
|
| int2bits-mone | proved | all subs proved
| uint2bits-one,
int2bits-neg-num,
|
| int2bits-mod2-len | proved | all subs proved
| uint2bits-zero,
uint2bits-one,
int2bits-neg-num,
int2bits-pos,
|
| int2bits-len-2-32-1 | proved | all subs proved
| uint2bits-one,
uint2bits-pos-num,
int2bits-pos-num,
|
| int2bits-011x | proved | all subs proved
| uint2bits-one,
uint2bits-pos-num,
int2bits-pos-num,
|
| bits2int-zero-03 | proved | all subs proved
| bits2int-zero,
|
| bits2int-011x | proved | all subs proved
| bits2uint-base,
bits2uint-ones,
bits2int-pos,
|
| bits2uint-one-02 | proved | all subs proved
| bits2uint-base,
bits2uint-zero,
|
| bits2int-neg-02 | proved | all subs proved
| bits2int-neg,
|
| int2bits-rec-pos | proved | all subs proved
| uint2bits-rec,
int2bits-pos,
|
| int2bits-neg-01 | proved | all subs proved
| int2bits-neg,
|
| uint2bits-rec-01 | proved | all subs proved
| uint2bits-rec,
|
| int2bits-pos-num | proved | all subs proved
| int2bits-pos,
|
| uint2bits-pos-num | proved | all subs proved
| uint2bits-rec,
|
| bits2uint-one-01 | proved | all subs proved
| bits2uint-base,
bits2uint-one,
|
| bits2uint-rec | proved | all subs proved
| bits2uint-one,
|
| bits2uint-rec-02 | proved | all subs proved
| bits2uint-one,
|
| bits2uint-rec-01 | proved | all subs proved
| bits2uint-zero,
|
| bits2int-neg-01 | proved | all subs proved
| bits2int-neg,
|
| bits2int-neg-03 | proved | all subs proved
| bits2int-neg,
|
| bits2int-zero | proved | all subs proved
| bits2uint-base,
bits2int-pos,
|
| bits2int-rec | proved | all subs proved
| bits2uint-one,
bits2int-pos,
|
| bits2uint-ones | proved | all subs proved
| bits2uint-base,
bits2uint-one,
|
| int2bits-neg-num | proved | all subs proved
| int2bits-neg,
|
| bits2int-pos-01 | proved | all subs proved
| bits2int-pos,
|
| uint2bits-rec | axiom | | |
| uint2bits-zero | axiom | | |
| bits2uint-zero | axiom | | |
| bits2int-pos | axiom | | |
| bits2uint-base | axiom | | |
| uint2bits-one | axiom | | |
| int2bits-neg | axiom | | |
| bits2uint-one | axiom | | |
| int2bits-pos | axiom | | |
| bits2int-neg | axiom | | |