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