[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-mult

addle(2,0)coef-21(2,2)le-rew(1,0)lssucc-01(1,0)mult-eq-succ-01(3,1)numeral-04(3,0)numeral-29(2,0)sqr-05(2,0)square-ls-04(11,7)twoeqf(3,1)
addle-01(5,0)coef-22(1,1)le-same(10,5)mod-ls(2,0)mult-eq-succ-02(2,1)numeral-05(3,0)numeral-30(3,0)sqr-06(1,1)square-ls-05(10,7)twoeqf-01(3,1)
coef-01(1,1)coef-23(2,2)le-succ(6,3)mod-neq(2,1)mult-ineq-le(2,0)numeral-06(3,0)numeral-32(3,0)sqr-07(2,1)square-one(3,1)twoeqf-02(3,0)
coef-02(3,3)dist(3,0)le2-02(2,1)mod-neq-01(2,1)mult-ineq-lt(2,0)numeral-07(2,0)numeral-33(2,0)sqr-08(1,1)square-two(8,5)twoeqf-03(3,1)
coef-03(3,3)dist-merge(1,0)le2-03(1,0)mod-neq-02(5,2)mult-le(1,0)numeral-08(3,0)numeral-35(3,0)sqr-09(3,0)sqzero(1,0)twole(1,0)
coef-04(1,1)dist-sub(3,0)le2-04(4,2)mod-neq-03(7,3)mult-le-01(8,5)numeral-09(3,0)numeral-36(3,0)square-eq(4,4)succ(2,0)twole-01(1,0)
coef-05(5,5)dist-sub-01(3,0)leone(7,1)mod-neq-04(2,0)mult-rec(0,0)numeral-10(7,2)one(1,0)square-eq-01(1,1)succ-01(3,1)twole-02(1,0)
coef-06(4,4)dist-sub-02(3,0)ls(2,2)mod-neq-05(2,1)mult-sub-less(2,0)numeral-11(3,0)one-01(2,1)square-eq-02(1,1)succ-merge(1,0)twols(2,0)
coef-07(4,4)dist-sub-03(3,0)ls-01(4,0)mod-nle(13,8)neqone(2,0)numeral-12(5,1)one-02(2,0)square-eq-03(4,4)three(17,11)twols-01(2,0)
coef-08(4,4)dist-sub-04(3,0)ls-02(4,2)mod-nle-01(3,1)nonumsimp-addls-01(1,0)numeral-15(3,0)rdist(4,1)square-even(9,4)threeeq(3,0)zero(1,0)
coef-09(1,1)eq(7,2)ls-03(2,0)mod-nls(4,2)nonumsimp-eqsucc(1,0)numeral-16(3,0)rsucc(1,0)square-even-01(3,1)threels(2,0)zero-01(1,0)
coef-10(2,2)eq-01(2,1)ls-03-num(2,0)modeq(8,3)nonumsimp-lstwo(1,0)numeral-17(7,2)rsucc-01(3,0)square-inject(3,2)two-02(1,0)zero-02(1,0)
coef-11(2,2)ex-two(9,2)ls-04(3,1)modeq-01(2,0)nonumsimp-mod-neq(2,0)numeral-18(3,0)rsucc-02(1,1)square-interval(6,5)two-03(6,3)zero-03(1,0)
coef-12(2,2)four(2,0)ls-05(2,0)modls(11,5)nonumsimp-mod-neq-05(9,4)numeral-19(3,0)sqle(3,1)square-le(2,2)two-les-01(1,0)zero-04(2,0)
coef-13(2,2)four-01(3,0)ls-06(3,1)modls-01(2,1)nonumsimp-succ(1,0)numeral-20(3,0)sqle-01(2,0)square-le-01(2,2)two-ls-01(1,0)zero-05(1,0)
coef-14(1,1)le(7,3)ls-07(3,1)modls-02(2,1)nonumsimp-twoeq(1,0)numeral-21(3,0)sqle-02(2,0)square-le-02(5,3)two-one-01(2,0)zero-06(2,0)
coef-15(2,2)le-01(2,0)ls-08(4,2)modls-03(7,2)nonumsimp-twoeq-01(1,0)numeral-23(3,0)sqls(5,2)square-le-03(3,3)two-succ-03(1,0)zero-num(2,0)
coef-16(1,1)le-02(2,0)ls-09(2,0)modp(6,2)nonumsimp-twole(1,0)numeral-24(3,0)sqp(3,0)square-less(4,3)two-succ-04(2,0)
coef-17(1,1)le-03(4,4)ls-10(2,0)mult-a(6,2)nonumsimp-twols(1,0)numeral-25(3,0)sqr(1,0)square-ls(16,10)two-succ-05(2,1)
coef-18(2,2)le-04(5,2)ls2-02(1,0)mult-base(0,0)nonumsimp-twonle(3,1)numeral-26(3,0)sqr-01(1,1)square-ls-01(2,1)two-succ-06(5,0)
coef-19(2,2)le-05(2,0)ls2-03(1,0)mult-c(3,0)numeral-01(2,0)numeral-27(3,0)sqr-02(1,0)square-ls-02(2,2)two-zero-01(1,0)
coef-20(2,2)le-num(2,0)lssucc(1,0)mult-eq-succ(4,2)numeral-03(3,0)numeral-28(3,0)sqr-03(1,1)square-ls-03(1,1)twoeq(1,0)