[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/at-uni is used by map-del-sharing, at-eq-sharing,
heapfuns/in-uni is used by map-del-sharing,
heapfuns/subset is used by maplet-unique,
heapfuns/write-left is used by map-put-rw,
heapfuns/at-uni is used by map-del-sharing, at-eq-sharing, at-rw,
heapfuns/del-uni is used by map-del-sharing, map-del,
heapfuns/disj-distr-uni is used by at-eq-sharing,
heapfuns/disj-emp-l is used by map-del-sharing,
heapfuns/disj-emp-r is used by map-del-sharing,
heapfuns/disj-l is used by map-del-sharing,
heapfuns/disj-r is used by map-del-sharing, at-eq-sharing,
heapfuns/disj-singleton-write is used by map-in, map-put-rw, map-del-sharing, map-same, map-del, map-write,
heapfuns/disj-write is used by map-del-sharing,
heapfuns/in-uni is used by map-in, map-del-sharing, at-eq-sharing, at-rw,
heapfuns/uni-emp is used by map-del-sharing,
heapfuns/uni-emp-l is used by map-del-sharing, map-del,
heapfuns/union-left-singleton is used by map-del-sharing, map-del,
heapfuns/union-left-singleton-at is used by map-write,

Used from specification heap-sep

heap-sep/Imp is used by ex2-shiftwr-impl, ex3-shiftwr-impl, ex1-shiftwr-impl,
heap-sep/precise is used by precise-map,
heap-sep/sep is used by ex1-shift, map-in, ex3-shiftw-inst, ex2-shiftw-inst, ex1-shiftw-inst, ex3-shift, map-put-rw, map-same, map-del, map-write, at-rw, ex2-shift,
heap-sep/sharing is used by map-del-sharing, at-eq-sharing,
heap-sep/split-union is used by ex1-shift, ex3-shiftw-inst, ex2-shiftw-inst, ex1-shiftw-inst, ex3-shift, ex2-shift,
heap-sep/wand is used by ex1-shiftwr, ex2-shiftwr, ex2-shiftw, ex3-shiftwr, ex3-shiftw, ex1-shiftw,
heap-sep/false-rev is used by map-null,
heap-sep/falseH is used by map-null, map-same,
heap-sep/sep-ass is used by ex1-shift, ex3-shiftw-inst, ex2-shiftw-inst, ex3-shift, map-put-rw, map-del, eq-objs, ex2-shift,
heap-sep/sep-com is used by ex1-shift, ex3-shiftw-inst, ex2-shiftw-inst, ex3-shift, map-put-rw, map-del, eq-objs, ex2-shift,
heap-sep/sharing-ass is used by map-del-sharing, at-eq-sharing, at-rw-sharing,
heap-sep/sharing-com is used by map-del-sharing, at-eq-sharing, at-rw-sharing,
heap-sep/split-union is used by ex1-shift, ex3-shift, ex2-shift,

Used from specification heap

heap/ext is used by map-del-sharing, at-eq-sharing, map-write,
heap/at-del is used by map-del-sharing,
heap/at-write is used by at-rw-singleton, map-del-sharing, at-eq-sharing, maplet-unique, map-write, at-rw,
heap/del-new is used by map-del-sharing, map-del,
heap/del-notin is used by map-del-sharing, map-del,
heap/in-alloc is used by map-in, map-in0, at-rw-singleton, map-put-rw, map-del-sharing, map-same, at-eq-sharing, map-del, maplet-unique, at-rw,
heap/in-del is used by map-del-sharing, map-del,
heap/in-emp is used by map-in, map-in0, at-rw-singleton, map-put-rw, map-del-sharing, map-same, at-eq-sharing, map-del, maplet-unique, at-rw,
heap/in-write is used by map-in, map-in0, map-put-rw, map-del-sharing, map-same, at-eq-sharing, maplet-unique, map-write,
heap/nonnull is used by map-put-rw, map-del-sharing, at-eq-sharing, map-del, maplet-unique, map-write,
heap/overwrite is used by map-put-rw,
heap/put-eq is used by map-del-sharing,
heap/write-del is used by map-del-sharing, map-del,