[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 int-abs

Abs-neg(0,0)abs-add-zero(4,0)absneg-01(1,0)estimate-add2-ls-left(1,0)int-simp-10(2,1)ler(1,0)neg(1,0)numabsneg(2,0)ple-02(1,0)sub-shift(1,0)
Abs-pos(0,0)abs-le-succ(4,1)absneg-02(1,0)estimate-add2-ls-right(1,0)int-simp-11(1,0)les(1,0)neg-01(1,0)numabspos(2,0)ple-03(1,0)sub-shift-second(1,0)
Minus-def(0,0)abs-ls(1,0)absone(1,0)estimate-add2-lsle-left(1,0)k-sub-rec1(1,0)ls-rew-succ(1,0)neg-02(1,0)numadd(2,0)ple-04(1,0)sub-sub(1,0)
Sub-def(0,0)abs-ls-01(1,0)absone-01(4,1)estimate-add2-lsle-right(1,0)k-sub-rec2(1,0)lsone(1,0)neg-03(1,0)numadd-01(2,0)pls(1,0)sub-sub-01(1,0)
abs(1,0)abs-ls-02(4,0)absone-02(1,0)ex-le-add(2,1)le-add(1,0)lstwo(1,0)neg-04(1,0)numle-01(2,0)pls-01(1,0)sub-sub-02(1,0)
abs-01(1,0)abs-ls-03(2,0)absp(1,0)forward-le(1,0)le-add-01(4,2)lstwo-01(1,0)neg-05(1,0)numle-02(2,0)rew-eqzero(1,0)sub-sub-03(1,0)
abs-02(1,0)abs-ls-04(1,0)absp-01(1,0)forward-le-01(1,0)le-add-02(2,1)minus(1,0)neg-06(1,0)numle-03(2,0)rew-eqzero-01(1,0)sub-sub-04(1,0)
abs-03(1,0)abs-mone(1,0)abssub(1,0)forward-le-02(1,0)le-add-03(2,1)minus-01(1,0)neg-07(1,0)numlef(2,0)sub-add(1,1)sub-zero(1,0)
abs-04(1,0)abs-neg(5,0)abssub-01(1,0)forward-le-03(1,0)le-add-04(3,3)minus-02(1,0)neg-08(1,0)numlef-01(2,0)sub-add-01(1,0)sub-zero-01(1,0)
abs-05(1,0)abs-one(1,0)abssub-02(1,0)forward-le-04(1,0)le-add-05(4,4)minus-add(2,0)neg-09(1,0)numleledel(2,0)sub-add-02(1,0)subneg(1,0)
abs-06(2,0)abs-one-01(2,0)abssub-03(2,0)forward-le-05(1,0)le-add-06(4,4)minus-ass(1,0)neg-10(1,0)numleledel-01(2,0)sub-add-03(1,0)subsub(1,0)
abs-07(2,0)abs-sub(2,0)abssub-04(1,0)forward-lele(1,0)le-add-07(4,4)minus-five(1,0)neg-11(1,0)numlelsdel(2,0)sub-add-04(1,0)succ-01(1,0)
abs-08(1,0)abs-sub-01(9,2)abssub-05(5,1)forward-lels(1,0)le-add-08(2,2)minus-four(1,0)neg-12(1,0)numlelsdel-01(2,0)sub-add-05(1,0)succ-02(2,1)
abs-09(1,0)abs-sub-02(1,0)add-pos-ge(1,0)forward-lsle(1,0)le-def(0,0)minus-gr(1,0)neg-13(1,0)numls-01(2,0)sub-add-06(1,0)transrew(1,0)
abs-10(1,0)abs-succ(4,1)add-rew(1,0)ge(1,0)le-rec(1,0)minus-neg(2,0)neg-14(1,0)numls-02(2,0)sub-add-07(1,0)transrew-01(1,0)
abs-11(1,0)abs-two(1,0)add-shift(1,0)ge-def(0,0)le-rew-succ(1,0)minus-rew(1,0)neg-15(1,0)numls-03(2,0)sub-add-08(1,0)ttwo(1,0)
abs-12(1,0)abs-zero(1,0)anti(1,0)gr-def(0,0)le-sub-same(1,0)minus-sub(1,0)neg-add(1,0)numlsf(2,0)sub-add-09(1,0)zero-eq(1,0)
abs-14(1,0)absa(4,0)bet(1,0)int-add-pos(1,0)le-three(2,1)minus-three(1,0)neg-eq(1,0)numlsf-01(2,0)sub-eq(1,0)zero-ge(2,1)
abs-15(1,0)abseq(2,0)bet-01(1,0)int-add-pos-01(1,0)lels(1,0)mmone(1,0)negadd(1,0)numlsf-02(2,0)sub-eq-01(1,0)zero-ge-01(1,0)
abs-16(1,0)absle(1,0)discard-add2-lels-left(1,0)int-add-same-pos(1,0)lels-01(1,0)mone(1,0)negeq(1,0)numlsledel(2,0)sub-le(1,0)zero-gels(1,0)
abs-17(1,0)absle-01(1,0)elim-sub(2,1)int-simp-01(2,1)lels-02(1,0)mone-01(1,0)negle-07(1,0)numlsledel-01(2,0)sub-le-01(1,0)zero-gels-01(1,0)
abs-18(1,0)absls(2,0)estimate-add1-le-left(1,0)int-simp-02(1,0)lels-03(1,0)mone-02(1,0)negle-13(1,0)numlslsdel(2,0)sub-less(10,9)zero-gels-02(1,0)
abs-19(1,0)absls-01(2,0)estimate-add1-le-right(1,0)int-simp-03(2,1)lels-04(1,0)mone-03(1,0)negone(1,0)numlslsdel-01(2,0)sub-ls(1,0)zero-gels-03(1,0)
abs-21(6,0)absls-02(4,0)estimate-add1-ls-left(1,0)int-simp-04(2,1)lenls(1,0)mone-04(1,0)not-mone(3,2)numlslsdel-02(2,0)sub-ls-01(1,0)zero-gels-04(1,0)
abs-abs(1,0)absls-03(1,0)estimate-add1-ls-right(1,0)int-simp-05(1,0)leone(1,0)mone-05(1,0)not-mtwo(3,2)numlslsdel-03(2,0)sub-ls-02(1,0)zero-gs(2,1)
abs-abs-01(1,0)absls-04(1,0)estimate-add1-lsle-left(1,0)int-simp-06(5,3)lep(1,0)mone-06(1,0)notle-pos(2,1)numsub(2,0)sub-minus(1,0)zero-not(6,1)
abs-add(1,0)absls-05(2,0)estimate-add1-lsle-right(1,0)int-simp-07(1,0)lep-01(1,0)mone-07(2,1)num-between(2,0)one-03(2,1)sub-pred(1,0)zeroone(1,0)
abs-add-le-zero(4,0)absls-06(1,0)estimate-add2-le-left(1,0)int-simp-08(4,2)lep-02(1,0)mone-08(1,0)num-eq-shift(2,0)ple(1,0)sub-same(1,0)
abs-add-pos(6,1)absneg(1,0)estimate-add2-le-right(1,0)int-simp-09(1,0)lepr(1,0)mone-neg(1,0)num-subadd(2,0)ple-01(10,4)sub-same-01(1,0)