[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/Difference
is used by
restrict-in,
restrict-at,
dom-restrict,
dom-rem,
- set-union/Intersect
is used by
restrict-intersect-empty,
in-dom-inter,
- set-union/del-e-02
is used by
restrict-intersect-empty-write-add,
- set-union/del-rax
is used by
dom-del,
- set-union/diff-e
is used by
restrict-empty,
- set-union/int-a
is used by
restrict-intersect-empty-write-add,
restrict-intersect-empty,
in-dom-inter,
- set-union/int-c
is used by
restrict-intersect-empty-write-add,
restrict-intersect-empty,
in-dom-inter,
- set-union/intersect-add-rem
is used by
restrict-intersect-empty-write-add,
Used from specification store
- store/At-other
is used by
rem-write-other,
- store/Del-at
is used by
Diff-get,
- store/Del-in
is used by
Diff-ext,
Diff-del-rw,
- store/Extension
is used by
restrict-intersect-empty,
restrict-empty,
rem-write-other,
rem-write,
dom-isemp,
- store/k-Extension
is used by
oplus-shift-put-l,
oplus-empty,
empty-oplus,
Diff-del-rw,
Diff-Diff-com,
- store/notin-del-notin
is used by
diff-add-notin,
- store/notmemlookup
is used by
Diff-mems-get,
- store/At-in-out
is used by
Data-in-other,
- store/At-other
is used by
rem-write,
oplus-shift-put-l,
Data-notin-other-3,
Data-notin-other-2,
Data-notin-other,
Data-in-putdelput,
Data-in-putdel,
Data-in-delput-2,
Data-in-delput,
- store/At-same
is used by
rem-write,
oplus-shift-put-l,
Data-notin-other-3,
Data-notin-other-2,
Data-notin-other,
Data-in-putsame,
Data-in-puteq,
Data-in-putdelput,
Data-in-putdel,
Data-in-other,
Data-in-delput-2,
Data-in-delput,
- store/Del-at
is used by
diff-get-add,
Data-in-putdelput,
Data-in-putdel,
- store/Del-at-strong
is used by
Diff-del-rw,
Data-in-putdelput,
Data-in-putdel,
Data-in-delput-2,
Data-in-delput,
Data-in-del,
- store/Del-in
is used by
dom-del,
Diff-del-rw,
Data-in-putdelput,
Data-in-putdel,
Data-in-delput-2,
Data-in-delput,
Data-in-del,
- store/Del-notin
is used by
Diff-del-rw,
- store/In-empty
is used by
restrict-empty,
oplus-empty,
empty-oplus,
dom-isemp,
- store/In-insert
is used by
rem-write-other,
oplus-shift-put-l,
dom-ins,
Data-in-other,
- store/deldel
is used by
diff-add-rem,
- store/empty-01
is used by
Diff-empty,
- store/in-neq
is used by
rem-write,
oplus-shift-put-l,
dom-ins,
Data-notin-other-3,
Data-notin-other-2,
Data-notin-other,
Data-in-putdelput,
Data-in-putdel,
Data-in-delput-2,
Data-in-delput,
- store/insert
is used by
Diff-mod,
- store/insin
is used by
rem-write,
oplus-shift-put-l,
Data-in-putsame,
Data-in-puteq,
Data-in-other,
- store/lookupisempty
is used by
Diff-get,
Data-in-putdelput,
- store/notmemlookup
is used by
restrict-intersect-empty,
restrict-empty,
dom-isemp,
Used from specification set-basic
- set-basic/Extension
is used by
restrict-intersect-empty,
dom-union-l,
dom-restrict,
dom-rem,
dom-isemp,
dom-ins,
dom-del,
- set-basic/In-empty
is used by
restrict-intersect-empty,
dom-isemp,
Diff-ext,
- set-basic/add
is used by
Diff-get,
- 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
restrict-intersect-empty,
restrict-at,
rem-write-other,
rem-write,
dom-restrict,
Diff-mems-get,
- set-basic/rax
is used by
dom-ins,
Diff-ext,
- set-basic/size-zero-01
is used by
restrict-intersect-empty,
restrict-at,
rem-write-other,
Diff-mems-get,
- set-basic/sub-in
is used by
dom-restrict,