[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/addex is used by isprefix-add-prefixn-size,
nat-basic/a is used by prefixn-split-sublist, prefixn-split-dropn, prefixn-shift-right, prefixn-prepend-one, prefixn-prefixn, prefixn-neq-empty-plusone, prefixn-eq-prefixn-app, prefixn-eq-append, prefixn-butlast, prefixn-append-slice, prefixn-append-prefix, prefixn-append-left, prefix-prefixn-not-shorter, prefix-append-one-sizeeq, isprefix-eq-size-app-eq1, isprefix-eq-size-app-eq, isprefix-append-size, isprefix-app-size-ls1, isprefix-app-size-ls, isprefix-add-prefixn-size, in-prefixn-samepos, in-prefixn-pos-smaller0, in-prefixn-pos-smaller, in-prefixn-in-shorter-prefix, dropn-first,
nat-basic/add-base is used by prefixn-eq-prefixn-app, prefixn-append-slice, isprefix-eq-size-app-eq, dropn-first,
nat-basic/c is used by prefixn-split-sublist, prefixn-split-dropn, prefixn-shift-right, prefixn-prepend-one, prefixn-prefixn, prefixn-neq-empty-plusone, prefixn-eq-prefixn-app, prefixn-eq-append, prefixn-butlast, prefixn-append-slice, prefixn-append-prefix, prefixn-append-left, prefix-prefixn-not-shorter, prefix-append-one-sizeeq, isprefix-eq-size-app-eq1, isprefix-eq-size-app-eq, isprefix-append-size, isprefix-app-size-ls1, isprefix-app-size-ls, isprefix-add-prefixn-size, in-prefixn-samepos, in-prefixn-pos-smaller0, in-prefixn-pos-smaller, in-prefixn-in-shorter-prefix, dropn-first,
nat-basic/eq-01 is used by prefixn-butlast, isprefix-eq-size-app-eq1, isprefix-add-prefixn-size,
nat-basic/eq-02 is used by prefixn-eq-prefixn-app, prefix-append-one-sizeeq, isprefix-eq-size-app-eq1, isprefix-eq-size-app-eq,
nat-basic/f is used by prefixn-split-sublist, prefixn-split-dropn, prefixn-size-prefixn, prefixn-prefixn, prefixn-len-le-n, prefixn-full-eq, prefixn-eq-prefixn-app, prefixn-eq-append, prefixn-butlast, prefixn-append-slice, prefixn-append-prefix, prefixn-append-left, prefix-prefixn-not-shorter, isprefix-prefixn, isprefix-eq-size-app-eq, isprefix-append-size, isprefix-app-size-ls1, isprefix-app-size-ls, isprefix-add-prefixn-size, in-prefixn-pos-smaller0, in-prefixn-pos-smaller, in-prefixn-in-shorter-prefix, in-prefixn-at-smaller, dropn-first,
nat-basic/l is used by prefixn-prefixn, isprefix-app-size-ls, in-prefixn-pos-smaller0,
nat-basic/l-01 is used by prefixn-prefixn, prefixn-eq-prefixn-app, prefixn-append-prefix,
nat-basic/l-02 is used by prefixn-split-sublist, prefixn-split-dropn, prefixn-prefixn, prefixn-eq-prefixn-app, prefixn-butlast, prefixn-append-left, prefix-prefixn-not-shorter, isprefix-append-size, isprefix-app-size-ls1, isprefix-app-size-ls, isprefix-add-prefixn-size,
nat-basic/l-05 is used by prefixn-eq-prefixn-app,
nat-basic/lf is used by prefixn-prefixn, prefixn-eq-prefixn-app, prefix-prefixn-not-shorter, in-prefixn-pos-smaller0,
nat-basic/lf-01 is used by prefixn-split-sublist, prefixn-split-dropn, prefixn-full-eq, prefixn-eq-prefixn-app, isprefix-prefixn, isprefix-eq-size-app-eq,
nat-basic/lf-02 is used by prefixn-split-sublist, prefixn-split-dropn, prefixn-prefixn, prefixn-full-eq, prefixn-eq-prefixn-app, isprefix-append-size, isprefix-app-size-ls1, isprefix-add-prefixn-size,
nat-basic/ls-02 is used by prefixn-split-sublist, prefixn-split-dropn, prefixn-prefixn, prefixn-full-eq, prefixn-eq-prefixn-app,
nat-basic/nls-fst is used by prefixn-prefixn,
nat-basic/one-01 is used by prefixn-butlast, dropn-first,
nat-basic/oz is used by prefixn-butlast,
nat-basic/ref is used by prefixn-size-prefixn, prefixn-prefixn, prefixn-len-le-n, prefixn-eq-append, dropn-first,
nat-basic/s-04 is used by prefixn-butlast, in-prefixn-pos-smaller, dropn-first,
nat-basic/succ is used by prefixn-prepend-one, prefixn-prefixn, prefixn-eq-prefixn-app, prefix-prefixn-not-shorter, in-prefixn-pos-smaller0, in-prefixn-pos-smaller, dropn-first,
nat-basic/trans is used by prefixn-prefixn, prefixn-eq-prefixn-app, prefix-prefixn-not-shorter, in-prefixn-pos-smaller0,
nat-basic/z-01 is used by prefixn-neq-empty-plusone, prefixn-butlast,
nat-basic/zero-01 is used by in-prefixn-pos-smaller,

Used from specification nat

nat/add-01 is used by dropn-first,
nat/anti is used by prefixn-le-size, prefixn-fulln, prefixn-full-eq, prefixn-eq-prefixn-app, prefixn-append-slice,
nat/elim-pred-c is used by prefixn-butlast,
nat/elim-sub is used by prefixn-shift-right, prefixn-append-slice,
nat/eq-01 is used by prefixn-append-slice,
nat/eqle-one is used by prefixn-butlast,
nat/fle is used by prefixn-prefixn, prefixn-butlast, prefixn-append-slice, prefixn-append-left, in-prefixn-pos-smaller0, in-prefixn-pos-smaller, dropn-first,
nat/fle-01 is used by prefixn-split-sublist, prefixn-split-dropn, prefixn-prefixn, prefixn-eq-prefixn-app,
nat/ge is used by prefixn-le-size, prefixn-full-eq, prefixn-eq-prefixn-app, prefixn-append-prefix,
nat/gr-def is used by isprefix-prefixn,
nat/le-add is used by prefixn-prefixn, prefixn-eq-prefixn-app,
nat/le-def is used by prefixn-split-sublist, prefixn-split-dropn, prefixn-size-prefixn, prefixn-shift-right, prefixn-prefixn, prefixn-len-le-n, prefixn-le-size, prefixn-full-eq, prefixn-eq-prefixn-app, prefixn-eq-append, prefixn-butlast, prefixn-append-slice, prefixn-append-prefix, prefixn-append-left, prefix-prefixn-exact, isprefix-prefixn, isprefix-add-prefixn-size, in-prefixn-pos-smaller0, in-prefixn-pos-smaller, in-prefixn-in-shorter-prefix, dropn-first,
nat/le-ls-simp is used by prefixn-split-dropn, prefixn-size-prefixn, prefixn-shift-right, prefixn-prefixn, prefixn-eq-prefixn-app, prefixn-eq-append, prefixn-append-slice, prefixn-append-prefix, isprefix-prefixn,
nat/lels is used by prefixn-prefixn, prefixn-eq-prefixn-app, prefixn-butlast, in-prefixn-pos-smaller,
nat/lels-02 is used by prefixn-eq-prefixn-app,
nat/lels-03 is used by prefixn-len-le-n, prefixn-le-size, prefixn-full-eq, prefixn-eq-prefixn-app, prefixn-append-prefix, prefix-prefixn-not-shorter,
nat/lep is used by prefixn-split-sublist, prefixn-split-dropn, prefixn-shift-right, prefixn-prefixn, prefixn-eq-prefixn-app, prefixn-eq-append, prefixn-butlast, prefixn-append-slice, prefixn-append-prefix, isprefix-add-prefixn-size, in-prefixn-samepos, in-prefixn-in-shorter-prefix, dropn-first,
nat/lep-02 is used by prefixn-split-sublist, prefixn-split-dropn, prefixn-prepend-one, prefixn-butlast,
nat/ler is used by slice-range0, prefixn-split-sublist, prefixn-size-prefixn, prefixn-le-size, prefixn-full, prefixn-eq-prefixn-app, in-prefixn-pos-smaller0,
nat/let is used by prefixn-shift-right, prefixn-append-slice, in-prefixn-in-shorter-prefix,
nat/lez is used by prefixn-eq-empty, prefixn-0, in-prefixn-pos-smaller, dropn-0,
nat/lez-01 is used by prefixn-split-dropn, prefixn-eq-empty, prefixn-empty, in-prefixn-pos-smaller0, in-prefixn-pos-smaller, dropn-empty,
nat/ls-01 is used by dropn-first,
nat/ls-02 is used by prefixn-split-dropn,
nat/ls-03 is used by prefixn-shift-right, prefixn-butlast, prefixn-append-slice, prefixn-append-prefix, dropn-first,
nat/ls-le-simp is used by prefixn-split-dropn, prefixn-prefixn, prefixn-le-size, prefixn-eq-prefixn-app, prefixn-butlast, prefixn-append-slice, isprefix-prefixn,
nat/pred-03 is used by dropn-first,
nat/sub-ls is used by dropn-first,
nat/succ-01 is used by prefixn-neq-empty-plusone, prefixn-butlast, in-prefixn-pos-smaller,
nat/zero is used by slice-range0, prefixn-append-slice,

Used from specification list-last

list-last/prefix is used by prefix-prefixn-not-shorter, prefix-prefixn-exact, prefix-append-one-sizeeq, isprefix-eq-size-app-eq1, isprefix-eq-size-app-eq, isprefix-append-size, isprefix-app-size-ls1, isprefix-app-size-ls, isprefix-add-prefixn-size,
list-last/last-elim is used by prefixn-butlast,
list-last/postifx-app-03 is used by prefix-append-one-sizeeq, isprefix-eq-size-app-eq1, isprefix-eq-size-app-eq,
list-last/prefix-app is used by isprefix-app-prefixn-isprefix,
list-last/prefix-app-01 is used by prefixn-append-prefix,
list-last/prefix-app-05 is used by prefixn-append-prefix,
list-last/prefix-longer-01 is used by prefix-prefixn-exact, isprefix-prefixn,
list-last/prefix-one-01 is used by prefix-append-one-sizeeq,
list-last/prefix-self is used by prefix-prefixn-same, isprefix-prefixn, isprefix-eq-size-app-eq1, isprefix-eq-size-app-eq,

Used from specification list-data

list-data/length-neq is used by prefixn-full-eq, prefix-append-one-sizeeq,
list-data/elim-list-c is used by dropn-first,
list-data/l is used by prefixn-prefixn, prefixn-full-eq, prefixn-eq-prefixn-app, prefixn-butlast, prefixn-append-prefix, prefix-prefixn-not-shorter, prefix-append-one-sizeeq, isprefix-prefixn, isprefix-eq-size-app-eq1, isprefix-eq-size-app-eq, isprefix-append-size, isprefix-app-size-ls1, isprefix-add-prefixn-size, in-prefixn-at-smaller, dropn-first,
list-data/length-rest is used by dropn-first,
list-data/size-01 is used by prefixn-split-dropn, prefixn-eq-prefixn-app, prefixn-eq-empty, prefixn-empty, prefixn-butlast, prefixn-append-slice, isprefix-eq-size-app-eq, dropn-empty,

Used from specification list

list/Nil is used by prefixn-eq-prefixn-app,
list/a is used by prefixn-split-sublist, prefixn-split-dropn, prefixn-shift-right, prefixn-prepend-one, prefixn-prefixn, prefixn-eq-prefixn-app, prefixn-eq-append, prefixn-butlast, prefixn-append-slice, prefixn-append-prefix, prefixn-append-left, prefix-prefixn-not-shorter, prefix-prefixn-exact, prefix-append-one-sizeeq, isprefix-eq-size-app-eq1, isprefix-eq-size-app-eq, isprefix-append-size, isprefix-app-size-ls1, isprefix-app-size-ls, isprefix-app-prefixn-isprefix, isprefix-add-prefixn-size, in-prefixn-samepos, in-prefixn-pos-smaller0, in-prefixn-pos-smaller, in-prefixn-in-shorter-prefix, dropn-first,
list/app is used by prefixn-split-dropn, prefixn-eq-prefixn-app, prefixn-append-slice,
list/app-01 is used by prefixn-shift-right, prefixn-eq-prefixn-app, prefixn-eq-append, prefixn-append-slice, isprefix-eq-size-app-eq1,
list/app-02 is used by prefixn-eq-prefixn-app, dropn-first,
list/app-04 is used by prefixn-prefixn, prefixn-eq-prefixn-app, prefixn-eq-append, prefix-append-one-sizeeq, isprefix-eq-size-app-eq1,
list/app-08 is used by prefixn-prepend-one,
list/c is used by prefixn-prepend-one, in-prefixn-pos-smaller0, in-prefixn-pos-smaller, dropn-first,
list/c-04 is used by prefixn-single-1,
list/e is used by prefix-append-one-sizeeq,
list/e-02 is used by prefixn-butlast,
list/e-03 is used by prefixn-butlast,
list/in-11 is used by in-prefixn-in-shorter-prefix,
list/in-15 is used by prefix-append-one-sizeeq, isprefix-append-size,
list/in-append is used by prefix-append-one-sizeeq, isprefix-append-size,
list/in-empty is used by in-prefixn-pos-smaller0, in-prefixn-pos-smaller,
list/in-rec is used by in-prefixn-pos-smaller0, in-prefixn-pos-smaller,
list/len is used by prefixn-split-sublist, prefixn-split-dropn, prefixn-shift-right, prefixn-prefixn, prefixn-eq-prefixn-app, prefixn-eq-append, prefixn-butlast, prefixn-append-slice, prefixn-append-prefix, prefixn-append-left, prefix-prefixn-not-shorter, prefix-append-one-sizeeq, isprefix-eq-size-app-eq1, isprefix-eq-size-app-eq, isprefix-append-size, isprefix-app-size-ls1, isprefix-app-size-ls, isprefix-add-prefixn-size, in-prefixn-samepos, in-prefixn-in-shorter-prefix, dropn-first,
list/len-01 is used by prefixn-prefixn, prefixn-eq-prefixn-app,
list/len-02 is used by prefixn-single-1, prefixn-butlast, prefix-append-one-sizeeq, isprefix-append-size,
list/len-05 is used by prefixn-prepend-one, dropn-first,
list/ni is used by prefix-append-one-sizeeq,
list/rest-01 is used by dropn-first,

Used from specification list-del

list-del/extension is used by isprefix-eq-size-app-eq, isprefix-append-size, isprefix-app-size-ls1, isprefix-add-prefixn-size,
list-del/first-append is used by prefixn-split-sublist, prefixn-split-dropn,
list-del/first-append-01 is used by prefixn-split-dropn,
list-del/firstn-app-01 is used by in-prefixn-in-shorter-prefix,
list-del/firstn-restn-eq is used by prefixn-split-sublist,
list-del/sublist-append is used by prefixn-split-sublist,
list-del/sublist-restn-02 is used by prefixn-split-sublist,
list-del/app-05 is used by in-prefixn-samepos,
list-del/elim-firstn-restn is used by prefixn-split-sublist, prefixn-split-dropn, prefixn-prefixn, prefixn-le-eq, prefixn-eq-prefixn-app, prefixn-eq-append, prefixn-butlast, prefixn-append-slice, prefixn-append-prefix, isprefix-app-prefixn-isprefix, isprefix-add-prefixn-size, in-prefixn-samepos, in-prefixn-in-shorter-prefix, dropn-first,
list-del/first-all is used by prefixn-size-prefixn, prefixn-le-size, prefixn-fulln, prefixn-full-eq, prefixn-full, prefixn-eq-prefixn-app,
list-del/first-all-01 is used by prefixn-full-eq, prefixn-eq-prefixn-app,
list-del/first-append is used by prefixn-append-left,
list-del/first-length is used by prefixn-size-prefixn, prefixn-size-eq, prefixn-len-le-n, prefixn-eq-prefixn-app, isprefix-prefixn,
list-del/firstN-dups-04 is used by prefixn-nodups,
list-del/firstN-empty is used by prefixn-neq-empty-plusone, prefixn-eq-empty,
list-del/firstN-in is used by prefixn-notin, prefixn-in, in-prefixn-in-shorter-prefix,
list-del/firstN-in-04 is used by in-prefixn-in-shorter-prefix,
list-del/firstN-len is used by prefixn-prefixn, prefixn-eq-prefixn-app, prefixn-butlast, prefix-prefixn-exact,
list-del/firstN-zero is used by prefixn-split-dropn, prefixn-eq-empty, prefixn-empty, prefixn-append-slice, prefixn-0, in-prefixn-pos-smaller0, in-prefixn-pos-smaller,
list-del/firstn-allprefix is used by isprefix-prefixn,
list-del/firstn-app is used by prefixn-shift-right, prefixn-append-slice,
list-del/firstn-length-03 is used by prefixn-le-size, prefixn-full-eq, prefix-prefixn-not-shorter,
list-del/firstn-length-04 is used by prefixn-size-prefixn, prefixn-size-eq, prefixn-prefixn, prefixn-len-n, prefixn-len-le-n, prefixn-le-eq,
list-del/firstn-one-02 is used by prefixn-single-1,
list-del/firstn-prefix is used by prefix-prefixn-same,
list-del/firstn-restn-eq is used by prefixn-split-dropn,
list-del/get-append-less is used by isprefix-eq-size-app-eq,
list-del/get-firstn is used by in-prefixn-at-smaller,
list-del/len-01 is used by in-prefixn-pos-smaller0, in-prefixn-pos-smaller,
list-del/pos-e is used by in-prefixn-pos-smaller0, in-prefixn-pos-smaller,
list-del/pos-n is used by in-prefixn-pos-smaller0, in-prefixn-pos-smaller,
list-del/pos-y is used by in-prefixn-pos-smaller0, in-prefixn-pos-smaller,
list-del/rest-len is used by prefixn-split-dropn, prefixn-append-slice,
list-del/restN-append is used by prefixn-split-dropn,
list-del/restN-len is used by dropn-first,
list-del/restN-zero is used by dropn-empty, dropn-0,
list-del/sublist-part is used by prefixn-split-dropn,
list-del/weak-firstN-rec is used by prefixn-prepend-one, in-prefixn-pos-smaller0, in-prefixn-pos-smaller,