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

Abs-neg(0,0)abs-16(2,0)abs-sub(2,0)absneg-01(2,0)estimate-add1-ls-left(2,0)forward-le-04(2,0)le-lem(2,0)lenum-addboth2(5,1)notle-pos(2,0)transrew(2,0)
Abs-pos(0,0)abs-17(2,0)abs-two(2,0)absneg-02(2,0)estimate-add1-ls-right(2,0)forward-le-05(2,0)le-num(2,1)lep(2,0)ple(2,0)transrew-01(2,0)
abs(2,0)abs-18(2,0)abs-zero(2,0)absp(2,0)estimate-add1-lsle-left(2,0)forward-lele(2,0)lele-add-notgr(2,0)lep-01(2,0)ple-01(3,1)ttwo(2,0)
abs-01(2,0)abs-19(2,0)absa(5,0)absp-01(3,0)estimate-add1-lsle-right(2,0)forward-lels(2,0)lels(2,0)lep-02(2,0)ple-02(2,0)zero-eq(2,0)
abs-02(2,0)abs-21(7,0)abseq(3,0)abssub(2,0)estimate-add2-le-left(2,0)forward-lsle(2,0)lels-02(2,0)ler(2,0)ple-03(2,0)zero-ge(2,0)
abs-03(2,0)abs-add(2,0)absle(2,0)abssub-01(2,0)estimate-add2-le-right(2,0)ge-def(0,0)lels-03(2,0)lsle-add-noteq(2,0)ple-04(2,0)zero-ge-01(2,0)
abs-04(2,0)abs-le-succ(7,0)absle-01(2,0)abssub-02(2,0)estimate-add2-ls-left(2,0)gr-def(0,0)lels-add-noteq(3,1)lsle-add-notge(2,0)pls(2,0)zero-gels(2,0)
abs-06(3,0)abs-ls(2,0)absls(2,0)abssub-04(2,0)estimate-add2-ls-right(2,0)le-add(2,0)lels-add-notge(3,1)lsle-add-notgr(2,0)pls-01(2,0)zero-gels-01(2,0)
abs-07(3,0)abs-ls-01(2,0)absls-01(2,0)antr(2,0)estimate-add2-lsle-left(2,0)le-add-03(2,0)lels-add-notgr(3,1)lsls-add-notge(3,1)real-add-pos(2,0)zero-gels-02(2,0)
abs-09(2,0)abs-ls-02(3,0)absls-02(5,0)betweenlele-zero-one(2,0)estimate-add2-lsle-right(2,0)le-add-04(3,1)lenls(2,0)minus-gr(2,0)real-add-pos-01(2,0)zero-gels-03(2,0)
abs-10(2,0)abs-ls-03(2,0)absls-03(2,1)betweenlels-zero-one(2,0)ex-le-add(2,1)le-add-05(3,1)lenum-add1(5,1)mone-neg(2,0)real-add-same-pos(2,0)zero-gels-04(2,0)
abs-11(2,0)abs-ls-04(2,0)absls-04(2,1)betweenlsle-zero-one(2,0)forward-le(2,0)le-add-06(9,6)lenum-add2(5,1)negle-07(2,0)real-simp-11(2,0)zero-gs(2,0)
abs-12(2,0)abs-mone(2,0)absls-05(7,3)discard-add2-lels-left(2,0)forward-le-01(2,0)le-add-07(6,3)lenum-add3(5,1)negle-13(2,0)sub-def(0,0)zero-not(5,0)
abs-14(2,0)abs-neg(2,0)absls-06(2,0)estimate-add1-le-left(2,0)forward-le-02(2,0)le-add-08(6,3)lenum-add4(5,1)not-mone(2,0)sub-le(2,0)
abs-15(2,0)abs-one(2,0)absneg(2,0)estimate-add1-le-right(2,0)forward-le-03(2,0)le-def(0,0)lenum-addboth1(5,1)not-mtwo(4,2)sub-le-01(2,0)