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