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

decimal/dec2int-def is used by dec2int-not-neg,
decimal/equality-any is used by mult-eq-same,
decimal/getint-neg is used by sub-def-any,
decimal/getint-neg-01 is used by ls-zero, getint-abs,
decimal/intvalue-base is used by sub-def-any, square-sqrt, square-isSquare, neg-any-def, mult-one, mult-def-any, add-def-any, abs-any-def,
decimal/intvalue-mod-10 is used by add-scale-neq,
decimal/intvalue-rec is used by square-sqrt, square-isSquare,
decimal/maxScale-base is used by add-scale-neq,
decimal/maxScale-pot10-02 is used by add-scale-neq,
decimal/maxScale-pot10-add is used by add-scale-neq,
decimal/maxScale-pot10-nls is used by add-scale-eq,
decimal/mkDecimal-constructor is used by sub-zero, scale-abs, getint-abs,
decimal/mkDecimal-enlarge is used by sub-same, sub-def-any, sub-add, mult-dist, ls-add-01, ls-add, less-trans, less-totality, add-same, add-def-any,
decimal/mkDecimal-maxScale-le-scale is used by add-scale-neq, add-scale-eq,
decimal/mkDecimal-maxScale-nle-scale is used by add-scale-neq, add-scale-eq,
decimal/mkDecimal-negated is used by sub-def-any,
decimal/mkDecimal-rec is used by sub-def-any, square-sqrt, neg-any-def, mult-def-any, add-def-any, abs-any-def,
decimal/mkDecimal-scale-not-neg is used by sub-add, square-sqrt-02, square-sqrt, neg-any-def, ls-add-01, ls-add, less-trans, less-totality, add-same, abs-any-def,
decimal/mkDecimal-selectors is used by square-sqrt-02, mult-one, add-zero-01, add-zero,
decimal/mkDecimal-zero is used by sub-id, sub-def-any, neg-any-def, mult-zero, mult-eq-same, mult-def-any, ls-add-02, abs-any-def,
decimal/scale-base is used by sub-def-any, square-sqrt, square-scale, neg-any-def, mult-one, mult-def-any, add-def-any, abs-any-def,
decimal/scale-rec is used by square-sqrt, square-scale,
decimal/eq-same is used by sub-same, sub-def-any, sub-add, square-sqrt-02, square-sqrt, neg-any-def, mult-dist, mult-abs, less-totality, abs-pos, abs-any-def,
decimal/eq-zero is used by square-sqrt, square-pos-01, neg-any-def, mult-zero-01, abs-any-def,
decimal/getint-neg-02 is used by square-int-nlz, less-same, less-def-any, le-zero,
decimal/getint-pos is used by ls-zero,
decimal/intvalue-zero is used by sub-zero, sub-def-any, neg-any-def, mult-zero-01, mult-zero, mult-def-any, less-irref, add-zero-01, add-zero, abs-any-def,
decimal/maxScale-zero is used by add-scale-neq,
decimal/scale-negate is used by scale-abs,
decimal/scale-not-neg is used by dec2int-not-neg, add-scale-neq, add-scale-eq,
decimal/scale-zero is used by sub-zero, sub-def-any, square-sqrt, neg-any-def, mult-zero-01, mult-zero, mult-def-any, add-zero-01, add-zero, abs-any-def,

Used from specification int-basic1

int-basic1/forward-pos is used by add-scale-neq,
int-basic1/ls-01 is used by square-sqrt, less-trans, less-totality, add-scale-neq,
int-basic1/lst-01 is used by add-scale-neq,

Used from specification int-mult

