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

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

Used from specification weakord

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

Used from specification olist

olist/cons-03 is used by ins-max, 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/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,
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-ins-last, max-ins-max,
olist/ins-e is used by sort-max-last, sort-max-max-list, ins-max, max-ins-last, max-ins-max, max-ins-max-last-sort,
olist/ins-n is used by ins-max, max-ins-last, max-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-ins-max,
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 nat-basic

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

Used from specification list

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

Used from specification list-data

Used from specification tord

tord/seq is used by sort-max-last, ins-max, max-ins-max, max-com,
tord/sls is used by sort-max-last, max-append, max-ordered, max-com, min-com, max-sort-sublist,

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

Used from specification list-del

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