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