int-mult/dist-lsplit is used by sub-add, add-scale-eq, add-same, add-a,
int-mult/dist-sub-split is used by sub-same, sub-def-any, square-sqrt, square-scale, square-isSquare, ls-add-01, ls-add,
int-mult/eq-nonzero is used by mult-eq-same,
int-mult/Mult-zero is used by sub-zero, sub-def-any, mult-zero-01, mult-zero, mult-eq-same, mult-def-any, ls-zero-01, ls-zero, add-zero-01, add-zero, add-scale-neq, add-def-any,
int-mult/abs-eqall is used by square-sqrt-02, square-sqrt, square-scale, square-ls, square-isSquare, mult-def-any, mult-abs, add-scale-eq, add-def-any, abs-any-def,
int-mult/add-mult-two is used by sub-same, sub-id, sub-add, square-sqrt-02, square-sqrt, square-scale, square-pos-01, square-pos, square-ls, square-isSquare, square-int-nlz, square-abs, mult-dist, add-scale-eq, add-same,
int-mult/associativity is used by sub-zero, sub-def-any, sub-add, square-sqrt-02, square-sqrt, square-scale, square-pos-01, square-pos, square-ls, square-isSquare, square-int-nlz, square-abs, mult-zero-01, mult-zero, mult-pos-02, mult-one, mult-ls, mult-eq-same, mult-dist, mult-def-any, mult-abs, mult-a, ls-zero-01, ls-zero, add-zero-01, add-zero, add-scale-neq, add-scale-eq, add-def-any, add-a, abs-any-def,
int-mult/commutativity is used by sub-zero, sub-def-any, sub-add, square-sqrt-02, square-sqrt, square-scale, square-pos-01, square-pos, square-ls, square-isSquare, square-int-nlz, square-abs, mult-zero-01, mult-zero, mult-pos-02, mult-one, mult-ls, mult-eq-same, mult-dist, mult-def-any, mult-c, mult-abs, mult-a, ls-zero-01, ls-zero, add-zero-01, add-zero, add-scale-neq, add-scale-eq, add-def-any, add-a, abs-any-def,
int-mult/eq-dist is used by mult-dist, add-def-any,
int-mult/eq-nonzero is used by sub-def-any, sub-add, mult-eq-same, mult-dist,
int-mult/eq-pos is used by sub-def-any,
int-mult/le-same is used by square-sqrt,
int-mult/le-same-04 is used by square-scale, square-isSquare, mult-def-any, add-def-any,
int-mult/ls-pos is used by mult-ls,
int-mult/minus-left is used by sub-def-any, square-ls,
int-mult/neq-not-zero is used by sub-def-any, sub-add, mult-dist,
int-mult/neq-two is used by square-sqrt, square-scale, square-isSquare,
int-mult/numls-08 is used by add-scale-eq,
int-mult/one is used by sub-zero, sub-def-any, square-sqrt-02, square-sqrt, square-scale, square-isSquare, mult-one, mult-def-any, ls-zero-01, ls-zero, add-zero-01, add-zero, add-scale-neq, add-scale-eq, add-def-any, abs-any-def,
int-mult/square-eq is used by square-sqrt-02,
int-mult/square-gez is used by square-pos, square-abs,
int-mult/square-lez is used by square-int-nlz,
int-mult/square-lez-01 is used by square-pos-01,
int-mult/square-ls is used by square-ls,
int-mult/square-zero is used by square-sqrt, square-scale, square-isSquare,
int-mult/two-zero is used by square-sqrt, square-scale, square-isSquare,
int-mult/zero-eq is used by square-sqrt, square-scale, square-isSquare, mult-dist,
int-mult/zero-ge is used by sub-add,
int-mult/zero-gr is used by square-sqrt,
int-mult/zero-ls-02 is used by mult-pos-02,
int-mult/zero-neq-01 is used by square-sqrt, square-scale, square-isSquare,

Used from specification int-gcd

int-gcd/mod-square-10 is used by square-sqrt, square-scale, square-isSquare,

Used from specification int-square

int-square/inverse-ii is used by square-sqrt-02, square-sqrt,
int-square/isSquare-def is used by square-sqrt-02,
int-square/isSquare-square is used by square-isSquare,
int-square/zero-01 is used by square-sqrt,

Used from specification int-pot

int-pot/Pot-pos is used by sub-def-any, add-scale-neq, add-def-any,
int-pot/pot-add-min is used by add-scale-neq,
int-pot/pot-dist-pos is used by sub-add, mult-ls, mult-eq-same, mult-dist, add-a,
int-pot/pot-mod-add-zero is used by add-scale-neq,
int-pot/grz is used by dec2int-not-neg,
int-pot/notneg-02 is used by square-ls,
int-pot/pot-zero-01 is used by mult-eq-same,

Used from specification int-abs

