[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 set-union

set-union/del-rax is used by del-01,
set-union/del-size is used by size-del-01, size-del,
set-union/size-del-leq is used by size-del-02,

Used from specification nat

nat/lels-01 is used by size-del, butmin-size,
nat/ls-02 is used by size-del, butmin-size,
nat/pred-03 is used by butmin-size-01, butmin-size,
nat/succ-01 is used by size-del, butmin-size,

Used from specification store

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

Used from specification set-basic

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

Used from specification nat-basic2

nat-basic2/a is used by size-del, butmin-size,
nat-basic2/c is used by size-del, butmin-size,

Used from specification oelem

oelem/irreflexivity is used by mk-in, min-put-ls, min-def, butmin-rewput, butmin-put-rew,
oelem/sls is used by min-put, min-def, butmin-rewput, butmin-in,
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-put, min,

Used from specification nat-basic1

nat-basic1/one-01 is used by size-del, butmin-size,
nat-basic1/ref-1 is used by size-del, butmin-size,