[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 butmin-size,
nat-basic/c is used by butmin-size,
nat-basic/one-01 is used by butmin-size,

Used from specification nat

nat/le-add is used by butmin-size,
nat/le-def is used by butmin-size,
nat/leprf is used by size-del-02, size-del,
nat/ler is used by size-del-02,
nat/ls-02 is used by butmin-size,
nat/pred-03 is used by butmin-size-01, butmin-size,

Used from specification set-union

set-union/del-size is used by size-del-02,
set-union/Delete is used by del-01,
set-union/del-in is used by size-del-02,
set-union/del-size is used by size-del, size-del-01,

Used from specification store

store/Del-at is used by butmin-put-01, butmin-rewput,
store/Extension is used by butmin-put-01, butmin-rewput, empty-01,
store/delete-put-rew is used by butmin-put-rew,
store/At-other is used by butmin-put-01, insert-01, butmin-rewput, insert-02,
store/At-same is used by butmin-put-01, butmin-rewput,
store/Del-at is used by butmin-at, butmin-rewput,
store/Del-empty is used by butmin-put, butmin-empty, butmin-one,
store/Del-in is used by del-01, del, butmin-in, butmin-rewput, butmin-notin,
store/Del-notin is used by butmin-rewput,
store/Del-rec-same is used by butmin-put-01, butmin-put, butmin-one, butmin-put-rew,
store/In-empty is used by butmin-in, empty, empty-01,
store/In-insert is used by insert-03,
store/del-put is used by butmin-put-rew,
store/del-putsame is used by butmin-id,
store/empty is used by butmin-size,
store/in-neq is used by butmin-rewput,
store/insin is used by butmin-rewput,
store/lookupisempty is used by butmin-put-01, butmin-rewput,
store/neq is used by min-put-01, butmin-put-01, min, min-put, min-put-ls,
store/notin-del-notin is used by butmin-put-01, butmin-rewput,
store/notmemlookup is used by butmin-put-01, butmin-rewput,
store/size is used by butmin-size-01, butmin-size,

Used from specification set-basic

set-basic/Extension is used by del-01, insert-03, empty, empty-01,
set-basic/In-empty is used by notempty, empty, empty-01,
set-basic/In-insert is used by insert-03, insert-01, insert-02,
set-basic/Size-empty is used by size-del, min-put,
set-basic/eq-03 is used by neq, insert,
set-basic/ne is used by insert-01, insert-02,
set-basic/ne-01 is used by sub, insert-01, insert-02,
set-basic/size-zero is used by mk-in, empty, min-put, insert-01, insert-02,
set-basic/size-zero-01 is used by mk-in, empty, min-put, insert-01, insert-02,
set-basic/size-zero-02 is used by size-del-02, size-del,
set-basic/sub-in is used by sub,

Used from specification oelem

oelem/irreflexivity is used by mk-in, butmin-put-rew, butmin-rewput, min-put-ls, min-def, empty-01,
oelem/sls is used by min-put, butmin-rewput, min-def,
oelem/transitivity is used by min-put,

Used from specification oset

oset/Min-min is used by min-def,
oset/min-ins-01 is used by min-put,
oset/min-ins-03 is used by min-put-ls,
oset/min-insert is used by min-put,
oset/min-inn is used by mk-in, min-put,
oset/min-one is used by min, min-put,