[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-del

list-del/partition/get-append-grt is used by resetcount-elem, NEWPARTS-theorem,
list-del/partition/get-append-less is used by resetcnt-mod-cnt, NEWPARTS-theorem,
list-del/partition/get-in is used by NEWPARTS-theorem,
list-del/partition/get-numrec is used by partitions-mod-count, Fok-mod-cnt,
list-del/partition/get-rec is used by NEWPARTS-theorem,
list-del/partition/get-zero is used by NEWPARTS-theorem,
list-del/partition/in-get is used by REFINEONE-theorem, NEWPARTS-theorem,
list-del/partition/put-at is used by partitions-mod-count, REFINEONE-theorem, Fok-mod-cnt,
list-del/partition/put-length is used by REFINEONE-theorem,
list-del/partition/put-rec-02 is used by partitions-mod-count, Fok-mod-cnt,
list-del/partition/get-app is used by NEWPARTS-theorem,
list-del/partition/get-append-grt is used by resetcnt-mod-cnt, NEWPARTS-theorem,
list-del/partition/get-append-grt-02 is used by NEWPARTS-theorem,
list-del/partition/get-append-less is used by resetcount-elem, NEWPARTS-theorem,
list-del/partition/get-in is used by REFINEONE-theorem,
list-del/partition/get-last-03 is used by NEWPARTS-theorem,
list-del/partition/get-succ is used by resetcount-elem, partitions-mod-count, NEWPARTS-theorem, Fok-mod-cnt,
list-del/partition/get-zero-01 is used by resetcount-elem, partitions-mod-count, NEWPARTS-theorem, Fok-mod-cnt,
list-del/partition/one-03 is used by resetcount-elem, resetcnt-mod-cnt, NEWPARTS-theorem, Fok-mod-cnt,
list-del/partition/put-app-left is used by resetcnt-mod-cnt,
list-del/partition/put-at-eq is used by partitions-mod-count, REFINEONE-theorem, Fok-mod-cnt,
list-del/partition/put-length is used by partitions-mod-count, REFINEONE-theorem, Fok-mod-cnt,
list-del/partition/put-one is used by resetcnt-mod-cnt, Fok-mod-cnt,
list-del/partition/put-succ is used by resetcnt-mod-cnt,
list-del/partition/put-zero is used by partitions-mod-count, Fok-mod-cnt,

Used from specification array

array/array_of_nat/Put-other is used by REFINEONE-theorem,
array/array_of_nat/Put-same is used by REFINEONE-theorem,
array/array_of_nat/Size-put is used by REFINEONE-theorem,
array/array_of_nat/cgetput is used by REFINEONE-theorem,
array/array_of_nat/ngp-06 is used by REFINEONE-theorem,

Used from specification nat-basic1

nat-basic1/f is used by split-init-2, resetcnt-mod-cnt, partitions-mod-count, one-oc, nodups-oc-2, nodups-oc, nodups-numoc, no-oc, elem-does-occur, REFINEONE-theorem, REFINE-theorem, NEWPARTS-theorem, Fok-mod-cnt, Fok-lem,
nat-basic1/lf is used by partitions-mod-count, nodups-oc-2, nodups-oc, REFINEONE-theorem, NEWPARTS-theorem, Fok-mod-cnt,
nat-basic1/lf-01 is used by partitions-mod-count, nodups-oc, REFINEONE-theorem, NEWPARTS-theorem,
nat-basic1/lf-02 is used by partitions-mod-count, one-oc, nodups-oc, nodups-numoc, REFINEONE-theorem, NEWPARTS-theorem, Fok-mod-cnt,
nat-basic1/ls-02 is used by one-oc, nodups-oc, no-oc, REFINEONE-theorem, NEWPARTS-theorem,
nat-basic1/ls-03 is used by REFINEONE-theorem,
nat-basic1/neq-01 is used by one-oc, REFINEONE-theorem, NEWPARTS-theorem,
nat-basic1/one is used by nodups-perm, nodups-numoc, NEWPARTS-theorem,
nat-basic1/one-01 is used by resetcount-elem, resetcnt-mod-cnt, NEWPARTS-theorem, Fok-mod-cnt,
nat-basic1/ref-1 is used by one-oc, no-oc, REFINEONE-theorem, REFINE-theorem, NEWPARTS-theorem,
nat-basic1/trans-1 is used by partitions-mod-count, nodups-oc-2, nodups-oc, REFINEONE-theorem, NEWPARTS-theorem, Fok-mod-cnt,
nat-basic1/zero is used by nodups-oc, NEWPARTS-theorem,
nat-basic1/zero-01 is used by split-init-2, resetcnt-mod-cnt, one-oc, nodups-oc, no-oc, Fok-mod-cnt,

Used from specification partelem

partelem/inj is used by NEWPARTS-theorem,
partelem/sel-03 is used by REFINEONE-theorem,
partelem/sel-04 is used by REFINEONE-theorem,
partelem/sel-05 is used by REFINEONE-theorem,
partelem/elim is used by startorfin-reset, split-init-2, partitions-mod-count, REFINEONE-theorem, REFINE-theorem, NEWPARTS-theorem, MAIN-theorem, Fok-lem,
partelem/inj is used by resetcount-elem, partitions-mod-count, REFINEONE-theorem,
partelem/sel-03 is used by startorfin-reset, split-init-2, partitions-mod-count, in-mod-count, REFINEONE-theorem, REFINE-theorem, NEWPARTS-theorem, Fok-lem,
partelem/sel-04 is used by startorfin-reset, partitions-mod-count, in-mod-count, REFINEONE-theorem, NEWPARTS-theorem, Fok-lem,
partelem/sel-05 is used by split-init-2, REFINEONE-theorem, REFINE-theorem, NEWPARTS-theorem, MAIN-theorem,
partelem/upd-03 is used by resetcount-elem, resetcnt-mod-cnt, resetcnt-idem, member-reset, REFINEONE-theorem, REFINE-theorem,

Used from specification nat-basic2

nat-basic2/a is used by split-init-2, resetcount-elem, resetcnt-mod-cnt, resetcnt-length, partitions-mod-count, one-oc, nodups-oc, no-oc, REFINEONE-theorem, REFINE-theorem, NEWPARTS-theorem, Fok-mod-cnt,
nat-basic2/ax-08 is used by split-init-2, one-oc, nodups-oc, no-oc, REFINE-theorem, NEWPARTS-theorem,
nat-basic2/between is used by NEWPARTS-theorem,
nat-basic2/c is used by split-init-2, resetcount-elem, resetcnt-mod-cnt, resetcnt-length, partitions-mod-count, one-oc, nodups-oc, no-oc, REFINEONE-theorem, REFINE-theorem, NEWPARTS-theorem, Fok-mod-cnt,
nat-basic2/eq is used by NEWPARTS-theorem,
nat-basic2/eq-01 is used by resetcnt-length, REFINEONE-theorem, NEWPARTS-theorem,
nat-basic2/eq-inc-neq is used by NEWPARTS-theorem,
nat-basic2/eqs is used by NEWPARTS-theorem,
nat-basic2/l is used by REFINEONE-theorem, NEWPARTS-theorem,
nat-basic2/l-01 is used by REFINEONE-theorem, NEWPARTS-theorem,
nat-basic2/l-02 is used by NEWPARTS-theorem,
nat-basic2/neq-01 is used by NEWPARTS-theorem,
nat-basic2/nls-fst is used by nodups-oc,
nat-basic2/one is used by one-oc, nodups-oc,
nat-basic2/one-03 is used by one-oc,
nat-basic2/oz is used by resetcount-elem, resetcnt-mod-cnt, partitions-mod-count, no-oc, REFINEONE-theorem, NEWPARTS-theorem, Fok-mod-cnt,
nat-basic2/s is used by resetcnt-mod-cnt, partitions-mod-count, one-oc, nodups-oc, no-oc, REFINEONE-theorem, REFINE-theorem, NEWPARTS-theorem, Fok-mod-cnt,
nat-basic2/succ is used by one-oc, nodups-oc-2, nodups-oc, no-oc, REFINEONE-theorem, NEWPARTS-theorem, Fok-mod-cnt,
nat-basic2/succ-03 is used by REFINEONE-theorem, NEWPARTS-theorem,
nat-basic2/z-01 is used by nodups-oc, no-oc,

Used from specification array-perm

array-perm/array_of_nat/perm-def is used by nodups-perm,
array-perm/array_of_nat/perm-swap is used by REFINEONE-theorem,
array-perm/array_of_nat/nonzero-numoc is used by elem-below-occurs,
array-perm/array_of_nat/numoc-base is used by one-oc, nodups-oc, no-oc,
array-perm/array_of_nat/numoc-rec is used by one-oc, nodups-oc, no-oc,
array-perm/array_of_nat/perm-refl is used by REFINEONE-theorem, REFINE-theorem,
array-perm/array_of_nat/perm-trans is used by REFINE-theorem,

Used from specification list

list/partition/Last is used by NEWPARTS-theorem,
list/list_of_nat/Last is used by REFINEONE-theorem, REFINE-theorem,
list/partition/Nil is used by NEWPARTS-theorem,
list/list_of_nat/a is used by REFINEONE-theorem, REFINE-theorem,
list/partition/a is used by split-init-2, resetcount-elem, resetcnt-mod-cnt, resetcnt-length, resetcnt-idem, partitions-mod-count, member-reset, divides-reset, divides-XornoX-head, REFINE-theorem, NEWPARTS-theorem, Fok-mod-cnt,
list/partition/app is used by resetcnt-mod-cnt, NEWPARTS-theorem, Fok-mod-cnt,
list/list_of_nat/app is used by REFINE-theorem,
list/partition/app-01 is used by resetcnt-mod-cnt,
list/partition/app-02-ant is used by NEWPARTS-theorem,
list/list_of_nat/app-03 is used by REFINE-theorem,
list/partition/app-03 is used by resetcnt-mod-cnt, NEWPARTS-theorem,
list/partition/app-05 is used by NEWPARTS-theorem,
list/list_of_nat/app-05 is used by REFINE-theorem,
list/partition/c is used by split-init-2, resetcount-elem, resetcnt-mod-cnt, resetcnt-length, resetcnt-idem, partitions-mod-count, member-reset, divides-reset, REFINE-theorem, NEWPARTS-theorem, Fok-mod-cnt,
list/list_of_nat/c is used by REFINE-theorem,
list/partition/c-04 is used by resetcnt-mod-cnt,
list/partition/c-06 is used by resetcnt-idem, REFINE-theorem,
list/partition/e is used by NEWPARTS-theorem,
list/partition/e-01 is used by resetcnt-mod-cnt, partitions-mod-count, NEWPARTS-theorem, Fok-mod-cnt,
list/list_of_nat/e-01 is used by REFINE-theorem,
list/partition/e-02 is used by NEWPARTS-theorem,
list/partition/e-03 is used by NEWPARTS-theorem,
list/partition/first-02 is used by NEWPARTS-theorem,
list/partition/fr is used by NEWPARTS-theorem,
list/partition/in-06 is used by member-reset,
list/partition/in-14 is used by NEWPARTS-theorem,
list/partition/in-15 is used by NEWPARTS-theorem,
list/list_of_nat/in-17 is used by REFINEONE-theorem,
list/partition/in-17 is used by split-init-2, member-reset, divides-reset, divides-XornoX-head, REFINE-theorem, NEWPARTS-theorem,
list/list_of_nat/in-append is used by REFINEONE-theorem,
list/partition/in-append is used by split-init-2, member-reset, divides-reset, divides-XornoX-head, REFINE-theorem, NEWPARTS-theorem,
list/list_of_nat/in-empty is used by split-init-2, REFINE-theorem,
list/partition/in-empty is used by split-init-2, member-reset, empty-divides, NEWPARTS-theorem,
list/partition/inapp-02 is used by NEWPARTS-theorem,
list/partition/len is used by resetcnt-mod-cnt, resetcnt-length, partitions-mod-count, NEWPARTS-theorem, Fok-mod-cnt,
list/list_of_nat/len is used by REFINE-theorem,
list/partition/len-02 is used by resetcount-elem, resetcnt-mod-cnt, resetcnt-length, partitions-mod-count, NEWPARTS-theorem, Fok-mod-cnt,
list/list_of_nat/len-02 is used by REFINE-theorem,

Used from specification list-data

list-data/list_of_nat/elim-list-c is used by REFINE-theorem,
list-data/partition/elim-list-c is used by NEWPARTS-theorem,
list-data/partition/l is used by resetcnt-mod-cnt, partitions-mod-count, REFINEONE-theorem, NEWPARTS-theorem, Fok-mod-cnt, Fok-lem,
list-data/partition/length-rest is used by NEWPARTS-theorem,
list-data/partition/size-01 is used by split-init-2, resetcnt-mod-cnt, resetcnt-length, Fok-mod-cnt,

Used from specification nat

nat/one-02 is used by nodups-numoc,
nat/add-num-03 is used by NEWPARTS-theorem,
nat/anti is used by one-oc, nodups-oc, no-oc, REFINEONE-theorem, NEWPARTS-theorem,
nat/cancel-01 is used by NEWPARTS-theorem,
nat/elim-pred-c is used by resetcount-elem, resetcnt-mod-cnt, partitions-mod-count, NEWPARTS-theorem, Fok-mod-cnt,
nat/elim-sub is used by NEWPARTS-theorem,
nat/eq is used by NEWPARTS-theorem,
nat/eq-01 is used by NEWPARTS-theorem,
nat/eqle-one is used by REFINEONE-theorem, NEWPARTS-theorem, Fok-mod-cnt,
nat/fle is used by partitions-mod-count, REFINEONE-theorem, NEWPARTS-theorem,
nat/fle-01 is used by partitions-mod-count, nodups-oc, REFINEONE-theorem, NEWPARTS-theorem, Fok-lem,
nat/l-num-01 is used by NEWPARTS-theorem,
nat/le-add is used by REFINEONE-theorem, NEWPARTS-theorem,
nat/le-ls-simp is used by partitions-mod-count, nodups-oc, REFINEONE-theorem, NEWPARTS-theorem, Fok-mod-cnt,
nat/le-one is used by REFINEONE-theorem, NEWPARTS-theorem,
nat/lels is used by resetcnt-mod-cnt, partitions-mod-count, one-oc, nodups-oc, no-oc, REFINEONE-theorem, NEWPARTS-theorem, Fok-mod-cnt,
nat/lels-01 is used by partitions-mod-count, nodups-perm, nodups-numoc, REFINEONE-theorem, NEWPARTS-theorem,
nat/lels-02 is used by nodups-oc, NEWPARTS-theorem,
nat/lels-03 is used by one-oc, nodups-oc, REFINEONE-theorem, NEWPARTS-theorem,
nat/lels-04 is used by REFINEONE-theorem,
nat/lep is used by REFINEONE-theorem, NEWPARTS-theorem,
nat/lep-02 is used by REFINEONE-theorem, NEWPARTS-theorem,
nat/ler is used by elem-does-occur, REFINEONE-theorem, NEWPARTS-theorem,
nat/les is used by REFINEONE-theorem, NEWPARTS-theorem,
nat/let is used by partitions-mod-count, REFINEONE-theorem, NEWPARTS-theorem, Fok-lem,
nat/lez is used by resetcnt-mod-cnt, partitions-mod-count, nodups-oc, NEWPARTS-theorem, Fok-mod-cnt,
nat/lez-01 is used by resetcnt-mod-cnt, Fok-mod-cnt,
nat/ls-01 is used by NEWPARTS-theorem,
nat/ls-le-simp is used by split-init-2, partitions-mod-count, REFINEONE-theorem, REFINE-theorem, NEWPARTS-theorem, Fok-mod-cnt,
nat/not-zero is used by Fok-mod-cnt,
nat/one-02 is used by nodups-perm,
nat/pred-03 is used by partitions-mod-count, NEWPARTS-theorem, Fok-mod-cnt,
nat/succ-01 is used by resetcnt-mod-cnt, partitions-mod-count, nodups-oc, REFINEONE-theorem, NEWPARTS-theorem, Fok-mod-cnt,
nat/zero is used by NEWPARTS-theorem,

Used from specification set-union

set-union/set_of_nat/Difference is used by NEWPARTS-theorem,
set-union/set_of_nat/Intersect is used by NEWPARTS-theorem,
set-union/set_of_nat/subdef is used by NEWPARTS-theorem,
set-union/set_of_nat/int-a is used by NEWPARTS-theorem,
set-union/set_of_nat/int-c is used by NEWPARTS-theorem,
set-union/set_of_nat/int-eq is used by NEWPARTS-theorem,

Used from specification store

store/map_nat_nat/At-other is used by REFINEONE-theorem,
store/map_nat_nat/At-same is used by REFINEONE-theorem,
store/map_nat_nat/In-insert is used by REFINEONE-theorem,
store/map_nat_nat/in-neq is used by REFINEONE-theorem,
store/map_nat_nat/ins-same-01 is used by REFINEONE-theorem,
store/map_nat_nat/insin is used by REFINEONE-theorem,
store/map_nat_nat/k-At-same is used by REFINEONE-theorem,

Used from specification set-basic

set-basic/set_of_nat/Extension is used by REFINEONE-theorem, NEWPARTS-theorem,