Used simplifier rules/spec theorems by specification

Used from specification heapfuns

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

Used from specification maplet

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

Used from specification ex-maplet

• ex-maplet/map-put is used by exec-assign-wp,
• ex-maplet/map-putex is used by assign-known-weak, assign-known, assign-unknown, assign-unknown-weak,
• ex-maplet/mapex is used by assign-wp, assign-known-weak, assign-known, free-unknown-weak,
• ex-maplet/mapex-new-rw is used by alloc,
• ex-maplet/mapex-elim is used by assign-known,
• ex-maplet/mapex-in is used by assign-wp, assign-known-weak, assign-known, assign-unknown, exec-assign-wp, assign-unknown-weak,
• ex-maplet/mapex-new-rw is used by alloc-rw,
• ex-maplet/mapex-null is used by alloc-rw,
• ex-maplet/mapex-put-rw is used by assign-unknown,

Used from specification heap-sep

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

Used from specification heap

• heap/exin is used by assign-wp,
• heap/ext is used by exec-assign-wp, assigned-known-getother,
• heap/at-del is used by exec-assign-wp,
• heap/at-write is used by exec-assign-wp, assigned-known-getother,
• heap/at-write-other is used by assigned-known-getother2, get-assign,
• heap/in-alloc is used by exec-assign-wp, assigned-known-getother,
• heap/in-del is used by in-remove, free-known, free-notin, exec-assign-wp,
• heap/in-emp is used by assign-wp, exec-assign-wp, assigned-known-getother,
• heap/in-write is used by assign-new-other, assign-known, assign-unknown, exec-assign-wp, in-assign, assigned-known-getother,
• heap/nonnull is used by exec-assign-wp, assigned-known-getother,
• heap/overwrite is used by assign-wp,
• heap/sanity is used by assign-wp,