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

Used simplifier rules/spec theorems by specification

Used from specification real-abs

real-abs/forward-lele is used by le-ceille, floor-le-int, int-le-floor,
real-abs/forward-lels is used by floor-triang, ceil-addint, le-floorle, int-ls-floor, int-le-floor,
real-abs/forward-lsle is used by floor-addint, le-floorle, ceil-triang,
real-abs/le-def is used by floor-notls, le-floorle, floor-le-int,
real-abs/le-num is used by floor-int, ceil-is-neg-floor-neg,
real-abs/lels is used by ceil-is-neg-floor-neg,
real-abs/ple is used by floor-triang, ceil-triang,
real-abs/ple-01 is used by ceil-is-neg-floor-neg,
real-abs/sub-def is used by ceil-triang,
real-abs/forward-lele is used by le-ceille,
real-abs/forward-lels is used by ceil-ls-int, le-ceille, ceil-le-int,
real-abs/forward-lsle is used by ceil-ls-int, ceil-le-int,
real-abs/le-def is used by ceil-is-neg-floor-neg, ls-notfloorgr, ls-ceille, floor-triang, ls-floorle, ls-notceilgr, ceil-ls-int, int-ls-floor, ceil-triang, int-le-floor, ceil-le-int,
real-abs/le-num is used by ceil-int, floor-addint, ceil-addint, le-floorle, le-ceille, floor-le-int, int-le-floor,
real-abs/lels is used by gr-ceilpred, floor-ls-int, ceil-is-neg-floor-neg, ls-floorsuc, floor-ls-negint, ceil-addint, ceil-ls-int, floor-le-int, ceil-triang, ceil-le-int,
real-abs/lels-03 is used by ceil-notls, floor-ls-int, ceil-is-neg-floor-neg, floor-ls-negint, ceil-addint, floor-le-int, ceil-triang, int-le-floor,
real-abs/lenls is used by gr-ceilpred, ceil-is-neg-floor-neg, ls-floorsuc, ceil-ls-int, le-ceille, ceil-le-int,
real-abs/lep-02 is used by le-ceille, floor-le-int,
real-abs/negle-07 is used by ceil-ls-negint, ceil-le-negint, ceil-is-neg-floor-neg,
real-abs/negle-13 is used by negint-le-floor,
real-abs/sub-le is used by negint-ls-floor,

Used from specification real-basic

real-basic/add-assoc is used by floor-addint,
real-basic/add-comm is used by floor-addint, ceil-addint,
real-basic/eqint-add is used by ceil-int, floor-addint, floor-int, ceil-is-neg-floor-neg, floor-triang, ceil-addint, ceil-ls-int, le-floorle, int-ls-floor, le-ceille, ceil-triang, int-le-floor, ceil-le-int,
real-basic/eqint-neg is used by negint-le-floor, ceil-ls-negint, ceil-is-neg-floor-neg, negint-le-ceil, floor-ls-negint, floor-le-negint, negint-ls-floor,
real-basic/eqint-sub is used by ceil-triang,
real-basic/less-add-cancel-l is used by floor-le-int,
real-basic/ls-num is used by floor-addint, floor-int, ceil-is-neg-floor-neg, int-ls-floor, floor-le-int,
real-basic/plst is used by floor-addint,
real-basic/add-assoc is used by ceil-ls-negint, gr-ceilpred, floor-addint, ceil-is-neg-floor-neg, ls-floorsuc, int-le-ceil, negint-le-ceil, ceil-addint, ceil-ls-int, int-ls-ceil, le-floorle, int-ls-floor, le-ceille, floor-le-int, ceil-triang, int-le-floor, ceil-le-int, floor-le-negint, negint-ls-floor,
real-basic/add-comm is used by ceil-ls-negint, gr-ceilpred, floor-addint, ceil-le-negint, ceil-is-neg-floor-neg, ls-floorsuc, int-le-ceil, negint-le-ceil, floor-ls-negint, ceil-addint, ceil-ls-int, int-ls-ceil, le-floorle, int-ls-floor, le-ceille, floor-le-int, ceil-triang, int-le-floor, ceil-le-int, floor-le-negint, negint-ls-floor,
real-basic/add-zero is used by gr-ceilpred, ceil-is-neg-floor-neg,
real-basic/bls-01 is used by ls-notfloorgr, ls-ceille, ls-floorle, ls-notceilgr,
real-basic/eqint-add is used by gr-ceilpred, ceil-is-neg-floor-neg,
real-basic/less-add-cancel-l is used by ls-floorsuc, ceil-addint, ceil-ls-int, int-ls-floor, le-ceille, ceil-le-int,
real-basic/ls-num is used by ceil-int, floor-triang, ceil-ls-int, int-ls-floor, ceil-triang, int-le-floor, ceil-le-int,
real-basic/neg-08 is used by int-ls-ceil,
real-basic/negl-ls is used by ceil-is-neg-floor-neg, negint-ls-ceil, negint-le-ceil,
real-basic/negladd-ls is used by ceil-is-neg-floor-neg, int-le-ceil, ceil-triang,
real-basic/negr-ls is used by floor-ls-negint,
real-basic/negradd-ls is used by floor-le-negint,
real-basic/sub-eq-01 is used by ceil-is-neg-floor-neg,

