[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/Difference is used by dom-restrict,
set-union/Union is used by dom-union-l,
set-union/Delete is used by dom-del,
set-union/Difference is used by dom-restrict, dom-rem, restrict-at, restrict-in,
set-union/Intersect is used by in-dom-inter, restrict-intersect-empty,
set-union/del-e-02 is used by restrict-intersect-empty-write-add,
set-union/diff-e is used by restrict-empty,
set-union/int-a is used by in-dom-inter, restrict-intersect-empty-write-add, restrict-intersect-empty,
set-union/int-c is used by in-dom-inter, restrict-intersect-empty-write-add, restrict-intersect-empty,
set-union/intersect-add-rem is used by restrict-intersect-empty-write-add,

Used from specification set-basic

set-basic/Extension is used by dom-restrict, dom-union-l, dom-del, dom-rem, restrict-intersect-empty, dom-ins, dom-isemp, in-dom-eq,
set-basic/In-empty is used by Diff-ext, restrict-intersect-empty, dom-isemp,
set-basic/In-insert is used by Diff-get, Diff-ext, dom-ins,
set-basic/eq-03 is used by dom-add-in,
set-basic/in-02 is used by Diff-get,
set-basic/ne-01 is used by dom-restrict, Diff-mems-get, rem-write-other, restrict-intersect-empty, restrict-at,
set-basic/size-zero-01 is used by Diff-mems-get, rem-write-other, restrict-intersect-empty, restrict-at,
set-basic/sub-in is used by dom-restrict,

Used from specification store

store/At-other is used by rem-write-other,
store/Del-at is used by Diff-get, Diff-del-rw,
store/Del-in is used by Diff-ext, Diff-del-rw,
store/Del-rec-same is used by Diff-mod,
store/Extension is used by restrict-empty, rem-write-other, rem-write, restrict-intersect-empty, dom-isemp,
store/Subset is used by diff-subset,
store/k-Extension is used by Diff-Diff-com, Diff-del-rw,
store/notin-del-notin is used by diff-add-notin,
store/notmemlookup is used by Diff-mems-get,
store/sw-01 is used by Diff-rec-rev,
store/At-in-out is used by Data-in-other,
store/At-other is used by Data-in-delput-2, Data-notin-other-2, Data-notin-other-3, Data-in-putdelput, rem-write, Data-in-delput, Data-in-putdel, Data-notin-other,
store/At-same is used by Data-in-delput-2, Data-notin-other-2, Data-notin-other-3, Data-in-putdelput, rem-write, Data-in-delput, Data-in-putdel, Data-in-other, Data-in-putsame, Data-in-puteq, Data-notin-other,
store/Del-at is used by Data-in-delput-2, Data-in-putdelput, Data-in-del, diff-get-add, Data-in-delput, Data-in-putdel, Diff-del-rw,
store/Del-empty is used by Diff-empty,
store/Del-in is used by Data-in-delput-2, Data-in-putdelput, dom-del, Data-in-del, Data-in-delput, Data-in-putdel, Diff-del-rw,
store/In-empty is used by restrict-empty, dom-isemp,
store/In-insert is used by rem-write-other, Data-in-other, dom-ins,
store/deldel is used by diff-add-rem,
store/in-neq is used by Data-in-delput-2, Data-notin-other-2, Data-notin-other-3, Data-in-putdelput, rem-write, Data-in-delput, Data-in-putdel, Data-notin-other,
store/insin is used by rem-write, Data-in-other, Data-in-putsame, Data-in-puteq,
store/lookupisempty is used by Diff-get, Diff-del-rw,
store/notmemlookup is used by restrict-empty, restrict-intersect-empty, dom-isemp,