[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 refmap-ex-maplet

refmap-ex-maplet/map-put is used by exec-assign-wp,
refmap-ex-maplet/map-putex is used by assign-known-weak, assign-unknown-weak,
refmap-ex-maplet/mapex is used by assign-wp, assign-known-weak, free-unknown,
refmap-ex-maplet/mapex-in is used by assign-wp, assign-known-weak, exec-assign-wp, assign-unknown-weak,

Used from specification map-sep

map-sep/sep is used by assign-wp, assigned-known-getother,
map-sep/sep-mp is used by exec-assign-wp,
map-sep/wand is used by assign-wp, exec-assign-wp,
map-sep/false-rev is used by free-unknown,
map-sep/false-sep is used by free-unknown, assigned-known-getother,
map-sep/falseH is used by free-unknown, assigned-known-getother,
map-sep/sep-ass is used by assign-wp, assign-known-weak, free-known, free-unknown, exec-assign-wp, assign-unknown-weak, assigned-known-getothermaplet, assigned-known-getother,
map-sep/sep-com is used by assign-wp, assign-known-weak, free-known, free-unknown, exec-assign-wp, assign-unknown-weak, assigned-known-getothermaplet, assigned-known-getother,

Used from specification heapfuns-map

heapfuns-map/at-uni is used by exec-assign-wp,
heapfuns-map/in-uni is used by exec-assign-wp,
heapfuns-map/disj-emp-r is used by assign-wp,
heapfuns-map/disj-singleton-write is used by assign-wp, exec-assign-wp, assigned-known-getother,
heapfuns-map/disj-write is used by assign-wp,
heapfuns-map/union-add-singleton-left is used by assign-wp, assigned-known-getother,
heapfuns-map/union-add-singleton-right is used by assign-wp,
heapfuns-map/union-left-singleton-at is used by exec-assign-wp,

Used from specification refmap-maplet

refmap-maplet/map-del is used by free-known, free-unknown,
refmap-maplet/maplet is used by assign-wp, exec-assign-wp, assigned-known-getother,
refmap-maplet/at-rw is used by assign-known-weak, assigned-known-getother,
refmap-maplet/ex is used by assign-wp,
refmap-maplet/ex1-shift is used by assign-known-weak, free-unknown,
refmap-maplet/map-in is used by assign-known-weak, free-unknown, assigned-known-getother,
refmap-maplet/map-null is used by free-unknown,
refmap-maplet/map-put-rw is used by assign-known-weak,
refmap-maplet/map-same is used by assigned-known-getother,
refmap-maplet/map-write is used by assign-known-weak, exec-assign-wp,
refmap-maplet/maplet is used by assign-wp,

Used from specification map

map/At-other is used by exec-assign-wp,
map/Extension is used by exec-assign-wp, assigned-known-getother,
map/exin is used by assign-wp,
map/notmemlookup is used by exec-assign-wp,
map/At-other is used by assigned-known-getother2, get-assign, assigned-known-getother,
map/Del-at is used by exec-assign-wp,
map/Del-in is used by in-remove, free-notin, exec-assign-wp,
map/In-empty is used by assign-wp, exec-assign-wp,
map/In-insert is used by assign-new-other, exec-assign-wp, in-assign, assigned-known-getother,
map/in-neq is used by in-add, exec-assign-wp,
map/inj-put is used by assign-wp,
map/k-At-same is used by exec-assign-wp,
map/put-same is used by assign-wp,