[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/sep-ass is used by rely-map-write-unknown, rely-map-write-known,
heap-sep/heap-aux/sep-com is used by rely-map-write-unknown, rely-map-write-known,

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 rely-owned-unchgd, owns-one-map,
set-union/refset/int-c is used by rely-owned-unchgd, owns-one-map,
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/size-union is used by rely-owned-unchgd,
set-union/refset/una is used by rely-owned-unchgd, owns-one-map,
set-union/refset/unadd is used by owns-one-map,
set-union/refset/unc is used by rely-owned-unchgd, owns-one-map,
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-reuse, rely-alloc,
set-basic/refset/in is used by rely-reuse, rely-alloc,
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,
set-basic/refset/ne-01 is used by rely-transfer-owner, rely-trans, rely-owns-one, rely-owns-none, rely-owned-unchgd, rely-owned-in-rs, rely-map-write-unknown, rely-map-write-known, owns-one-none, owns-one-map, owns-none-one2, owns-none-one,
set-basic/refset/size-zero-01 is used by rely-transfer-owner, rely-owns-one, rely-owns-none, rely-owned-unchgd, rely-owned-in-rs, rely-map-write-unknown, rely-map-write-known, owns-one-none, owns-one-map, owns-none-one2, owns-none-one,

Used from specification heap-fun

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

Used from specification embed-aux

embed-aux/lift-aux is used by rely-owned-unchgd, owns-one-map,
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 rely-owned-unchgd, owns-one-map,
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,