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

heapfuns/subset is used by precise-mapex,
heapfuns/at-uni is used by mapex-new,
heapfuns/disj-singleton-write is used by mapex-new,
heapfuns/in-uni is used by mapex-new,
heapfuns/union-add-singleton-left is used by mapex-new,

Used from specification maplet

maplet/map-del is used by mapex-del, map-putex,
maplet/maplet is used by mapex-new, precise-mapex,
maplet/ex is used by mapex-null, precise-mapex, mapex-and,
maplet/ex1-shift is used by mapex-new, mapex-del, map-put, mapex-elim, map-putex, mapex-put, mapex-in,
maplet/map-in is used by map-put, map-putex, mapex-in,
maplet/map-null is used by mapex-null,
maplet/map-put-rw is used by map-putex,
maplet/map-write is used by map-putex, mapex-put,
maplet/maplet is used by mapex-new,

Used from specification heap-sep

heap-sep/and-weaken is used by mapex-and,
heap-sep/precise-alt-def is used by precise-mapex,
heap-sep/sep is used by mapex-new,
heap-sep/false-rev is used by mapex-null,
heap-sep/falseH is used by mapex-null,
heap-sep/imp is used by mapex-and,
heap-sep/precise-emp is used by precise-mapornull,
heap-sep/sep-ass is used by mapex-new, mapex-put-rw, mapex-del, map-put, mapex-elim, map-putex, mapex-put, mapex-in,
heap-sep/sep-com is used by mapex-new, mapex-put-rw, mapex-del, map-put, mapex-elim, map-putex, mapex-put, mapex-in,

Used from specification heap

heap/exin is used by map-putex,
heap/ext is used by mapex-new, precise-mapex,
heap/at-alloc is used by mapex-new,
heap/at-write is used by mapex-new, map-putex, precise-mapex,
heap/del-new is used by map-putex,
heap/in-alloc is used by mapex-new, map-putex, precise-mapex,
heap/in-emp is used by mapex-new, precise-mapex,
heap/in-write is used by mapex-new, map-putex, precise-mapex,
heap/nonnull is used by map-putex, precise-mapex,
heap/overwrite is used by map-putex,
heap/sanity is used by map-putex,
heap/write-again is used by mapex-new,
heap/write-del is used by map-putex,