[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-pot
- Status: Proved!
- Axioms: 3,
User Theorems: 159
(Proved: 159,
Partially proved: 0,
Unproved: 0,
Invalid: 0,
Siginvalid: 0)
- Proof steps: 852,
Interactions: 453
| 2pot-leone(1,0) | divmod2-2pot(2,0) | le-2pot(10,5) | ls-pos-2pot-01(1,1) | mod-same(2,1) | odd-square(3,2) | pot-pot-03(2,1) | pot2-est-mult8(14,8) | sqrt-10pot(4,3) | two-zero-01(1,0) |
| Pot-neg(0,0) | divmod2-2pot-neg(14,9) | le-2pot-01(10,5) | ls-same(4,1) | mod-two-ge(1,0) | one(1,1) | pot-root-est(33,31) | pot2-le-pred(6,3) | square-mod-four(1,0) | twolezero(1,0) |
| Pot-pos(0,0) | eq-one(4,3) | le-2pot-succ(10,3) | minus-odd(6,3) | mod-two-ge-01(14,5) | one-01(7,4) | pot-square(1,0) | pot2-le-pred-01(1,0) | square-nls(4,3) | twopot-mone-div(13,7) |
| Pot-zero(0,0) | eq-pos(13,5) | le-pos(29,14) | minus-one-even(4,2) | mod-two-ls(2,1) | one-02(5,2) | pot-square-01(1,0) | pot2-ls-pred(2,1) | succ(2,1) | twotwo(1,0) |
| abs-2pot(1,1) | eq-two(1,0) | le-pos-01(10,4) | minus-one-odd(6,3) | mod-two-ls-01(1,1) | one-03(1,0) | pot-square-02(4,2) | pot2-ls-pred-01(6,3) | two-le(1,0) | zero(6,3) |
| add-eq2pot(13,6) | eq2(6,3) | le-same(2,0) | minus-square(3,2) | mod2-2pot(6,3) | pot-add-min(8,5) | pot-square-03(1,0) | pot2-mod2-zero(2,1) | two-le-01(1,1) | zero-01(1,0) |
| add-eq2pot-01(6,2) | eqone(1,0) | lemon2pot(1,0) | minus-square-01(1,1) | mod2-2pot-01(10,4) | pot-dist-pos(11,4) | pot-square-04(1,0) | pot2-pos(1,0) | two-leone(2,1) | zero-02(2,1) |
| div-div-rec(44,35) | eqone-01(1,0) | lemon2pot-01(1,1) | mod-2pot(1,0) | mod2-2pot-02(5,2) | pot-div(4,1) | pot-square-05(2,1) | pot2-pos-01(2,1) | two-lez(1,0) | zero-03(1,0) |
| div-div-rec-01(1,1) | eqone-02(1,1) | lemon2pot-02(1,1) | mod-add1-negneg(2,1) | mod2-2pot-03(1,0) | pot-div3-nls(11,4) | pot-square-est(2,1) | pot2-pos-02(2,1) | two-lez-01(1,0) | zerozero(1,0) |
| div-twopot(6,2) | equal-minus-one(44,25) | ls-2pot(2,1) | mod-add1-pospos(2,1) | mod2-2pot-04(5,2) | pot-eq-sub(2,1) | pot-square-est-01(16,10) | pot2-pos-03(2,1) | two-ls(2,1) |
| div2(3,1) | even-square(3,2) | ls-2pot-01(2,1) | mod-lesame(2,1) | mod2-2pot-05(1,0) | pot-lez(1,0) | pot-square-est-02(23,16) | pot2-pos-04(2,1) | two-lsz(1,0) |
| div2-2pot(2,1) | exin2pot(25,13) | ls-mult-2pot(9,4) | mod-lez(1,0) | mod2-2pot-06(2,1) | pot-mod-add-zero(14,7) | pot-square-est-div6(9,8) | pot2-pos-05(1,0) | two-minus(2,1) |
| div2-2pot-01(2,1) | exin2pot-neg(8,4) | ls-pos(10,6) | mod-lsz(2,1) | mod2-pos(1,0) | pot-mod-zero(4,3) | pot-sub-dist(8,3) | pot2-suble(2,1) | two-minus-01(1,1) |
| div2-2pot-02(2,0) | exinpot(9,5) | ls-pos-01(1,0) | mod-next-square(2,2) | notneg(6,3) | pot-nls(3,2) | pot-zero-01(6,3) | pot2-subls(2,1) | two-mod(1,0) |
| div2-2pot-03(6,2) | geom-mod(26,21) | ls-pos-02(10,4) | mod-ngez(2,1) | notneg-01(4,2) | pot-pot(2,1) | pot2-add(1,0) | pot2-succ(1,0) | two-mod-01(3,2) |
| div2-2pot-04(1,1) | grz(2,1) | ls-pos-03(4,2) | mod-ngez-01(2,1) | notneg-02(4,2) | pot-pot-01(1,0) | pot2-div2(2,0) | pot2-succ-01(1,1) | two-mone(1,0) |
| div2-2pot-neg(6,5) | isSquare-10pot(3,3) | ls-pos-2pot(1,0) | mod-pot-shift-pos(19,9) | notone(7,3) | pot-pot-02(10,5) | pot2-est-div6(45,23) | pred-le(2,0) | two-zero(1,0) |