[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 nat-basic

nat-basic/a is used by ordered-max, ordered-count-splits, min-com, max-ins-max, max-com,
nat-basic/add-base is used by ordered-count-splits,
nat-basic/c is used by ordered-max, ordered-count-splits, min-com, max-ins-max, max-com,
nat-basic/f is used by ordered-count-splits,
nat-basic/l is used by ordered-count-splits, min-com, max-com,
nat-basic/lf-01 is used by ordered-count-splits,
nat-basic/nls-fst is used by ordered-count-splits,
nat-basic/one-01 is used by ordered-count-splits,
nat-basic/oz is used by ordered-count-splits,
nat-basic/refl-nat is used by ordered-count-splits,
nat-basic/s-04 is used by ordered-count-splits,
nat-basic/succ is used by ordered-count-splits, max-com,
nat-basic/zero is used by ordered-count-splits,

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/elim-pred-c is used by ordered-count-splits,
nat/eqle-one is used by ordered-count-splits,
nat/fle is used by ordered-count-splits,
nat/le-add is used by ordered-max, min-com, max-ins-max, max-com,
nat/lels is used by ordered-count-splits, min-com, max-com,
nat/les is used by ordered-count-splits,
nat/lez is used by ordered-count-splits,
nat/succ-01 is used by ordered-count-splits,

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-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/last-one is used by ordered-max, ordered-app-max, 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, ordered-count-splits, 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-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-count-splits, ordered-app-max, min-com, max-sort-sublist, max-ordered, max-ins-max-last-sort, 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-last, max-ins, max-in-01, max-in, max-ge-first, max-ge, max-com, max-append, ins-max,
list/app-01 is used by sort-max-last-01, sort-max-last,
list/app-02 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/c is used by sort-max-max-list, sort-max-last, ordered-max, ordered-count-splits, ordered-app-max, min-com, max-sort-sublist, max-ordered, 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, ins-max,
list/c-06 is used by 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-count-splits, 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-17 is used by sort-max-last, max-ge-every,
list/in-append is used by sort-max-last, max-ge-every,
list/in-empty is used by max-ge-every,
list/len is used by ordered-max, min-com, max-ins-max,
list/len-01 is used by ins-max,
list/len-02 is used by ordered-max, ordered-count-splits, min-com, max-ins-max,
list/len-05 is used by ordered-count-splits, max-com,

Used from specification filter-count

filter-count/count-zero is used by ordered-count-splits,
filter-count/count-base is used by ordered-count-splits,
filter-count/count-rec is used by ordered-count-splits,

Used from specification oelem

oelem/irreflexivity is used by sort-max-max-list, sort-max-last, ordered-max, ordered-count-splits, ordered-app-max, min-com, max-ordered, 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-last, ordered-max, max-sort-sublist, max-ins-max, max-com, max-append,
oelem/ls-le is used by sort-max-max-list, sort-max-last, min-com, max-ins-max, max-com, ins-max,
oelem/nen is used by sort-max-last, max-com, ins-max,
oelem/nll is used by sort-max-max-list, sort-max-last, ordered-max, ordered-count-splits, ordered-app-max, min-com, max-ins-max-last-sort, 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-count-splits, ordered-app-max, max-ins-max, max-ins, max-com, ins-max,
oelem/seq is used by sort-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, max-ins-last, max-ins, max-ge-every, max-ge-01, max-ge, max-com, max-append, 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,
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/orderedle-ls is used by ordered-count-splits,
olist/app-01 is used by ordered-max, ordered-count-splits, ordered-app-max,
olist/cons-02 is used by ordered-count-splits, ins-max,
olist/cons-03 is used by 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, max-ins-last, ins-max,
olist/ins-n is used by max-ins-max, max-ins-last, ins-max,
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, max-ins,
olist/le-o is used by sort-max-max-list, ordered-app-max, ins-max,
olist/le-r is used by ins-max,
olist/ole-last-01 is used by ordered-app-max,
olist/one-02 is used by sort-max-last,

Used from specification list-del

list-del/get-append-less is used by ordered-count-splits,
list-del/get-append-grt is used by ordered-count-splits,
list-del/get-in is used by ordered-count-splits,
list-del/one-03 is used by ordered-count-splits,