[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 heap

heap/node-heap/ext is used by apply-empty,
heap/node-heap/at-uni is used by reachable-closed,
heap/node-heap/disj-r is used by reachable-closed,
heap/node-heap/in-alloc is used by dom-alloc,
heap/node-heap/in-emp is used by dom-empty, closed-empty, apply-empty,
heap/node-heap/in-uni is used by reachable-closed,
heap/node-heap/in-write-strong is used by dom-write,
heap/node-heap/subset-in is used by closed-succ-in-subheap,

Used from specification list

list/a is used by reachable-closed, path-last-in, path-first-in, map-path,
list/c is used by reachable-closed, path-last-in, path-first-in, map-path,

Used from specification set-basic

set-basic/refset/Extension is used by ran-put-new, ran-in-heap-eq, ran-empty, dom-write, dom-empty, dom-alloc,
set-basic/refset/In-empty is used by ran-empty, dom-empty,
set-basic/refset/rax is used by ran-put-new, dom-alloc,
set-basic/refset/sub-ntrans-01 is used by map-path,

Used from specification store

store/successors/k-Extension is used by apply-succ-empty,
store/ref-map/At-in-out is used by ran-put-new,
store/successors/Del-at-strong is used by closed-succ-rm,
store/successors/Del-in is used by closed-succ-rm,
store/ref-map/In-empty is used by ran-empty, inj-empty, apply-empty,
store/successors/In-empty is used by closeds-empty, apply-succ-empty,
store/ref-map/In-insert is used by ran-put-new,
store/ref-map/notmemlookup is used by map-path,

Used from specification node

node/elim is used by reachable-closed, path-last-in, map-path, closed-succ,
node/inj is used by map-path, closed-succ,
node/sel-01 is used by reachset-succ, reachable-one, map-path,

Used from specification store+set

store+set/ref-map-store+set-r/Data-in is used by ran-put-new, ran-empty,
store+set/ref-map-store+set-r/Data-in-putsame is used by ran-put-new,
store+set/ref-map-store+set-r/Data-notin-other is used by ran-put-new,
store+set/ref-map-store+set-r/Dom is used by map-path, H-dom-subset,
store+set/ref-map-store+set-r/In-data-in is used by ran-in-heap-eq,

Used from specification set-union

set-union/refset/subdef is used by reachset-succ, map-path, closeds-subset, H-dom-subset,