[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/sep-ass is used by alloc-refset, write-unknown, read-known, free-known, free-unknown, read-unknown, alloc, write-known,
heap-sep/sep-com is used by alloc-refset, write-unknown, read-known, free-known, free-unknown, read-unknown, alloc, write-known,

Used from specification maplet

maplet/at-eq is used by read-known,
maplet/map-in is used by read-known, free-known, write-known,
maplet/map-put-rw is used by write-known,
maplet/mapex-in is used by write-unknown, free-unknown, read-unknown,
maplet/mapex-new-rw is used by alloc-refset, alloc,
maplet/mapex-put-rw is used by write-unknown,

Used from specification heap

heap/dom is used by alloc-refset,

Used from specification separation

separation/free-known is used by free-known,
separation/free-unknown is used by free-unknown,
separation/eq-same is used by free-known, free-unknown,

Used from specification set-union

set-union/refset/subdef is used by alloc-refset,

Used from specification ops-impl

ops-impl/infinite-mem is used by alloc,
ops-impl/infinite-refs is used by alloc-refset,