[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 real-multdiv

abs-eqall(9,0)eq-same-03(2,0)invmult-gr-pos(2,1)le-same-04(7,3)ls-same-04(2,0)num-distr-add-eq1(4,1)pls-pos-01(2,0)square-le-03(2,0)twice-ls-zero(2,0)zero-ge-add-01(2,0)
abs-eqneg(2,0)eq-succ(2,0)invmult-gr-pos-add(2,1)le-same-05(3,1)ls-same-05(6,3)num-distr-add-eq2(4,1)pls-pos-02(2,0)square-le-04(10,7)two-def(0,0)zero-ge-add-02(9,6)
abs-ite(2,0)eq-succ-01(2,0)invmult-le-neg(6,5)le-same-06(2,0)ls-two(2,0)num-distr-add-le1(4,1)pnle-neg(3,1)square-le-05(4,3)two-eq(2,0)zero-ge-case(6,3)
abs-le-one-multiple(7,3)est-nle(2,0)invmult-le-neg-add(5,4)ls-add-02(2,0)ls-two-01(2,0)num-distr-add-le2(4,1)pnle-pos(3,1)square-le-05a(2,1)two-le(2,0)zero-gr(2,1)
abs-ls-multiple-one(7,0)inv-def(0,0)invmult-le-pos(6,5)ls-add-03(2,0)ls-two-02(2,0)num-distr-add-ls1(4,1)pnls-neg(3,1)square-le-one(2,1)two-le-01(2,0)zero-gr-01(6,3)
abs-ls-one-multiple(7,0)inv-eq(5,3)invmult-le-pos-add(5,4)ls-dist(2,0)ls-two-03(2,0)num-distr-add-ls2(4,1)pnls-negpos(4,2)square-lez(3,2)two-le-02(2,0)zero-gr-02(2,1)
abs-ls-same(6,0)inv-ge-neg(2,1)invmult-ls-neg(6,5)ls-dist-01(2,0)minus-left(4,2)num-distr-addboth-eq1(4,1)pnls-pos(4,2)square-lez-01(3,1)two-le-03(2,0)zero-gr-03(2,1)
abs-not-neg(7,0)inv-ge-pos(2,1)invmult-ls-neg-add(5,4)ls-dist-02(2,0)minus-one(4,2)num-distr-addboth-eq2(4,1)pnls-posneg(4,2)square-ls(3,2)two-le-04(2,0)zero-gr-add-01(2,0)
add-mult-two(3,2)inv-gr-neg(2,1)invmult-ls-pos(6,5)ls-dist-03(2,0)minus-one-01(2,0)num-distr-addboth-le1(4,1)posint-factor(3,1)square-ls-01(2,0)two-ls(2,0)zero-gr-case(5,3)
distr(0,0)inv-gr-pos(2,1)invmult-ls-pos-add(5,4)ls-dist-04(2,0)mods-ls(3,1)num-distr-addboth-le2(4,1)pzero-gr(2,1)square-ls-02(7,3)two-ls-01(2,0)zero-le(2,1)
div-def(0,0)inv-le-neg(6,5)le-abs(7,0)ls-dist-05(2,0)mods-zero-07(3,2)num-distr-addboth-ls1(4,1)pzero-ls(3,1)square-ls-03(3,2)two-ls-02(2,1)zero-le-01(4,2)
eq-dist(2,0)inv-le-pos(6,5)le-dist(2,0)ls-dist-06(2,0)mult-add-greater(2,0)num-distr-addboth-ls2(4,1)square-abs(3,0)square-ls-03a(2,1)two-ls-03(2,0)zero-le-02(2,1)
eq-neg(3,1)inv-ls-neg(6,5)le-dist-01(2,0)ls-forward(2,0)mult-ass(0,0)num-distr-eq1(4,1)square-eq(5,4)square-ls-04(4,2)two-ls-04(2,0)zero-le-03(2,1)
eq-neg-01(2,1)inv-ls-pos(6,5)le-dist-02(2,0)ls-neg(6,3)mult-com(0,0)num-distr-eq2(4,1)square-eq-01(7,3)square-ls-04a(2,1)two-sub(3,2)zero-le-case(6,3)
eq-nonzero(6,3)inv-mult(4,2)le-neg(11,9)ls-neg-01(2,1)mult-gt-both(2,1)num-distr-le1(4,1)square-eq-02(5,2)square-ls-one(4,1)two-sub-01(2,0)zero-ls(2,1)
eq-nonzero-01(2,0)inv-mult-add-eq(2,0)le-neg-01(2,0)ls-negint(2,1)mult-gt-one(2,0)num-distr-le2(4,1)square-eq-03(3,1)square-minus(2,0)two-sub-02(2,1)zero-ls-01(2,0)
eq-nonzero-02(2,0)inv-twice(2,1)le-negint(2,1)ls-pos(4,3)mult-one(0,0)num-distr-ls1(5,1)square-eq-one(6,1)square-zero(2,1)two-sub-03(2,1)zero-ls-02(2,1)
eq-nonzero-03(2,0)invmult-eq(2,1)le-pos(9,7)ls-pos-01(2,0)mult-pos(2,1)num-distr-ls2(4,1)square-ge-one(6,1)square-zero-01(3,2)two-sub-04(2,1)zero-ls-03(4,2)
eq-nonzero-int(3,1)invmult-ge-neg(2,1)le-pos-01(2,0)ls-pos-02(3,0)mult-pos-pos(2,0)order(0,0)square-gez(2,0)square-zero-01a(2,1)two-sub-05(2,1)zero-ls-case(5,3)
eq-pos(3,1)invmult-ge-neg-add(2,1)le-posint(3,1)ls-posint(3,1)mult-zero(3,2)ple-neg(3,1)square-gez-01(3,1)square-zero-02(2,1)zero-eq(5,3)zero-neq(3,1)
eq-pos-01(2,0)invmult-ge-pos(2,1)le-same(6,5)ls-same(2,1)neq-not-zero(2,0)ple-pos(4,2)square-gr-one(4,1)succ-lsplit(2,0)zero-ge(2,1)zero-neq-01(9,5)
eq-same(3,2)invmult-ge-pos-add(2,1)le-same-01(4,2)ls-same-01(3,1)neq-not-zero-01(2,0)ple-pos-better(2,1)square-interval(10,5)succ-rmerge(2,0)zero-ge-01(2,1)
eq-same-01(2,0)invmult-gr-neg(2,1)le-same-02(4,2)ls-same-02(2,1)noeth-zero-ls(2,0)pls-neg(2,1)square-interval-01(9,6)succ-rsplit(2,0)zero-ge-02(2,1)
eq-same-02(2,0)invmult-gr-neg-add(2,1)le-same-03(2,1)ls-same-03(2,1)num-distr(2,1)pls-pos(2,1)square-le(72,44)twice-le-zero(2,1)zero-ge-03(2,1)