Used simplifier rules/spec theorems by specification

Used from specification heap-sep

• heap-sep/sep is used by ex-shift-o-p, compact-local, alloc-p, propagate, ex-shift-o, write-known-p,
• heap-sep/sep-ass is used by alloc-p,
• heap-sep/split-union is used by ex-shift-o-p, compact-local, alloc-p, propagate, ex-shift-o, write-known-p,
• heap-sep/emp is used by owned-emp,
• heap-sep/emp-sep is used by write-unknown, alloc, write-known,
• heap-sep/sep-ass is used by write-unknown, ex-shift-o-p, write-unknown-p, alloc-p, alloc, propagate, write-known-p, write-known,
• heap-sep/sep-com is used by write-unknown, ex-shift-o-p, write-unknown-p, alloc-p, alloc, propagate, 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 maplet

• maplet/map-putex is used by write-known-p,
• maplet/mapex is used by write-unknown-p, alloc-p, lift-mapex,
• maplet/mapex-new-rw is used by alloc-p,
• maplet/maplet is used by lift-map, lift-mapex,
• maplet/at-eq is used by write-known-p,
• maplet/ex3 is used by alloc-p, lift-mapex, ex-shift-o,
• maplet/ex3-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/mapex-elim is used by write-known-p,

Used from specification heap

• heap/at-uni is used by propagate,
• heap/disj is used by alloc-p, write-known-p,
• heap/ext is used by propagate,
• heap/in-uni is used by propagate,
• heap/subset is used by propagate,
• heap/subset-uni is used by propagate,
• heap/write-again is used by write-known-p,
• heap/write-left is used by write-known-p,
• heap/at-uni is used by propagate, write-known-p,
• heap/at-write is used by write-known-p,
• heap/disj-com-rw is used by propagate,
• heap/disj-distr-uni is used by alloc-p,
• heap/disj-distr-uni-com is used by ex-shift-o-p,
• heap/disj-l is used by propagate,
• heap/disj-r is used by compact-local, propagate, write-known-p,
• heap/in-alloc is used by lift-map, alloc-p, lift-mapex,
• heap/in-emp is used by lift-map, owned-emp, lift-mapex,
• heap/in-uni is used by ex-shift-o-p, compact-local, propagate, write-known-p,
• heap/in-write is used by lift-map, lift-mapex, write-known-p,
• heap/nonnull is used by alloc-p,
• heap/overwrite is used by write-known-p,