[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 olist-sort

olist-sort/Ordered is used by sort-max-max-list, sort-max, max-ins-max-last-sort,
olist-sort/empty is used by sort-max-max-list, sort-max-last, max-ins-max-last-sort,
olist-sort/emptyp is used by sort-max-max-list, sort-max,
olist-sort/in is used by sort-max-last,
olist-sort/one is used by sort-max-last,
olist-sort/rec is used by sort-max-max-list, sort-max-last,

Used from specification nat

nat/le-add is used by min-com, max-com,
nat/lels is used by min-com, max-com,
nat/succ-01 is used by ordered-max, max-ins-max,

Used from specification list-last

list-last/l-02 is used by max-ins-last,
list-last/prefix is used by max-ordered,
list-last/l is used by ordered-max, ordered-app-max, max-ins-last,
list-last/l-02 is used by ordered-max, ordered-app-max,
list-last/last-def is used by sort-max-max-list, sort-max-last, max-ins-last,
list-last/prefix-empty is used by max-ordered,

Used from specification list-data

list-data/elim-list-c is used by ordered-max, max-ins-max,
list-data/l is used by ordered-max, max-ins-max,

Used from specification list

list/Noassoc is used by max-sort-sublist,
list/Nil is used by sort-max-last, min-com, max-sort-sublist, max-ordered, max-ins-max-last-sort, max-ins-max-last, max-ge, max-com-01, max-com, max-append, ins-max,
list/a is used by sort-max-max-list, sort-max-last-01, sort-max-last, sort-max-append-1, ordered-max, ordered-app-max, min-com, max-sort-sublist, max-ordered, max-ins-max-last-sort, max-ins-max-last, max-ins-max, max-ins-last, max-ins, max-in-01, max-in, max-ge-first, max-ge-every, max-ge-01, max-ge, max-com-01, max-com, max-append, ins-max,
list/app is used by sort-max-max-list, sort-max-last, sort-max-append-1, ordered-max, ordered-app-max, min-com, max-sort-sublist, max-ordered, max-ins-max-last, max-ins-last, max-ins, max-in-01, max-in, max-ge-first, max-ge-every, max-ge, max-com, max-append, ins-max,
list/app-01 is used by sort-max-last-01, sort-max-last, ins-max,
list/app-02-ant is used by sort-max-last, min-com, max-sort-sublist, max-ordered, max-ins-max, max-ins, max-ge, max-com-01, max-com, max-append,
list/app-08 is used by sort-max-last, max-ins-max-last,
list/c is used by sort-max-max-list, sort-max-last, ordered-max, ordered-app-max, min-com, max-sort-sublist, max-ordered, max-ins-max-last, max-ins-max, max-ins-last, max-ins, max-in-01, max-ge-every, max-ge, max-com, max-append, ins-max,
list/c-04 is used by sort-max-last, max-ins-max-last-sort, max-ins-max-last, ins-max,
list/c-06 is used by max-ins-max-last, ins-max,
list/c-07 is used by ordered-max, max-ins-max,
list/c-08 is used by ordered-max, max-ins-max,
list/e is used by sort-max-max-list, max-ins-max, max-ins,
list/e-01 is used by sort-max-max-list, ordered-max, ordered-app-max, min-com, max-sort-sublist, max-ordered, max-ins-max, max-ins, max-in-01, max-ge, max-com, max-append,
list/e-02 is used by sort-max-max-list, sort-max-last,
list/e-03 is used by min-com, max-com,
list/first is used by sort-max-max-list,
list/in-06 is used by max-in-01,
list/in-15 is used by sort-max-last,
list/in-append is used by sort-max-last,
list/in-empty is used by max-ge-every,
list/in-rec is used by sort-max-last, max-ge-every,
list/len is used by min-com,
list/len-05 is used by ordered-max, min-com, max-ins-max, max-com,

Used from specification nat-basic2

nat-basic2/a is used by ordered-max, min-com, max-ins-max, max-com,
nat-basic2/c is used by ordered-max, min-com, max-ins-max, max-com,
nat-basic2/l is used by min-com, max-com,
nat-basic2/succ is used by ordered-max, min-com, max-ins-max, max-com,

Used from specification oelem

oelem/irreflexivity is used by sort-max-max-list, sort-max-last, ordered-max, ordered-app-max, min-com, max-ordered, max-ins-max-last, max-ins-max, max-ge-first, max-ge-01, max-ge, max-com-01, max-com, ins-max,
oelem/lel is used by sort-max-max-list, sort-max-last, ordered-max, min-com, max-sort-sublist, max-ordered, max-ins-max, max-ins, max-com-01, max-com, max-append,
oelem/ls-le is used by sort-max-max-list, sort-max-last, min-com, max-ins-max-last, max-ins-max, max-com, ins-max,
oelem/nen is used by sort-max-max-list, sort-max-last, min-com, max-ins-max-last, max-com, ins-max,
oelem/nll is used by sort-max-max-list, sort-max-last, ordered-max, ordered-app-max, min-com, max-ins-max-last-sort, max-ins-max-last, max-ins-max, max-ins-last, max-ins, max-ge-every, max-ge, max-com, ins-max,
oelem/nnn is used by sort-max-last, ordered-max, ordered-app-max, max-ins-max-last, max-ins-max, max-ins, max-com, ins-max,
oelem/seq is used by sort-max-last, max-ins-max-last, max-ins-max, max-com, ins-max,
oelem/sls is used by sort-max-last, min-com, max-sort-sublist, max-ordered, max-com, max-append,
oelem/transitivity is used by sort-max-max-list, sort-max-last, ordered-max, ordered-app-max, min-com, max-sort-sublist, max-ordered, max-ins-max-last, max-ins-max, max-ins-last, max-ins, max-ge-every, max-ge-01, max-ge, max-com, max-append, ins-max,

Used from specification nat-basic1

nat-basic1/one-01 is used by ordered-max, max-ins-max,

Used from specification olist

olist/cons-03 is used by max-ins-max, ins-max,
olist/ins-less-last is used by sort-max-last,
olist/ins-n is used by max-ins-max-last, max-ins, ins-max,
olist/k-le-r is used by ordered-max, max-ins-max,
olist/le-r is used by max-ins-max,
olist/ordered-append is used by sort-max-max-list,
olist/orderedle-all is used by max-ordered,
olist/app-01 is used by ins-max,
olist/cons-02 is used by ordered-max, ordered-app-max, max-ins-max-last,
olist/cons-03 is used by max-ins-max-last, ins-max,
olist/empty is used by max-ins-max, max-ins-last, max-ins,
olist/ins-e is used by sort-max-max-list, sort-max-last, max-ins-max-last-sort, max-ins-max-last, max-ins-max, max-ins-last, max-ins, ins-max,
olist/ins-n is used by max-ins-max, max-ins-last,
olist/ins-one is used by max-ins-last,
olist/ins-one-01 is used by sort-max-last, max-ins,
olist/ins-one-02 is used by sort-max-last,
olist/ins-y is used by max-ins-max-last, max-ins-max, max-ins, ins-max,
olist/le-o is used by sort-max-max-list, ordered-app-max, max-ins-max-last, ins-max,
olist/le-r is used by max-ins-max, ins-max,
olist/ole-last-01 is used by ordered-app-max,
olist/one-02 is used by sort-max-last,