Used simplifier rules/spec theorems by specification

Used from specification obj-aux

• obj-aux/inj-timtim is used by map-putrev,
• obj-aux/elim-timtim is used by ext, mk-exists, ex3-shiftw, at-alloc-M01, at-write-M01, ex3-shift-01, ex3-03, at-alloc-M02, at-write-M02, mapex, mk-ext, map-del-01, ex3-shift,
• obj-aux/inj-timtim is used by ext, mapex-put-rw, at-rw, map-write-M02, map-put-rw, at-alloc-M01, at-write-M01, eq-objs-M01, eq-objs-M02, at-alloc-M02, at-write-M02, map-write-M01, map-putex, at-rw0, map-del-01, map-del,
• obj-aux/sel-timtim-dotaux is used by ex3-shiftw, at-unir-M02, ex3-shiftw-inst, ex3-shift-01, at-eq, ex3-03, at-write-M02, at-unil-M02, at-rw-M02, ex3-shift, at-mk-M02,
• obj-aux/sel-timtim-dotobj is used by ex3-shiftw, at-write-M01, ex3-shiftw-inst, ex3-shift-01, at-rw-M01, at-unil-M01, at-eq, ex3-03, at-mk-M01, ex3-shift, at-unir-M01,

Used from specification heap-sep

• heap-sep/heap-aux-inst/and is used by prop-sep,
• heap-sep/heap-aux-inst/and-ass is used by prop-emp, mapex-and, prop-sep,
• heap-sep/heap-aux-inst/and-com is used by prop-emp, mapex-and, prop-sep,
• heap-sep/heap-aux-inst/emp-sep is used by prop-emp,
• heap-sep/heap-aux-inst/false-rev is used by prop, map-null, mapex-null,
• heap-sep/heap-aux-inst/prop is used by prop-sep,
• heap-sep/heap-aux-inst/prop-shift is used by prop-emp, prop-sep,
• heap-sep/heap-aux-inst/sep-ass is used by ex2-shift-01, true-elim, mapex-put-rw, map-write-M02, mapex-elim-01, map-put-rw, prop-emp, split-uni, mapex-new-rw, ex3-shift-01, eq-objs-M01, ex1-shift, map-same, at-rw-M01, mapex-elim, at-eq, mapex-put-01, eq-objs-M02, mapex-in-01, sep, map-put-01, mapex-new-01, map-put, ex2-shift, map-write-M01, map-putex, at-rw-M02, map-del-01, map-in, map-in-01, ex1-shift-01, true-emp, mapex-put, ex3-shift, map-del, mapex-in, prop-sep,
• heap-sep/heap-aux-inst/sep-com is used by ex2-shift-01, true-elim, mapex-put-rw, map-write-M02, mapex-elim-01, map-put-rw, prop-emp, split-uni, mapex-new-rw, ex3-shift-01, eq-objs-M01, ex1-shift, map-same, at-rw-M01, mapex-elim, at-eq, mapex-put-01, eq-objs-M02, mapex-in-01, sep, map-put-01, mapex-new-01, map-put, ex2-shift, map-write-M01, map-putex, at-rw-M02, map-del-01, map-in, map-in-01, ex1-shift-01, true-emp, mapex-put, ex3-shift, map-del, mapex-in, prop-sep,
• heap-sep/heap-aux-inst/true-and is used by prop-emp, prop-sep,
• heap-sep/heap-aux-inst/true-rev is used by prop-emp, prop, prop-sep,

Used from specification set-union

• set-union/refset/del-in is used by map-del,
• set-union/refset/int-a is used by at-unir-M02, split-uni, at-unil-M01, sep, at-unil-M02, at-unir-M01,
• set-union/refset/int-c is used by at-unir-M02, split-uni, at-unil-M01, sep, at-unil-M02, at-unir-M01,
• set-union/refset/una is used by split-uni, sep,
• set-union/refset/unc is used by split-uni, sep,

Used from specification maplet

• maplet/heap-aux-inst/ex1-shiftw-inst is used by ex1-shiftw-inst,
• maplet/heap-aux-inst/ex2-shiftw-inst is used by ex2-shiftw-inst,
• maplet/heap-aux-inst/ex3-shiftw-inst is used by ex3-shiftw-inst,
• maplet/heap-aux-inst/map-del is used by map-del-01,
• maplet/heap-aux-inst/map-put is used by map-put-01,
• maplet/heap-aux-inst/map-putex is used by map-putex,
• maplet/heap-aux-inst/mapex is used by mapex,
• maplet/heap-aux-inst/mapex-del is used by mapex-del-01,
• maplet/heap-aux-inst/mapex-new-rw is used by mapex-new-rw, mapex-new-01,
• maplet/heap-aux-inst/mapex-put is used by mapex-put-01,
• maplet/heap-aux-inst/maplet is used by maplet,
• maplet/heap-aux-inst/at-rw is used by at-rw-M01, at-eq, at-rw-M02, map-del-01,
• maplet/heap-aux-inst/eq-objs is used by eq-objs-M01, eq-objs-M02,
• maplet/heap-aux-inst/ex1 is used by ex1,
• maplet/heap-aux-inst/ex1-shift is used by ex1-shift-01,
• maplet/heap-aux-inst/ex1-shiftw is used by ex1-shiftw,
• maplet/heap-aux-inst/ex2 is used by ex2,
• maplet/heap-aux-inst/ex2-shift is used by ex2-shift-01,
• maplet/heap-aux-inst/ex2-shiftw is used by ex2-shiftw,
• maplet/heap-aux-inst/ex3 is used by ex3-03,
• maplet/heap-aux-inst/ex3-shift is used by ex3-shift,
• maplet/heap-aux-inst/ex3-shiftw is used by ex3-shiftw,
• maplet/heap-aux-inst/map-in is used by map-put-rw, map-del-01, map-in-01,
• maplet/heap-aux-inst/map-in0 is used by map-in0-02,
• maplet/heap-aux-inst/map-null is used by map-null,
• maplet/heap-aux-inst/map-put-rw is used by map-put-rw,
• maplet/heap-aux-inst/map-same is used by map-same,
• maplet/heap-aux-inst/map-write is used by mapex-put-rw, map-write-M02, map-put-rw, map-put-01, map-write-M01, map-putex,
• maplet/heap-aux-inst/mapex-and is used by mapex-and,
• maplet/heap-aux-inst/mapex-elim is used by mapex-elim-01, mapex-put-01,
• maplet/heap-aux-inst/mapex-in is used by mapex-put-rw, mapex-in-01, map-put-01, map-putex,
• maplet/heap-aux-inst/mapex-put-rw is used by mapex-put-rw, map-put-01, map-putex,
• maplet/heap-aux-inst/precise-map is used by precise-map,

