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

list/intlist/a is used by unique-prefix,
list/intlist/firsteq is used by unique-prefix, first-in,
list/intlist/Nil is used by min-concat, max-concat,
list/intlist/a is used by unique-prefix-nil, unique-prefix, min-le, min-in, min-concat, max-in, max-gt-rec, max-ge, max-concat, first-in, depths-size-one, depths-nonnil,
list/intlist/app is used by unique-prefix-nil, min-le, min-in, min-concat, max-in, max-ge, max-concat,
list/intlist/app-01 is used by unique-prefix,
list/intlist/app-02-ant is used by unique-prefix, max-concat, depths-nonnil,
list/intlist/c is used by unique-prefix, min-le, min-in, min-concat, max-in, max-ge, max-concat,
list/intlist/c-04 is used by depths-one,
list/intlist/e is used by min-concat, max-concat, depths-nonnil,
list/intlist/e-01 is used by unique-prefix, min-in, min-concat, max-in, max-concat,
list/intlist/first-app is used by unique-prefix,
list/intlist/in-01 is used by min-le, max-ge,
list/intlist/in-06 is used by min-in, max-in,
list/intlist/in-08 is used by first-in,
list/intlist/in-10 is used by max-in,
list/intlist/in-11 is used by unique-prefix,
list/intlist/in-12 is used by max-ge,
list/intlist/in-14 is used by unique-prefix, first-in,
list/intlist/in-17 is used by unique-prefix, min-le, min-in, max-gt-rec, max-ge,
list/intlist/in-append is used by unique-prefix, min-le, min-in, max-gt-rec, max-ge, first-in,
list/intlist/in-empty is used by min-le, max-ge,
list/intlist/len is used by min-le, min-in, min-concat, max-in, max-ge, max-concat, depths-size-one,
list/intlist/len-02 is used by min-le, min-in, min-concat, max-in, max-ge, max-concat, depths-size-one, depths-one,

Used from specification int-basic2

int-basic2/add-a is used by unique-prefix, depths-min, depths-max,
int-basic2/add-c is used by unique-prefix, depths-size-one, depths-min, depths-max,
int-basic2/succ-01 is used by depths-max,

Used from specification int-abs

int-abs/forward-lels is used by min-le, max-in, max-ge, in-depths-gt,
int-abs/forward-lsle is used by max-in,
int-abs/lels is used by min-le, min-in, min-concat, max-in, max-ge, max-concat,
int-abs/lels-01 is used by min-le-max, min-le, max-ge, depths-min, depths-max,
int-abs/lels-03 is used by unique-prefix, min-le-max, max-gt-rec, in-depths-gt,
int-abs/succ-01 is used by unique-prefix,
int-abs/succ-02 is used by depths-min, depths-max,

Used from specification int-min

int-min/Max-left is used by min-le, min-concat, max-concat,
int-min/Min-left is used by min-in, max-in, max-ge,
int-min/Max-left is used by min-in,
int-min/Max-right is used by min-le, min-in, min-concat, max-in, max-concat,
int-min/Min-left is used by min-le, min-in, min-concat, max-ge, max-concat,
int-min/Min-right is used by min-le, min-in, min-concat, max-in, max-ge, max-concat,
int-min/max is used by max-in, max-concat,
int-min/max-01 is used by max-ge, max-concat, depths-max,
int-min/max-a is used by min-le, min-in, min-concat, max-in, max-ge, max-concat, depths-max,
int-min/max-c is used by min-le, min-in, min-concat, max-in, max-ge, max-concat, depths-max,
int-min/min-02 is used by depths-min,
int-min/min-03 is used by min-le, max-concat,
int-min/min-a is used by min-le, min-in, min-concat, max-in, max-ge, max-concat, depths-min,
int-min/min-c is used by min-le, min-in, min-concat, max-in, max-ge, max-concat, depths-min,
int-min/min-right is used by min-concat,

Used from specification nat-basic1

nat-basic1/one is used by max-concat,

Used from specification int-basic1

int-basic1/irref is used by min-le, max-in, max-ge, depths-min, depths-max,
int-basic1/ls-01 is used by min-in, max-in, depths-max,
int-basic1/lst-01 is used by min-in,

Used from specification list-data

list-data/intlist/elim-list-c is used by unique-prefix,
list-data/intlist/l is used by depths-size-one,

Used from specification tree

tree/disj is used by unique-prefix, depths-size-one,
tree/inj is used by unique-prefix,

Used from specification nat

nat/add-num-03 is used by max-concat,
nat/le-add is used by max-concat,
nat/lels is used by max-concat,

Used from specification nat-basic2

nat-basic2/a is used by min-le, min-in, min-concat, max-in, max-ge, max-concat, depths-size-one,
nat-basic2/c is used by min-le, min-in, min-concat, max-in, max-ge, max-concat, depths-size-one,
nat-basic2/l is used by min-le, min-in, min-concat, max-in, max-ge, max-concat,
nat-basic2/one-02 is used by depths-size-one,
nat-basic2/one-03 is used by depths-size-one,