Used from specification int-basic2

int-basic2/add-a is used by ceil-int, ceil-ls-negint, gr-ceilpred, floor-addint, floor-int, ceil-le-negint, ceil-is-neg-floor-neg, int-le-ceil, negint-ls-ceil, negint-le-ceil, floor-ls-negint, floor-triang, ceil-addint, ceil-ls-int, int-ls-ceil, le-floorle, le-ceille, ceil-triang, int-le-floor, ceil-le-int,
int-basic2/add-c is used by ceil-int, ceil-ls-negint, gr-ceilpred, floor-addint, floor-int, ceil-le-negint, ceil-is-neg-floor-neg, int-le-ceil, negint-ls-ceil, negint-le-ceil, floor-ls-negint, floor-triang, ceil-addint, ceil-ls-int, int-ls-ceil, le-floorle, le-ceille, ceil-triang, int-le-floor, ceil-le-int, negint-ls-floor,
int-basic2/add-zero-rev is used by ceil-ls-negint, ceil-le-negint, negint-ls-ceil, negint-le-ceil,

Used from specification int-basic1

int-basic1/lst-01 is used by floor-addint, ceil-is-neg-floor-neg, ceil-addint,
int-basic1/irref is used by floor-addint,

Used from specification int-abs

int-abs/le-def is used by floor-ls-int,
int-abs/lels is used by ceil-is-neg-floor-neg, le-notceilgr,
int-abs/lenls is used by le-notfloorgr,
int-abs/ls-rew-succ is used by floor-addint, ceil-addint,
int-abs/neg-07 is used by floor-ls-negint,
int-abs/succ-02 is used by int-ls-floor,
int-abs/forward-le-01 is used by ceil-le-int,
int-abs/forward-le-02 is used by ceil-le-int,
int-abs/forward-le-04 is used by ceil-ls-int,
int-abs/forward-le-05 is used by ceil-ls-int,
int-abs/le-def is used by floor-triang, le-floorle, le-ceille, floor-le-int, ceil-triang, int-le-floor, ceil-le-int,
int-abs/lels is used by floor-addint, floor-ls-int, floor-ls-negint, ceil-addint, ceil-ls-int, le-floorle, int-ls-floor, le-ceille,
int-abs/lels-02 is used by ceil-int, floor-int,
int-abs/lels-03 is used by ceil-int, floor-addint, floor-int, ceil-is-neg-floor-neg, floor-triang, ceil-addint, ceil-ls-int, le-floorle, int-ls-floor, le-ceille, floor-le-int, ceil-le-int,
int-abs/lenls is used by ceil-ls-int, int-ls-floor, ceil-triang, int-le-floor, ceil-le-int,
int-abs/lsone is used by ceil-is-neg-floor-neg, ceil-ls-int,
int-abs/mone-06 is used by ceil-is-neg-floor-neg, ceil-le-int,
int-abs/neg-01 is used by ceil-ls-negint, negint-ls-ceil,
int-abs/neg-07 is used by int-ls-ceil, ceil-le-int,
int-abs/neg-13 is used by ceil-ls-int, ceil-le-int, negint-ls-floor,
int-abs/neg-15 is used by ceil-ls-negint, ceil-le-negint, negint-ls-ceil, negint-le-ceil, ceil-ls-int,
int-abs/negeq is used by ceil-is-neg-floor-neg,
int-abs/negle-07 is used by int-le-ceil, floor-le-negint,
int-abs/negle-13 is used by negint-le-floor, ceil-le-negint, negint-le-ceil, ceil-le-int,
int-abs/numls-02 is used by ceil-le-int,
int-abs/sub-le is used by ceil-le-negint,
int-abs/sub-le-01 is used by ceil-le-negint, negint-le-ceil,
int-abs/sub-ls is used by ceil-ls-negint, ceil-triang,
int-abs/sub-ls-01 is used by negint-ls-ceil, ceil-ls-int,
int-abs/succ-01 is used by floor-addint, ceil-addint, le-floorle, le-ceille,
int-abs/succ-02 is used by ceil-int, floor-int, floor-triang, ceil-triang, int-le-floor,
int-abs/zero-gels-01 is used by ceil-le-int,
int-abs/zero-gels-04 is used by ceil-ls-int, ceil-le-int,