[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-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 max-ins-last, sort-max-max-list, sort-max-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 nat

nat/anti is used by allgrrange-reclow, allgerange-reclow, allls-one, allge-one, allgr-numone, allge-numone, alllsrange-recup, alllsrange-reclow, allgr-one, allle-numone, allls-numone, allgrrange-recup, allle-one, allgerange-recup, alllerange-recup, alllerange-reclow,
nat/elim-pred-c is used by alllsrange-recup, ordered-count-splits, allgrrange-recup, allgerange-recup, alllerange-recup,
nat/eqle-one is used by ordered-count-splits,
nat/fle is used by allls-one, allge-one, allgr-numone, allge-numone, ordered-count-splits, allle-declower, allgr-one, allgr-declower, allle-numone, allls-numone, allge-declower, allls-declower, allle-one,
nat/fle-01 is used by allgrrange-upgr, allgrrange-reclow, allgerange-reclow, allle-decupper-inclower, alllsrange-recup, allle-incupper, allge-incupper, allle-decupper, allle-inclower, allls-incupper, alllsrange-reclow, alllerange-notupgr, alllsrange-upls, allle-declower, allgr-declower, allgr-incupper, allls-decupper-inclower, allgrrange-notupgr, allgrrange-recup, allgr-decupper-inclower, allge-declower, allls-declower, allgr-inclower, allgr-decupper, allge-decupper-inclower, allge-inclower, allgerange-recup, alllsrange-notupgr, allls-inclower, allge-decupper, allls-decupper, allgerange-notupls, alllerange-recup, alllerange-reclow,
nat/ge is used by allls-one, allge-one, allgr-numone, allge-numone, allgr-one, allle-numone, allls-numone, allle-one,
nat/le-add is used by max-ins-max, ordered-max, min-com, max-com,
nat/le-def is used by allls-one, allge-one, allgr-numone, allle-decupper-inclower, allge-numone, alllsrange-recup, allle-inclower, allls-incupper, allle-declower, allgr-one, allgr-declower, allle-numone, allls-numone, allls-decupper-inclower, allgrrange-recup, allgr-decupper-inclower, allge-declower, allgr-inclower, allge-decupper-inclower, allge-inclower, allle-one, allgerange-recup, allls-inclower, alllerange-recup,
nat/le-ls-simp is used by allls-one, allge-one, allgr-numone, allge-numone, allgr-one, allle-numone, allls-numone, allle-one,
nat/lels is used by min-com, allgrrange-reclow, allgerange-reclow, allls-one, allge-one, allgr-numone, max-com, allle-decupper-inclower, allge-numone, alllsrange-recup, allle-incupper, allge-incupper, allle-decupper, alllsrange-reclow, ordered-count-splits, allgr-one, allle-numone, allls-numone, allgr-incupper, allls-decupper-inclower, allgrrange-recup, allgr-decupper-inclower, allls-declower, allgr-decupper, allge-decupper-inclower, allle-one, allgerange-recup, allge-decupper, allls-decupper, alllerange-recup, alllerange-reclow,
nat/lels-03 is used by allgrrange-reclow, allgerange-reclow, alllsrange-recup, allls-incupper, alllsrange-reclow, allgrrange-recup, allls-declower, allgerange-recup, alllerange-recup, alllerange-reclow,
nat/ler is used by allgrrange-reclow, allgerange-reclow, allls-one, allgrrange-notlowgr, allge-one, allgr-numone, allge-numone, alllsrange-notlowgr, alllerange-notlowgr, alllsrange-reclow, allgrrange-grlow, allgr-one, allle-numone, allls-numone, alllsrange-lslow, allle-one, alllerange-reclow, allgerange-notlowls,
nat/les is used by ordered-count-splits,
nat/let is used by allls-one, allge-one, allgr-numone, allge-numone, alllsrange-recup, allle-incupper, allge-incupper, allls-incupper, allgr-one, allle-numone, allls-numone, allgr-incupper, allgrrange-recup, allle-one, allgerange-recup, alllerange-recup,
nat/lez is used by allle-alllerange, allgr-allsrange, allls-allsrange, ordered-count-splits, allge-allgerange,
nat/ls is used by alllsrange-recup, allgrrange-recup, allgerange-recup, alllerange-recup,
nat/ls-le-simp is used by allls-one, allge-one, allgr-numone, allgr-empty, allge-numone, allle-empty, allls-empty, allgr-one, allge-empty, allle-numone, allls-numone, allle-one,
nat/succ-01 is used by allgrrange-reclow, allgerange-reclow, alllsrange-reclow, ordered-count-splits, alllerange-reclow,

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 max-ins-max, ordered-max,
olist/le-r is used by max-ins-max,
olist/orderedle-all is used by max-ordered,
olist/orderedle-append is used by sort-max-max-list,
olist/orderedle-ls is used by ordered-count-splits,
olist/app-01 is used by ordered-max, ordered-app-max, ordered-count-splits,
olist/cons-02 is used by ins-max, ordered-count-splits,
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 max-ins-max, max-ins-max-last-sort, max-ins-last, ins-max, sort-max-max-list, sort-max-last,
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 max-ins, sort-max-last,
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 ordered-app-max, ins-max, sort-max-max-list,
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 oelem

oelem/irreflexivity is used by max-ins-max, max-ordered, ordered-max, min-com, allgrrange-notlowgr, ordered-app-max, notallge-notallge, max-com, max-ge-01, max-ge-first, ins-max, alllsrange-notlowgr, allgr-notls, notallle-notallls, max-ge, sort-max-max-list, ordered-count-splits, allgrrange-notupgr, sort-max-last, allls-notgr, max-com-01, alllsrange-notupgr,
oelem/lel is used by max-ins-max, ordered-max, max-append, max-com, max-sort-sublist, sort-max-last,
oelem/ls-le is used by max-ins-max, min-com, max-com, ins-max, sort-max-max-list, sort-max-last,
oelem/nen is used by max-com, ins-max, sort-max-last,
oelem/nll is used by max-ins-max, ordered-max, min-com, allgrrange-reclow, max-ins-max-last-sort, ordered-app-max, max-ins-last, max-com, ins-max, max-ge, sort-max-max-list, ordered-count-splits, max-ins, sort-max-last, allgrrange-recup, max-ge-every, alllerange-recup, alllerange-reclow,
oelem/nnn is used by max-ins-max, ordered-max, ordered-app-max, max-com, ins-max, ordered-count-splits, max-ins, sort-max-last,
oelem/seq is used by max-ins-max, max-com, ins-max, sort-max-last,
oelem/sls is used by max-ordered, min-com, max-append, max-com, max-sort-sublist, sort-max-last,
oelem/transitivity is used by max-ins-max, max-ordered, ordered-max, min-com, max-append, allgrrange-notlowgr, ordered-app-max, notallge-notallge, max-ins-last, max-com, max-ge-01, ins-max, alllsrange-notlowgr, allgr-notls, notallle-notallls, max-ge, sort-max-max-list, max-sort-sublist, max-ins, allgrrange-notupgr, sort-max-last, allls-notgr, max-ge-every, alllsrange-notupgr,

Used from specification list-data

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

nat-basic/a is used by allgrrange-upgr, max-ins-max, ordered-max, min-com, allgrrange-reclow, allgerange-reclow, allls-one, allge-one, allgr-numone, max-com, allle-decupper-inclower, allge-numone, alllsrange-recup, allle-incupper, allge-incupper, allle-decupper, allle-inclower, allls-incupper, alllsrange-reclow, alllerange-notupgr, alllsrange-upls, ordered-count-splits, allle-declower, allgr-one, allgr-declower, allle-numone, allls-numone, allgr-incupper, allls-decupper-inclower, allgrrange-notupgr, allgrrange-recup, allgr-decupper-inclower, allge-declower, allls-declower, allgr-inclower, allgr-decupper, allge-decupper-inclower, allge-inclower, allle-one, allgerange-recup, alllsrange-notupgr, allls-inclower, allge-decupper, allls-decupper, allgerange-notupls, alllerange-recup, alllerange-reclow,
nat-basic/add-base is used by ordered-count-splits,
nat-basic/c is used by allgrrange-upgr, max-ins-max, ordered-max, min-com, allgrrange-reclow, allgerange-reclow, allls-one, allge-one, allgr-numone, max-com, allle-decupper-inclower, allge-numone, alllsrange-recup, allle-incupper, allge-incupper, allle-decupper, allle-inclower, allls-incupper, alllsrange-reclow, alllerange-notupgr, alllsrange-upls, ordered-count-splits, allle-declower, allgr-one, allgr-declower, allle-numone, allls-numone, allgr-incupper, allls-decupper-inclower, allgrrange-notupgr, allgrrange-recup, allgr-decupper-inclower, allge-declower, allls-declower, allgr-inclower, allgr-decupper, allge-decupper-inclower, allge-inclower, allle-one, allgerange-recup, alllsrange-notupgr, allls-inclower, allge-decupper, allls-decupper, allgerange-notupls, alllerange-recup, alllerange-reclow,
nat-basic/f is used by allgrrange-upgr, allle-alllerange, allgrrange-reclow, allgr-alt-def, allgerange-reclow, allls-one, allgr-allsrange, allls-allsrange, allgrrange-notlowgr, allge-one, allgr-numone, allle-decupper-inclower, allls-alt-def, allge-numone, allgr-gr, alllsrange-recup, alllsrange-notlowgr, allle-incupper, alllerange-notlowgr, allgr-notls, allge-incupper, allge-notls, allle-decupper, allle-inclower, allls-ls, allls-incupper, alllsrange-reclow, allge-alt-def, alllerange-notupgr, alllsrange-upls, ordered-count-splits, allle-alt-def, allle-declower, allgrrange-grlow, allgr-one, allgr-declower, allle-numone, allls-numone, allgr-incupper, allls-decupper-inclower, allgrrange-notupgr, allgrrange-recup, allgr-decupper-inclower, allge-declower, allle-notgr, allls-declower, allge-allgerange, allgr-inclower, allls-notgr, allgr-decupper, alllsrange-lslow, allge-decupper-inclower, allge-inclower, allle-one, allgerange-recup, alllsrange-notupgr, allls-inclower, allge-decupper, allls-decupper, allgerange-notupls, alllerange-recup, alllerange-reclow, allgerange-notlowls,
nat-basic/l is used by min-com, max-com, alllsrange-recup, ordered-count-splits, allgrrange-recup, allgerange-recup, alllerange-recup,
nat-basic/l-01 is used by allle-incupper, allge-incupper, allls-incupper, allle-declower, allgr-declower, allgr-incupper, allge-declower, allls-declower,
nat-basic/l-02 is used by allle-decupper-inclower, allle-decupper, allle-inclower, allls-decupper-inclower, allgr-decupper-inclower, allgr-inclower, allgr-decupper, allge-decupper-inclower, allge-inclower, allls-inclower, allge-decupper, allls-decupper,
nat-basic/less-zero is used by alllsrange-recup, allgrrange-recup, allgerange-recup, alllerange-recup,
nat-basic/lf is used by allgrrange-reclow, allgerange-reclow, alllsrange-recup, alllsrange-reclow, allgrrange-recup, allgerange-recup, alllerange-recup, alllerange-reclow,
nat-basic/lf-01 is used by ordered-count-splits,
nat-basic/lf-02 is used by allls-one, allge-one, allgr-numone, allge-numone, allgr-one, allle-numone, allls-numone, allle-one,
nat-basic/ls-02 is used by alllsrange-recup, allgrrange-recup, allgerange-recup, alllerange-recup,
nat-basic/nls-fst is used by alllsrange-recup, ordered-count-splits, allgrrange-recup, allgerange-recup, alllerange-recup,
nat-basic/one-01 is used by alllsrange-recup, ordered-count-splits, allgrrange-recup, allgerange-recup, alllerange-recup,
nat-basic/oz is used by alllsrange-recup, ordered-count-splits, allgrrange-recup, allgerange-recup, alllerange-recup,
nat-basic/refl-Nat is used by allgrrange-upgr, allls-one, allge-one, allgr-numone, allge-numone, alllsrange-recup, alllerange-notupgr, alllsrange-upls, ordered-count-splits, allgr-one, allle-numone, allls-numone, allgrrange-notupgr, allgrrange-recup, allle-one, allgerange-recup, alllsrange-notupgr, allgerange-notupls, alllerange-recup,
nat-basic/s-04 is used by allgrrange-upgr, allls-one, allge-one, allgr-numone, allge-numone, alllsrange-recup, alllerange-notupgr, alllsrange-upls, ordered-count-splits, allgr-one, allle-numone, allls-numone, allgrrange-notupgr, allgrrange-recup, allle-one, allgerange-recup, alllsrange-notupgr, allgerange-notupls, alllerange-recup,
nat-basic/succ is used by allgrrange-reclow, allgerange-reclow, max-com, alllsrange-recup, alllsrange-reclow, ordered-count-splits, allgrrange-recup, allgerange-recup, alllerange-recup, alllerange-reclow,
nat-basic/trans-Nat is used by allgrrange-reclow, allgerange-reclow, alllsrange-recup, alllsrange-reclow, allgrrange-recup, allgerange-recup, alllerange-recup, alllerange-reclow,
nat-basic/zero is used by alllsrange-recup, ordered-count-splits, allgrrange-recup, allgerange-recup, alllerange-recup,

Used from specification list

list/Noassoc is used by max-sort-sublist,
list/Nil is used by max-ordered, min-com, max-ins-max-last-sort, max-append, max-com, ins-max, max-ge, max-sort-sublist, sort-max-last, max-com-01,
list/a is used by max-ins-max, allls-rec, max-ordered, ordered-max, allle-rec, min-com, max-ins-max-last-sort, max-append, ordered-app-max, max-ins-last, max-com, allgr-rec, max-ge-01, max-in, sort-max-last-01, max-ge-first, ins-max, allge-rec, max-ge, sort-max-max-list, ordered-count-splits, max-sort-sublist, max-ins, sort-max-last, max-in-01, sort-max-append-1, max-com-01, max-ge-every,
list/app is used by max-ordered, ordered-max, min-com, max-append, ordered-app-max, max-ins-last, max-com, max-in, max-ge-first, ins-max, max-ge, sort-max-max-list, max-sort-sublist, max-ins, sort-max-last, max-in-01, sort-max-append-1,
list/app-01 is used by sort-max-last-01, sort-max-last,
list/app-02 is used by max-ins-max, max-ordered, min-com, max-append, max-com, max-ge, max-sort-sublist, max-ins, sort-max-last, max-com-01,
list/c is used by max-ins-max, max-ordered, ordered-max, min-com, max-append, ordered-app-max, max-ins-last, max-com, ins-max, max-ge, sort-max-max-list, ordered-count-splits, max-sort-sublist, max-ins, sort-max-last, max-in-01, max-ge-every,
list/c-04 is used by max-ins-max-last-sort, ins-max, sort-max-last,
list/c-06 is used by ins-max,
list/c-07 is used by max-ins-max, ordered-max,
list/c-08 is used by max-ins-max, ordered-max,
list/e is used by max-ins-max, sort-max-max-list, max-ins,
list/e-01 is used by max-ins-max, max-ordered, ordered-max, min-com, max-append, ordered-app-max, max-com, max-ge, sort-max-max-list, ordered-count-splits, max-sort-sublist, max-ins, max-in-01,
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 allge-base, allgr-base, allle-base, allls-base, max-ge-every,
list/in-rec is used by allls-rec, allle-rec, allgr-rec, allge-rec,
list/len is used by max-ins-max, ordered-max, min-com,
list/len-01 is used by ins-max,
list/len-02 is used by max-ins-max, ordered-max, min-com, ordered-count-splits,
list/len-05 is used by max-com, ordered-count-splits,

Used from specification olist-sort

olist-sort/Ordered is used by max-ins-max-last-sort, sort-max-max-list, sort-max,
olist-sort/empty is used by max-ins-max-last-sort, sort-max-max-list, sort-max-last,
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 list-del

list-del/get-append-less is used by ordered-count-splits,
list-del/in-get is used by allle-alllerange, allgr-alt-def, allgr-allsrange, allls-allsrange, allls-alt-def, allge-alt-def, allle-alt-def, allge-allgerange,
list-del/get-append-grt is used by ordered-count-splits,
list-del/get-in is used by allle-alllerange, allgr-alt-def, allgr-allsrange, allls-allsrange, allls-alt-def, allgr-gr, allgr-notls, allge-notls, allls-ls, allge-alt-def, ordered-count-splits, allle-alt-def, allle-notgr, allge-allgerange, allls-notgr,
list-del/one-03 is used by ordered-count-splits,