[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 map-sep

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

Used from specification heapfuns-map

heapfuns-map/at-uni is used by at-rw,
heapfuns-map/del-uni is used by map-del,
heapfuns-map/disj-singleton-write is used by map-same, map-in, map-del, map-write, map-put-rw,
heapfuns-map/in-uni is used by map-in, at-rw, map-put-rw,
heapfuns-map/uni-emp-l is used by map-del,
heapfuns-map/union-add-singleton-left is used by map-write, map-put-rw,
heapfuns-map/union-left-singleton is used by map-del,

Used from specification map

map/Del-empty is used by map-del,
map/Del-in is used by map-del,
map/Del-rec-same is used by map-del,
map/In-insert is used by map-same, map-in, map-in0, at-rw, map-put-rw,
map/eq-put2 is used by map-del,
map/inj-put is used by map-put-rw,
map/k-At-same is used by at-rw-singleton, at-rw,
map/notin-del-notin is used by map-del,
map/put-neq is used by map-write,
map/put-same is used by map-put-rw,