int-abs/Abs-pos is used by sub-def-any, square-sqrt-01, square-sqrt, square-scale, square-ls, square-isSquare, scale-abs, getint-abs, add-scale-eq,
int-abs/add-shift is used by add-scale-neq,
int-abs/lels-02 is used by sub-def-any,
int-abs/Sub-def is used by sub-def-any,
int-abs/abs-01 is used by sub-add, square-sqrt-02, square-sqrt, square-scale, square-ls, square-isSquare, ls-add-01, ls-add, less-trans, less-totality, add-same,
int-abs/abs-03 is used by sub-same, sub-def-any, sub-add, square-ls, mult-ls, mult-eq-same, mult-dist, ls-add-01, ls-add, less-totality, add-same, add-a, abs-not-neg,
int-abs/abs-06 is used by sub-def-any, add-def-any,
int-abs/abs-07 is used by square-sqrt, square-scale, square-isSquare,
int-abs/abs-08 is used by sub-def-any, square-sqrt-01, square-sqrt, square-ls, scale-abs, getint-abs, abs-neg,
int-abs/abs-12 is used by add-scale-neq,
int-abs/abs-16 is used by square-sqrt,
int-abs/abs-abs is used by sub-def-any, square-sqrt, square-scale, square-isSquare, mult-def-any, add-def-any,
int-abs/abs-abs-01 is used by sub-add, mult-ls, mult-eq-same, mult-dist, mult-def-any, mult-a, add-def-any, add-a,
int-abs/abs-add-pos is used by sub-def-any, less-trans,
int-abs/abs-add-zero is used by sub-def-any, mult-def-any, add-def-any,
int-abs/abs-zero is used by sub-def-any, square-sqrt, square-scale, square-isSquare,
int-abs/absle is used by add-scale-neq, abs-pos,
int-abs/absls is used by mult-eq-same,
int-abs/forward-le-01 is used by square-sqrt-01, square-sqrt, scale-abs, mult-pos-02, less-trans, getint-abs, add-scale-neq, abs-pos,
int-abs/forward-le-02 is used by square-int-nlz, scale-abs, getint-abs, dec2int-not-neg, add-scale-neq, abs-neg,
int-abs/forward-le-04 is used by sub-def-any, add-scale-neq,
int-abs/forward-le-05 is used by sub-def-any, square-sqrt, mult-ls, dec2int-not-neg, add-scale-neq,
int-abs/forward-lels is used by less-trans, add-scale-neq,
int-abs/forward-lsle is used by less-trans, add-scale-neq,
int-abs/le-add is used by add-scale-neq,
int-abs/lels is used by sub-def-any, square-sqrt-01, square-sqrt, square-scale, square-pos-01, square-ls, square-isSquare, scale-abs, neg-any-def, mult-def-any, less-trans, less-totality, getint-abs, add-scale-neq, add-def-any, abs-any-def,
int-abs/lels-01 is used by sub-def-any, square-sqrt, less-trans, le-zero, le-same, le-pos, dec2int-not-neg, add-scale-neq, add-scale-eq,
int-abs/lels-02 is used by square-sqrt, less-totality, add-scale-neq,
int-abs/lels-03 is used by dec2int-not-neg, add-scale-neq,
int-abs/lenls is used by mult-pos-02, le-zero, le-same, le-pos, add-scale-eq,
int-abs/leone is used by add-def-any,
int-abs/lsone is used by sub-def-any, square-sqrt, square-scale, square-isSquare,
int-abs/minus-02 is used by sub-def-any, square-sqrt,
int-abs/neg-05 is used by ls-zero,
int-abs/neg-06 is used by sub-def-any, square-sqrt, ls-zero, add-scale-neq,
int-abs/neg-07 is used by square-ls,
int-abs/neg-10 is used by neg-any-def, add-scale-neq,
int-abs/neg-13 is used by square-ls,
int-abs/neg-15 is used by sub-def-any, square-sqrt, getint-abs, add-scale-neq,
int-abs/negeq is used by getint-abs,
int-abs/num-subadd is used by square-sqrt,
int-abs/sub-add-01 is used by sub-def-any, mult-def-any, add-def-any,
int-abs/sub-eq is used by sub-def-any, sub-add, square-sqrt, square-scale, square-isSquare, getint-abs, add-scale-neq,
int-abs/sub-le-01 is used by add-def-any,
int-abs/sub-ls is used by sub-def-any, square-sqrt, square-scale, square-isSquare, ls-add-01, less-same, less-def-any,
int-abs/sub-ls-01 is used by ls-add, add-scale-neq, add-scale-eq,
int-abs/sub-pred is used by sub-def-any, add-scale-neq, add-def-any,
int-abs/sub-sub is used by square-sqrt, square-scale, square-isSquare, add-scale-neq,
int-abs/sub-sub-03 is used by sub-id, ls-add-02, add-scale-neq,
int-abs/sub-zero-01 is used by sub-zero, sub-def-any,
int-abs/zero-gels-01 is used by ls-zero-01, add-scale-neq,
int-abs/zero-gels-04 is used by add-scale-neq,
int-abs/zero-gs is used by add-scale-neq,

