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