[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 int-mult
- Status: Proved!
- Axioms: 3,
User Theorems: 296
(Proved: 296,
Partially proved: 0,
Unproved: 0,
Invalid: 0,
Siginvalid: 0)
- Proof steps: 934,
Interactions: 424
| 5-not-even(2,1) | eq-pos-01(1,0) | ls-add-02(1,0) | mod-neq(10,5) | mods-zero-07(1,0) | numeq(2,0) | numls-07(5,2) | pzero-gr(1,1) | square-zero(1,0) | zero-ge-03(2,1) |
| 7-not-even(2,1) | eq-same(3,2) | ls-add-03(1,0) | mod-nle(5,4) | modzero(2,1) | numeq-01(2,0) | numls-08(3,0) | pzero-ls(1,1) | square-zero-01(1,0) | zero-ge-add(5,3) |
| Mult-pred(0,0) | eq-same-01(1,0) | ls-dist(1,0) | mod-nls(3,1) | modzero-01(3,2) | numeq-02(2,0) | numls-09(3,0) | short-mult-max(7,5) | square-zero-02(2,2) | zero-ge-add-01(1,0) |
| Mult-succ(0,0) | eq-same-02(1,0) | ls-dist-01(1,0) | modeqp(10,3) | modzero-02(3,2) | numeq-03(2,0) | numls-10(2,0) | square-abs(1,1) | succ-lsplit(7,0) | zero-ge-add-02(2,1) |
| Mult-zero(0,0) | eq-same-03(1,0) | ls-dist-02(1,0) | modeqp-01(3,2) | modzero-03(3,2) | numeq-04(2,0) | numls-11(2,0) | square-eq(19,15) | succ-rmerge(1,0) | zero-ge-case(2,1) |
| abs-eqall(5,3) | eq-succ(1,0) | ls-dist-03(1,0) | modeqp-02(2,1) | modzero-04(3,2) | numle(3,0) | numls-12(3,0) | square-eq-01(6,3) | succ-rsplit(2,2) | zero-gr(6,3) |
| abs-eqneg(1,0) | eq-succ-01(2,2) | ls-dist-04(1,0) | modeqp-03(5,3) | modzero-05(3,2) | numle-01(3,0) | numls-13(3,0) | square-eq-02(3,3) | three(16,9) | zero-gr-01(2,1) |
| abs-ls(2,1) | est-nle(1,0) | ls-dist-05(1,0) | modeqp-copied(13,8) | modzero-06(3,2) | numle-02(3,0) | numlsneg(2,0) | square-even(8,4) | three-01(2,1) | zero-gr-02(2,1) |
| abs-ls-same(1,0) | ex-two(6,3) | ls-dist-06(1,0) | modeqp-neg(2,1) | modzero-07(1,0) | numle-03(3,0) | numlsneg-01(2,0) | square-ex(17,9) | two-eq(1,1) | zero-gr-03(2,1) |
| abs-ls-same-01(18,12) | exdivmod(27,13) | ls-forward(1,0) | modeqp-pos(2,1) | modzero-08(6,3) | numle-04(3,0) | numlsneg-02(2,0) | square-gez(1,0) | two-le(1,0) | zero-gr-add(2,1) |
| abs-not-neg(2,1) | exdivmodpos(4,3) | ls-neg(2,1) | modlep(6,3) | mult-add-greater(1,0) | numle-05(3,0) | numlsneg-03(2,0) | square-gez-01(2,1) | two-le-01(1,0) | zero-gr-add-01(1,0) |
| add-mult-two(1,0) | four(1,0) | ls-pos(11,3) | modlep-01(1,1) | mult-gt-both(6,3) | numle-06(3,0) | numsub(3,0) | square-gez-02(3,2) | two-le-02(1,0) | zero-gr-add-02(7,5) |
| associativity(10,4) | le-abs(2,1) | ls-pos-01(1,0) | modlep-02(1,1) | mult-gt-one(1,0) | numle-07(7,4) | numsucc(2,0) | square-inject(5,5) | two-le-03(1,0) | zero-gr-case(2,1) |
| auxexdivmod(19,13) | le-dist(1,0) | ls-pos-02(2,1) | modlep-03(9,3) | mult-pos(1,0) | numle-08(3,0) | odd-even(1,0) | square-interval(8,7) | two-le-04(1,0) | zero-le(2,1) |
| auxexdivmod-01(3,2) | le-dist-01(1,0) | ls-same(2,1) | modlep-04(7,4) | mult-pos-pos(1,0) | numle-09(3,0) | one(1,1) | square-le(4,3) | two-leone(1,0) | zero-le-01(3,1) |
| commutativity(6,2) | le-dist-02(1,0) | ls-same-01(1,0) | modlsp(3,2) | mult-sub-less(1,0) | numle-10(2,0) | one-01(1,0) | square-le-01(2,1) | two-ls(1,0) | zero-le-02(2,1) |
| dist-lsplit(1,0) | le-neg(7,4) | ls-same-02(2,1) | modlsp-01(1,1) | mult-sub-lesseq(1,0) | numle-11(2,0) | ple-neg(1,1) | square-le-02(5,3) | two-ls-01(1,0) | zero-le-03(2,1) |
| dist-rmerge(1,0) | le-neg-01(1,0) | ls-same-03(2,1) | modlsp-02(1,1) | neq-3-not-even(2,1) | numle-12(3,0) | ple-pos(1,1) | square-le-03(1,0) | two-ls-02(1,0) | zero-le-case(2,1) |
| dist-rsplit(9,4) | le-one(2,1) | ls-same-04(1,0) | modlsp-03(9,3) | neq-5-not-even(2,1) | numle-13(3,0) | ple-pos-better(3,2) | square-le-04(16,13) | two-ls-03(1,0) | zero-le-two(1,1) |
| dist-sub-merge(2,0) | le-pos(4,2) | ls-same-05(1,0) | modlsp-04(2,1) | neq-7-not-even(4,2) | numleneg(2,0) | pls-neg(3,2) | square-le-05(3,3) | two-ls-04(1,0) | zero-left(2,0) |
| dist-sub-split(2,0) | le-pos-01(1,0) | ls-same-06(2,0) | modlsp-05(2,1) | neq-9-not-even(2,1) | numleneg-01(2,0) | pls-pos(3,2) | square-le-06(7,4) | two-mone(1,0) | zero-ls(2,1) |
| eq-dist(1,0) | le-same(2,1) | ls-sub(2,0) | modlsp-06(2,1) | neq-not-zero(1,0) | numleneg-02(2,0) | pls-pos-01(1,0) | square-lez(2,1) | two-oddeq(3,2) | zero-ls-01(1,0) |
| eq-neg(2,1) | le-same-01(2,1) | ls-two(1,0) | modneqp(6,4) | neq-not-zero-01(1,0) | numleneg-03(2,0) | pls-pos-02(1,0) | square-lez-01(2,1) | two-pred(2,0) | zero-ls-02(2,1) |
| eq-nonzero(15,11) | le-same-02(2,1) | ls-two-01(1,0) | mods-eq(2,1) | neq-two(1,0) | numls(3,0) | pnle-neg(2,2) | square-ls(10,7) | two-sub(1,0) | zero-ls-03(4,2) |
| eq-nonzero-01(1,0) | le-same-03(2,1) | ls-two-02(1,0) | mods-ls(2,1) | noeth-ls-pos(1,1) | numls-01(3,0) | pnle-pos(4,3) | square-ls-01(1,0) | two-sub-01(1,0) | zero-ls-case(2,1) |
| eq-nonzero-02(1,0) | le-same-04(4,3) | ls-two-03(1,0) | mods-ls-01(2,1) | noeth-modlep(27,14) | numls-02(3,0) | pnls-neg(2,2) | square-ls-02(10,7) | two-zero(1,0) | zero-ls-sub(1,0) |
| eq-nonzero-03(1,0) | le-same-05(1,0) | minus-left(3,3) | mods-ls-02(2,1) | noeth-zero-ls(11,4) | numls-03(3,0) | pnls-negpos(2,1) | square-ls-03(3,3) | zero-eq(3,2) | zero-ls-two(1,0) |
| eq-one(21,13) | le-same-06(1,0) | minus-one(1,0) | mods-ls-03(2,1) | numabs(2,1) | numls-04(3,0) | pnls-pos(4,3) | square-ls-04(4,3) | zero-ge(2,1) | zero-neq(1,0) |
| eq-one-neg(7,5) | le-two(4,3) | minus-one-01(1,0) | mods-ls-04(4,2) | numabs-01(2,0) | numls-05(3,0) | pnls-posneg(2,1) | square-minus(1,0) | zero-ge-01(2,1) | zero-neq-01(1,0) |
| eq-pos(2,1) | ls-add(4,2) | minus-one-02(1,0) | mods-nls(4,2) | numdist(2,0) | numls-06(3,0) | pred-rmerge(2,0) | square-one-le(4,2) | zero-ge-02(2,1) |