[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 propagate,
heapfuns/disj is used by alloc-p, write-known-p,
heapfuns/in-uni is used by propagate,
heapfuns/subset is used by propagate,
heapfuns/subset-uni is used by propagate,
heapfuns/write-left is used by write-known-p,
heapfuns/at-uni is used by propagate, write-known-p,
heapfuns/disj-com-rw is used by propagate,
heapfuns/disj-distr-uni is used by alloc-p,
heapfuns/disj-distr-uni-com is used by propagate, ex-shift-o-p,
heapfuns/disj-r is used by write-known-p,
heapfuns/in-uni is used by compact-local, propagate, ex-shift-o-p, write-known-p,

Used from specification maplet

maplet/maplet is used by lift-map, lift-mapex,
maplet/at-rw is used by write-known-p,
maplet/ex is used by alloc-p, ex-shift-o, lift-mapex,
maplet/ex1-shift is used by ex-shift-o-p,
maplet/map-in is used by write-known-p,
maplet/map-in0 is used by alloc-p,
maplet/map-put-rw is used by write-known-p,
maplet/map-write is used by write-known-p,

Used from specification ex-maplet

ex-maplet/map-putex is used by write-known-p,
ex-maplet/mapex is used by alloc-p, write-unknown-p, lift-mapex,
ex-maplet/mapex-new-rw is used by alloc-p,
ex-maplet/mapex-elim is used by write-known-p,
ex-maplet/mapex-in is used by write-known-p,

Used from specification heap-sep

heap-sep/sep is used by compact-local, alloc-p, ex-shift-o, propagate, ex-shift-o-p, write-known-p,
heap-sep/sep-ass is used by alloc-p,
heap-sep/split-union is used by compact-local, alloc-p, ex-shift-o, propagate, ex-shift-o-p, write-known-p,
heap-sep/emp is used by owned-emp,
heap-sep/emp-sep is used by alloc, write-unknown, write-known,
heap-sep/precise-split-l is used by propagate,
heap-sep/precise-split-r is used by alloc-p,
heap-sep/sep-ass is used by alloc, alloc-p, write-unknown, propagate, write-unknown-p, ex-shift-o-p, write-known-p, write-known,
heap-sep/sep-com is used by alloc, alloc-p, write-unknown, propagate, write-unknown-p, ex-shift-o-p, write-known-p, write-known,
heap-sep/split-union is used by ex-shift-o-p,
heap-sep/true-elim is used by propagate,
heap-sep/trueH is used by propagate,

Used from specification heap

heap/ext is used by propagate,
heap/at-write is used by write-known-p,
heap/in-alloc is used by alloc-p, lift-map, lift-mapex,
heap/in-emp is used by lift-map, owned-emp, lift-mapex,
heap/in-write is used by lift-map, write-known-p, lift-mapex,
heap/nonnull is used by alloc-p,
heap/overwrite is used by write-known-p,
heap/write-again is used by write-known-p,