[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/del-in is used by restrict-add-not-in,
set-union/disjoint-diff is used by restrict-diff,
set-union/Delete is used by dom-del, restrict-at-insert, restrict-at-insert-tw0, restrict-del,
set-union/Difference is used by dom-rem, restrict-add-not-in, dom-restrict, dom-restrict-intersect, restrict-in, restrict-at, in-dom-diff, restrict-subset, restrict-del,
set-union/Intersect is used by in-dom-inter, dom-restrict-intersect, restrict-intersect-empty,
set-union/del-e-02 is used by restrict-intersect-empty-write-add,
set-union/diff-add-del is used by restrict-add-not-in, restrict-at-insert, restrict-at-insert-tw0,
set-union/diff-del-plus-1 is used by restrict-diff, restrict-subset,
set-union/diff-del-plus-2 is used by restrict-diff,
set-union/diff-diff-right is used by dom-restrict-intersect,
set-union/diff-e is used by restrict-empty,
set-union/diff-e-01 is used by restrict-diff, restrict-subset,
set-union/diff-idem is used by restrict-dom,
set-union/disjoint-diff1 is used by restrict-diff,
set-union/int-a is used by in-dom-inter, restrict-intersect-empty-write-add, dom-restrict-intersect, restrict-intersect-empty,
set-union/int-c is used by in-dom-inter, restrict-intersect-empty-write-add, dom-restrict-intersect, restrict-intersect-empty,
set-union/intersect-add-rem is used by restrict-intersect-empty-write-add,
set-union/una is used by diff-union,
set-union/unadd is used by diff-union,
set-union/unc is used by diff-union,
set-union/une is used by diff-union,

Used from specification set-basic

set-basic/Extension is used by dom-del, dom-rem, dom-isemp, dom-union-l, dom-restrict, dom-restrict-intersect, restrict-intersect-empty, in-dom-diff, dom-ins, in-dom-eq,
set-basic/In-empty is used by dom-isemp, restrict-intersect-empty, Diff-ext,
set-basic/In-insert is used by Diff-get, dom-ins, Diff-ext,
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 Diff-mems-get, dom-restrict, restrict-intersect-empty, rem-write-other, restrict-diff, restrict-at, restrict-subset, restrict-del,
set-basic/size-zero-01 is used by Diff-mems-get, restrict-intersect-empty, rem-write-other, restrict-diff, restrict-at, restrict-subset, restrict-del,
set-basic/sub-add-03 is used by restrict-subset,
set-basic/sub-in is used by dom-restrict,

Used from specification map

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