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