[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/and-weaken is used by mapex-and,
map-sep/precise-alt-def is used by precise-mapex,
map-sep/imp is used by mapex-and,
map-sep/sep-ass is used by map-add, mapex-put-rw, mapex-del, map-put, mapex-elim, map-putex, mapex-put, mapex-in,
map-sep/sep-com is used by map-add, mapex-put-rw, mapex-del, map-put, mapex-elim, map-putex, mapex-put, mapex-in,

Used from specification map-maplet

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

Used from specification map

map/Subset is used by precise-mapex,
map/exin is used by map-putex,
map/Del-rec-same is used by map-add, map-putex,
map/In-empty is used by precise-mapex,
map/In-insert is used by map-add, map-putex, precise-mapex,
map/eq-put2 is used by precise-mapex,
map/k-At-same is used by map-add, map-putex, precise-mapex,
map/notin-del-notin is used by map-add, map-putex,
map/put-same is used by map-putex,