Used from specification int-min

int-min/Min-right is used by add-scale-neq,
int-min/even-def-mod is used by square-scale-01,
int-min/Max-left is used by add-scale-neq,
int-min/Max-right is used by add-scale-neq,
int-min/Min-left is used by add-scale-neq,
int-min/even-2 is used by square-scale,
int-min/even-mult is used by square-scale,
int-min/max-a is used by add-scale-neq,
int-min/max-c is used by add-scale-neq,
int-min/min-a is used by add-scale-neq,
int-min/min-c is used by add-scale-neq,

Used from specification nat-basic2

nat-basic2/a is used by sub-def-any, mult-def-any, add-def-any,
nat-basic2/c is used by sub-def-any, mult-def-any, add-def-any,
nat-basic2/l is used by sub-def-any, mult-def-any, add-def-any,

Used from specification intnat

intnat/labs is used by sub-def-any, square-sqrt, square-scale, square-isSquare, neg-any-def, mult-def-any, add-def-any, abs-any-def,

Used from specification int-basic2

int-basic2/add-c is used by add-scale-neq,
int-basic2/add-a is used by sub-zero, sub-same, sub-id, sub-def-any, sub-add, square-sqrt-02, square-sqrt, square-scale, square-pos-01, square-pos, square-ls, square-isSquare, square-int-nlz, square-abs, mult-zero-01, mult-zero, mult-one, mult-ls, mult-eq-same, mult-dist, mult-def-any, mult-a, ls-zero, less-trans, less-same, less-def-any, getint-abs, add-zero-01, add-zero, add-scale-neq, add-scale-eq, add-same, add-def-any, add-a,
int-basic2/add-c is used by sub-zero, sub-same, sub-id, sub-def-any, sub-add, square-sqrt-02, square-sqrt, square-scale, square-pos-01, square-pos, square-ls, square-isSquare, square-int-nlz, square-abs, mult-zero-01, mult-zero, mult-one, mult-ls, mult-eq-same, mult-dist, mult-def-any, mult-c, mult-a, ls-zero, ls-add-01, ls-add, less-trans, less-totality, less-same, less-def-any, getint-abs, add-zero-01, add-zero, add-scale-neq, add-scale-eq, add-same, add-def-any, add-c, add-a,
int-basic2/add-in is used by sub-def-any, sub-add, add-scale-neq,
int-basic2/add-zero is used by sub-zero, sub-def-any, mult-zero-01, mult-zero, mult-one, mult-def-any, ls-zero, less-same, less-def-any, getint-abs, add-zero-01, add-zero, add-scale-neq, add-def-any,
int-basic2/eq is used by add-scale-neq,
int-basic2/ls is used by add-scale-neq,
int-basic2/ls-01 is used by add-scale-neq,

Used from specification int-div

int-div/div-zero-nls is used by dec2int-not-neg,
int-div/modex is used by sub-def-any, square-sqrt-02, square-sqrt, square-scale, square-isSquare, mult-def-any, add-def-any, abs-any-def,
int-div/abs is used by sub-def-any, square-sqrt-02, neg-any-def, abs-any-def,
int-div/abs-div10-le is used by sub-def-any, neg-any-def, abs-any-def,
int-div/div-mult-num is used by sub-def-any, square-sqrt-02, square-sqrt, square-scale, square-isSquare, mult-def-any, add-def-any, abs-any-def,
int-div/mod-neg-01 is used by neg-any-def, add-scale-neq,
int-div/mod-zero-num is used by square-sqrt, square-scale, square-isSquare, mult-def-any, add-scale-neq, add-def-any, abs-any-def,
int-div/neg-01 is used by neg-any-def,
int-div/nummult-ls is used by square-sqrt, square-scale, square-isSquare,

Used from specification Unknown

Unknown/Unknown is used by sub-add, square-ls,
Unknown/Unknown is used by mult-ls,
Unknown/Unknown is used by mult-dist,