[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/and-weaken is used by mapex-and,
heap-sep/precise is used by precise-mapornull, precise-mapex, precise-map,
heap-sep/sep is used by at-rw, ex1-shiftw-inst, ex2-shiftw-inst, ex3-shiftw-inst, mapex-new, ex1-shift, mapex-del, map-same, ex2-shift, map-putex, map-write, map-in, ex3-shift, map-del,
heap-sep/split-union is used by ex1-shiftw-inst, ex2-shiftw-inst, ex3-shiftw-inst, ex1-shift, ex2-shift, ex3-shift,
heap-sep/wand is used by ex3-shiftw, ex1-shiftw, ex2-shiftw,
heap-sep/false-rev is used by map-null, mapex-null,
heap-sep/falseH is used by map-same, map-null, 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-put-rw, map-put-rw, mapex-new-rw, mapex-new, ex1-shift, mapex-del, mapex-elim, map-put, ex2-shift, map-putex, mapex-put, ex3-shift, map-del, mapex-in,
heap-sep/sep-com is used by mapex-put-rw, map-put-rw, mapex-new-rw, mapex-new, ex1-shift, mapex-del, mapex-elim, map-put, ex2-shift, map-putex, mapex-put, ex3-shift, map-del, mapex-in,
heap-sep/split-union is used by ex1-shift, ex2-shift, ex3-shift,

Used from specification heap

heap/at-alloc is used by mapex-new,
heap/at-uni is used by mapex-new,
heap/exin is used by map-putex,
heap/ext is used by mapex-new, precise-mapornull, precise-mapex, map-write,
heap/in-uni is used by mapex-new, precise-mapornull, precise-mapex,
heap/write-left is used by map-putex,
heap/at-uni is used by at-rw, mapex-new, map-del,
heap/at-write is used by at-rw, mapex-new, map-putex, map-write, map-del,
heap/del-new is used by mapex-del, map-putex, map-del,
heap/del-notin is used by mapex-del, map-del,
heap/del-uni is used by mapex-del, map-del,
heap/disj-singleton-write is used by mapex-new, mapex-del, map-same, precise-mapornull, precise-mapex, map-putex, map-write, map-in, map-del,
heap/in-alloc is used by at-rw, mapex-new, mapex-del, map-same, precise-mapornull, precise-mapex, map-putex, map-in, map-del, map-in0,
heap/in-del is used by map-del,
heap/in-emp is used by at-rw, mapex-new, mapex-del, map-same, precise-mapornull, precise-mapex, map-putex, map-in, map-del, map-in0,
heap/in-uni is used by at-rw, mapex-new, map-in, map-del,
heap/in-write is used by mapex-new, map-same, precise-mapornull, precise-mapex, map-putex, map-write, map-in, map-del, map-in0,
heap/nonnull is used by mapex-new, map-putex, map-write, map-del,
heap/overwrite is used by map-putex,
heap/sanity is used by map-putex,
heap/uni-emp-l is used by mapex-del, map-del,
heap/union-left-singleton is used by map-del,
heap/union-left-singleton-at is used by precise-mapornull, precise-mapex, map-write,
heap/write-del is used by mapex-del, map-putex, map-del,