[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 nat-div
- Status: Proved!
- Axioms: 2,
User Theorems: 139
(Proved: 139,
Partially proved: 0,
Unproved: 0,
Invalid: 0,
Siginvalid: 0)
- Proof steps: 383,
Interactions: 154
| Divdef(0,0) | exmult(2,1) | mod-eq-02(2,1) | mod-nls(1,0) | mod-zero-01(2,1) | one-01(1,1) | square-nle-01-01(1,1) | two-loup-07(6,2) | two-neq(2,0) | two-twosucc-02(1,0) |
| Moddef(0,0) | le(1,0) | mod-le(1,0) | mod-once(4,2) | mod2-succ(2,1) | rax(3,1) | square-nls(4,2) | two-loup-08(4,1) | two-neq-01(2,0) | two-zero(1,0) |
| add(2,1) | le-01(4,2) | mod-le-01(1,0) | mod-one(1,1) | modex(2,0) | rec(2,0) | two-eq(3,0) | two-loup-09(4,1) | two-neq-02(2,0) | two-zero-01(1,0) |
| cond(2,1) | le-div-to-mult(12,6) | mod-le-02(1,0) | mod-one-01(2,1) | mult(5,2) | square-even(2,1) | two-le(1,0) | two-loup-10(2,0) | two-odd(1,0) | two-zero-01-01(4,1) |
| cond-01(2,1) | le-succ(4,0) | mod-le-03(6,4) | mod-rec(2,0) | mult-01(1,0) | square-even-01(1,1) | two-le-01(1,0) | two-loup-11(4,1) | two-odd-01(1,1) | zero(2,1) |
| div-add(2,1) | ls(4,0) | mod-le-04(1,0) | mod-rew(4,1) | mult-02(1,0) | square-even-02(1,1) | two-le-02(1,0) | two-loup-12(8,3) | two-one(1,0) | zero-01(2,1) |
| div-elim(2,1) | ls-01(4,0) | mod-ls(1,0) | mod-same(2,1) | mult-div(2,1) | square-even-03(1,1) | two-le-03(2,1) | two-loup-13(4,1) | two-one-01(1,0) |
| div-le(1,0) | ls-02(4,2) | mod-ls-01(2,0) | mod-succ(2,0) | mult-ls(2,1) | square-inj(3,3) | two-le-04(1,0) | two-ls(2,0) | two-padd(1,0) |
| div-le-01(2,0) | ls-03(8,5) | mod-ls-02(2,0) | mod-succ-01(2,0) | mult-ls-01(2,1) | square-inject(6,6) | two-loup(4,1) | two-ls-01(1,0) | two-peq(3,1) |
| div-mult(2,1) | ls-even(1,0) | mod-ls-03(2,0) | mod-succ-02(2,2) | nummult-eq(2,0) | square-interval(10,10) | two-loup-01(1,0) | two-ls-02(2,0) | two-ppred(6,2) |
| div-one(1,1) | ls-succ(1,1) | mod-mod(4,2) | mod-succ-03(1,0) | nummult-le-01(2,0) | square-ls(1,1) | two-loup-02(6,2) | two-ls-03(1,0) | two-rec(1,0) |
| div-succ(7,5) | mod-add(4,2) | mod-mod-01(4,2) | mod-succ-04(6,0) | nummult-le-03(2,0) | square-ls-01(1,1) | two-loup-03(1,0) | two-ls-04(2,1) | two-succ(1,0) |
| div-succ-01(1,1) | mod-by6(23,12) | mod-mult(7,2) | mod-succ-05(1,0) | nummult-ls-01(2,0) | square-ls-02(2,2) | two-loup-04(8,2) | two-ls-05(2,1) | two-three(1,1) |
| div-two-add(1,0) | mod-eq(2,1) | mod-mult-01(1,1) | mod-succ-06(1,1) | nummult-ls-03(2,0) | square-ls-03(10,9) | two-loup-05(4,1) | two-mdiv2-02(1,0) | two-two-01(1,1) |
| div-two-mult(6,2) | mod-eq-01(5,3) | mod-neq(1,0) | mod-zero(2,1) | one(2,1) | square-nle-01(7,5) | two-loup-06(4,1) | two-mdiv2-03(1,0) | two-two-02(1,0) |