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

heap-sep/heap-aux-inst/sep-ass is used by rely-map-write-known, rely-map-write-unknown,
heap-sep/heap-aux-inst/sep-com is used by rely-map-write-known, rely-map-write-unknown,

Used from specification set-union

set-union/refset/subdef is used by rely-owned-unchgd,
set-union/refset/One is used by owns-one-map,
set-union/refset/del-addeq-02 is used by owns-one-map,
set-union/refset/del-e-01 is used by owns-one-map,
set-union/refset/diff-int is used by rely-owned-unchgd,
set-union/refset/int-a is used by owns-one-map, rely-owned-unchgd,
set-union/refset/int-c is used by owns-one-map, rely-owned-unchgd,
set-union/refset/int-e is used by owns-one-map,
set-union/refset/intersect-add-rem is used by owns-one-map,
set-union/refset/una is used by owns-one-map, rely-owned-unchgd,
set-union/refset/unadd is used by owns-one-map,
set-union/refset/unc is used by owns-one-map, rely-owned-unchgd,
set-union/refset/une is used by owns-one-map,
set-union/refset/unin-01 is used by rely-owned-unchgd,
set-union/refset/union-difference is used by rely-owned-unchgd,

Used from specification maplet

maplet/maplet-singleton-heap is used by owns-one-map,

Used from specification set-basic

set-basic/refset/In-insert is used by rely-alloc, rely-reuse,
set-basic/refset/in is used by rely-alloc, rely-reuse,
set-basic/refset/in-02 is used by owns-none-one2,
set-basic/refset/in-03 is used by owns-none-one2,
set-basic/refset/in-04 is used by owns-one-map,

Used from specification heap-fun

heap-fun/at-mk is used by owns-one-map,
heap-fun/at-mk is used by rely-owned-unchgd,
heap-fun/in-mk is used by owns-one-map, rely-owned-unchgd,

Used from specification embed-aux

embed-aux/lift-aux is used by owns-one-map, rely-owned-unchgd,
embed-aux/get-known is used by rely-map-write-known,
embed-aux/get-unknown is used by rely-map-write-unknown,

Used from specification heap

heap/ext is used by owns-one-map, rely-owned-unchgd,
heap/at-write is used by owns-one-map,
heap/in-alloc is used by owns-one-map,
heap/in-emp is used by owns-one-map,
heap/in-write is used by owns-one-map,

Used from specification heap-aux

heap-aux/apply is used by owns-one-map, rely-owned-unchgd,
heap-aux/sep is used by owns-one-map, rely-owned-unchgd,
heap-aux/prop-true is used by owns-one-map, rely-owned-unchgd,