Used from specification set-basic

• set-basic/refset/ne-01 is used by map-putrev, write, map-del,
• set-basic/refset/size-zero-01 is used by map-putrev, write, map-del,

Used from specification heap-fun

• heap-fun/heap-aux-inst/apply is used by apply, prop-sep,
• heap-fun/heap-aux-inst/at-rw0 is used by at-rw0,
• heap-fun/heap-aux-inst/del is used by del,
• heap-fun/heap-aux-inst/map-del is used by at-rw, map-del,
• heap-fun/heap-aux-inst/map-put is used by map-put,
• heap-fun/heap-aux-inst/map-putrev is used by map-putrev,
• heap-fun/heap-aux-inst/mapex-del is used by mapex-del,
• heap-fun/heap-aux-inst/mapex-new is used by mapex-new,
• heap-fun/heap-aux-inst/mapex-put is used by mapex-put,
• heap-fun/heap-aux-inst/mk-exists is used by mk-exists,
• heap-fun/heap-aux-inst/mk-ext is used by mk-ext,
• heap-fun/heap-aux-inst/prop-emp is used by prop-emp,
• heap-fun/heap-aux-inst/sep is used by sep,
• heap-fun/heap-aux-inst/uni is used by uni,
• heap-fun/heap-aux-inst/write is used by write,
• heap-fun/heap-aux-inst/at-mk is used by at-mk-M01, at-mk-M02,
• heap-fun/heap-aux-inst/at-unil is used by at-unil-M01, at-unil-M02,
• heap-fun/heap-aux-inst/at-unir is used by at-unir-M02, at-unir-M01,
• heap-fun/heap-aux-inst/disj is used by in-uni, disj,
• heap-fun/heap-aux-inst/emp is used by emp,
• heap-fun/heap-aux-inst/ex1-shift is used by ex1-shift,
• heap-fun/heap-aux-inst/ex2-shift is used by ex2-shift,
• heap-fun/heap-aux-inst/ex3-shift is used by ex3-shift-01,
• heap-fun/heap-aux-inst/in-mk is used by in-mk, in-uni,
• heap-fun/heap-aux-inst/map-in is used by map-put, map-in, map-del,
• heap-fun/heap-aux-inst/map-in0 is used by map-in0,
• heap-fun/heap-aux-inst/mapex-elim is used by mapex-elim, mapex-put,
• heap-fun/heap-aux-inst/mapex-in is used by mapex-put, mapex-in,
• heap-fun/heap-aux-inst/mapex-in0 is used by mapex-in0,
• heap-fun/heap-aux-inst/prop-false is used by prop, prop-false,
• heap-fun/heap-aux-inst/prop-true is used by prop-true, prop,
• heap-fun/heap-aux-inst/split-uni is used by split-uni, sep,
• heap-fun/heap-aux-inst/true-elim is used by true-elim,
• heap-fun/heap-aux-inst/true-emp is used by true-emp,

Used from specification heap-aux

• heap-aux/mapex-null is used by mapex-null,
• heap-aux/mapornull-emp is used by mapornull, mapornull-emp,
• heap-aux/mapornull-ex is used by mapornull, mapornull-ex,
• heap-aux/precise-mapex is used by precise-mapex,
• heap-aux/precise-mapornull is used by precise-mapornull,

Used from specification heap

• heap/heap-aux-inst/at-alloc is used by at-alloc-M01, at-alloc-M02,
• heap/heap-aux-inst/ext is used by ext,
• heap/heap-aux-inst/in-uni is used by in-uni,
• heap/heap-aux-inst/at-del is used by at-del-M01, at-del-M02,
• heap/heap-aux-inst/at-write is used by at-write-M01, at-write-M02,
• heap/heap-aux-inst/del-notin is used by map-del-01,
• heap/heap-aux-inst/diff-write is used by diff-write,
• heap/heap-aux-inst/in-write is used by in-write,
• heap/heap-aux-inst/size-write is used by size-write,
• heap/heap-aux-inst/write-del is used by write-del,
• heap/heap-aux-inst/write-left is used by write-left,
• heap/heap-aux-inst/write-right is used by write-right,