[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 store+set

store+set/index-store-address-store/restrict-at is used by restrict-add-subseteq-at, restrict-2, btree-restrict-union-proper, btree-inv-alloc,
store+set/index-store-address-store/Dom is used by restrict-dom, btree-write-node, btree-restrict-union-proper, btree-reset-root-frame, btree-repl-dirty-address, btree-null, btree-mark-dirty, btree-istore-reduce-refed, btree-inv-format, btree-inv-crash, btree-inv-alloc, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-clean-adr-in, btree-adrs,
store+set/index-store-address-store/dom-emp is used by btree-as-empty,
store+set/index-store-address-store/dom-ins is used by btree-write-other,
store+set/index-store-address-store/in-dom-inter is used by restrict-dom,
store+set/index-store-address-store/restrict-at is used by subseteq-restrict, restrict-further, restrict-add-at, restrict-2, btree-restrict-union-proper,
store+set/index-store-address-store/restrict-empty is used by btree-as-empty-rev, btree-as-empty,
store+set/index-store-address-store/restrict-in is used by subseteq-restrict, restrict-further, restrict-dom, restrict-add-subseteq-in, restrict-add-subseteq-at, restrict-add-in, restrict-add-at, restrict-2, btree-restrict-union-proper, btree-inv-alloc,

Used from specification znode-ops

znode-ops/save-node is used by btree-inv-format,
znode-ops/scan-strong is used by ri-range-ext,
znode-ops/save-branches-base is used by btree-inv-format,
znode-ops/scan-base is used by ri-range-ext,
znode-ops/scan-last is used by ri-range-ext,
znode-ops/scan-min-eq is used by ri-range-ext,
znode-ops/scan-rec is used by ri-range-ext,

Used from specification nat-basic

nat-basic/a is used by sep-forall-reduce-true, sep-forall-reduce, ri-range-ext, nat-le-eq, btree-write-other, btree-write-node, btree-sub-clean-write-branches, btree-sub-clean-next, btree-ri-unique, btree-repl-dirty-address, btree-refed-subseteq-alladrs, btree-mark-dirty, btree-leaf-adr, btree-istore-reduce-refed, btree-inv-format, btree-dirty-adr-notin, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-clean-adr-in, btree-adrs,
nat-basic/add-base is used by nat-le-eq, btree-write-other, btree-write-node, btree-ri-unique, btree-repl-dirty-address, btree-refed-subseteq-alladrs, btree-mark-dirty, btree-leaf-adr, btree-istore-reduce-refed, btree-inv-format, btree-dirty-adr-notin, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-clean-adr-in, btree-adrs,
nat-basic/c is used by sep-forall-reduce-true, sep-forall-reduce, ri-range-ext, nat-le-eq, btree-write-other, btree-write-node, btree-sub-clean-write-branches, btree-sub-clean-next, btree-ri-unique, btree-repl-dirty-address, btree-refed-subseteq-alladrs, btree-mark-dirty, btree-leaf-adr, btree-istore-reduce-refed, btree-inv-format, btree-dirty-adr-notin, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-clean-adr-in, btree-adrs,
nat-basic/eq-01 is used by btree-ri-unique, btree-clean-fwd-strong, btree-clean-fwd,
nat-basic/eqs is used by ri-range-ext,
nat-basic/f is used by sep-forall-reduce-true, sep-forall-reduce, ri-range-ext, btree-write-other, btree-write-node, btree-sub-clean-write-branches, btree-sub-clean-next, btree-sub-clean-leaf, btree-ri-unique, btree-restrict-union-proper, btree-reset-root-frame, btree-refed-subseteq-alladrs, btree-mark-dirty, btree-istore-reduce-refed, btree-inv-crash, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,
nat-basic/l is used by ri-range-ext,
nat-basic/l-01 is used by btree-ri-unique, btree-clean-fwd-strong, btree-clean-fwd,
nat-basic/l-02 is used by btree-ri-unique, btree-clean-fwd-strong, btree-clean-fwd,
nat-basic/lf is used by ri-range-ext, btree-sub-clean-write-branches, btree-ri-unique,
nat-basic/lf-01 is used by btree-write-other, btree-write-node, btree-sub-clean-write-branches, btree-ri-unique, btree-refed-subseteq-alladrs, btree-mark-dirty, btree-istore-reduce-refed, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,
nat-basic/lf-02 is used by ri-range-ext, btree-sub-clean-next, btree-ri-unique,
nat-basic/ls-02 is used by sep-forall-reduce-true, sep-forall-reduce,
nat-basic/oz is used by ri-range-ext, btree-write-other, btree-write-node, btree-ri-unique, btree-refed-subseteq-alladrs, btree-mark-dirty, btree-istore-reduce-refed, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,
nat-basic/s-04 is used by sep-forall-reduce-true, sep-forall-reduce, ri-range-ext, btree-write-other, btree-write-node, btree-sub-clean-write-branches, btree-sub-clean-next, btree-ri-unique, btree-refed-subseteq-alladrs, btree-mark-dirty, btree-istore-reduce-refed, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,
nat-basic/succ is used by sep-forall-reduce-true, sep-forall-reduce, ri-range-ext, btree-write-other, btree-write-node, btree-sub-clean-write-branches, btree-ri-unique, btree-refed-subseteq-alladrs, btree-mark-dirty, btree-istore-reduce-refed, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,
nat-basic/z-01 is used by ri-range-ext,
nat-basic/zero is used by ri-range-ext, btree-inv-format, btree-clean-fwd-strong, btree-clean-fwd,
nat-basic/zero-01 is used by sep-forall-reduce, ri-range-ext, btree-sub-clean-0,

Used from specification ablock

ablock/index-store/sel-03 is used by btree-inv-alloc,

Used from specification zbranch

zbranch/elim-01 is used by btree-write-other, btree-write-node, btree-sub-clean-write-branches, btree-sub-clean-next, btree-ri-unique, btree-refed-subseteq-alladrs, btree-istore-reduce-refed, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,
zbranch/inj is used by btree-write-other, btree-sub-clean-write-branches, btree-refed-subseteq-alladrs, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,
zbranch/sel-01 is used by btree-write-node, btree-sub-clean-write-branches, btree-sub-clean-next, btree-ri-unique, btree-clean-fwd,
zbranch/sel-03 is used by btree-ri-unique, btree-clean-fwd,
zbranch/test-03 is used by btree-write-other, btree-write-node, btree-sub-clean-write-branches, btree-sub-clean-next, btree-ri-unique, btree-refed-subseteq-alladrs, btree-istore-reduce-refed, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,

Used from specification ablock-nodes

ablock-nodes/index-store/at-nodes is used by btree-inv-format,
ablock-nodes/index-store/prefix-imp-dom-nodes-subset is used by btree-inv-crash,
ablock-nodes/index-store/prefix-imp-nodes-subset is used by btree-inv-crash,
ablock-nodes/index-store/at-nodes is used by btree-inv-alloc,
ablock-nodes/index-store/in-nodes is used by btree-inv-format, btree-inv-crash, btree-inv-alloc,
ablock-nodes/index-store/nodes-at-alloc is used by btree-inv-alloc,
ablock-nodes/index-store/prefix-imp-nodes-subset is used by btree-inv-root-null-or-clean, btree-inv-root-null, btree-inv-remove-refsize0, btree-inv-clean-commit,

Used from specification znode

znode/elim is used by btree-write-node, btree-sub-clean-write-branches, btree-sub-clean-next, btree-repl-dirty-address, btree-null-or-clean-below, btree-inv-root-null-or-clean, btree-inv-clean-commit,
znode/inj is used by btree-write-node, btree-sub-clean-write-branches, btree-sub-clean-next, btree-ri-unique, btree-repl-dirty-address, btree-null-or-clean-below, btree-mark-dirty, btree-leaf-fwd, btree-dirty-adr-notin, btree-clean-adr-in,
znode/sel-02 is used by btree-write-node, btree-sub-clean-write-branches, btree-sub-clean-next, btree-sub-clean-leaf, btree-inv-format,
znode/sel-03 is used by btree-write-node, btree-sub-clean-write-branches, btree-sub-clean-next, btree-sub-clean-leaf, btree-inv-format,
znode/sel-04 is used by btree-write-node, btree-sub-clean-next, btree-istore-reduce-refed, btree-inv-root-null-or-clean, btree-inv-remove-refsize0, btree-inv-format, btree-inv-clean-commit, btree-adrs,
znode/sel-05 is used by btree-write-node, btree-sub-clean-write-branches, btree-sub-clean-next, btree-sub-clean-leaf, btree-inv-format,
znode/upd-02 is used by btree-sub-clean-write-branches,

Used from specification heap-sep

heap-sep/zheap/sep is used by btree-clean-fwd-strong, btree-clean-fwd, btree-adrs,
heap-sep/zheap/and is used by btree-write-node, btree-ri-unique, btree-repl-dirty-address, btree-refed-subseteq-alladrs, btree-mark-dirty, btree-leaf-adr, btree-istore-reduce-refed, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,
heap-sep/zheap/and-ass is used by btree-write-other, btree-write-node, btree-ri-unique, btree-repl-dirty-address, btree-refed-subseteq-alladrs, btree-mark-dirty, btree-leaf-adr, btree-istore-reduce-refed, btree-inv-format, btree-dirty-adr-notin, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-clean-adr-in, btree-adrs,
heap-sep/zheap/and-com is used by btree-write-other, btree-write-node, btree-ri-unique, btree-repl-dirty-address, btree-refed-subseteq-alladrs, btree-mark-dirty, btree-leaf-adr, btree-istore-reduce-refed, btree-inv-format, btree-dirty-adr-notin, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-clean-adr-in, btree-adrs,
heap-sep/zheap/emp-sep is used by sep-forall-reduce-true, sep-forall-reduce, btree-write-other, btree-write-node, btree-ri-unique, btree-repl-dirty-address, btree-refed-subseteq-alladrs, btree-mark-dirty, btree-leaf-adr, btree-istore-reduce-refed, btree-inv-format, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,
heap-sep/zheap/false-and is used by btree-dirty-adr-notin, btree-clean-adr-in,
heap-sep/zheap/false-rev is used by maplet-null, btree-dirty-adr-notin, btree-clean-adr-in,
heap-sep/zheap/false-sep is used by maplet-null, btree-dirty-adr-notin, btree-clean-adr-in,
heap-sep/zheap/falseH is used by maplet-null, btree-dirty-adr-notin, btree-clean-adr-in,
heap-sep/zheap/prop is used by btree-write-other, btree-write-node, btree-ri-unique, btree-repl-dirty-address, btree-refed-subseteq-alladrs, btree-mark-dirty, btree-leaf-adr, btree-istore-reduce-refed, btree-inv-format, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,
heap-sep/zheap/prop-shift is used by btree-write-other, btree-write-node, btree-ri-unique, btree-repl-dirty-address, btree-refed-subseteq-alladrs, btree-mark-dirty, btree-leaf-adr, btree-istore-reduce-refed, btree-inv-format, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,
heap-sep/zheap/sep-ass is used by sep-forall-reduce-true, sep-forall-reduce, maplet-null, btree-write-other, btree-write-node, btree-truify-context, btree-root-in-heap, btree-ri-unique, btree-restrict-union-proper, btree-reset-root-frame, btree-reset-root, btree-repl-dirty-address, btree-remove-context, btree-refed-subseteq-alladrs, btree-null-or-clean-below, btree-null, btree-mark-dirty, btree-leaf-fwd, btree-leaf-adr, btree-istore-restrict-to-as, btree-istore-restrict, btree-istore-reduce-refed, btree-istore-reduce, btree-inv-root-null-or-clean, btree-inv-root-null, btree-inv-root-neq-null-fwd, btree-inv-remove-refsize0, btree-inv-format, btree-inv-crash, btree-inv-clean-commit, btree-inv-alloc, btree-imp-dirty, btree-dirty-adr-notin, btree-crash, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-clean-adr-in, btree-as-empty-rev, btree-as-empty, btree-adrs,
heap-sep/zheap/sep-com is used by sep-forall-reduce-true, sep-forall-reduce, maplet-null, btree-write-other, btree-write-node, btree-truify-context, btree-root-in-heap, btree-ri-unique, btree-restrict-union-proper, btree-reset-root-frame, btree-reset-root, btree-repl-dirty-address, btree-remove-context, btree-refed-subseteq-alladrs, btree-null-or-clean-below, btree-null, btree-mark-dirty, btree-leaf-fwd, btree-leaf-adr, btree-istore-restrict-to-as, btree-istore-restrict, btree-istore-reduce-refed, btree-istore-reduce, btree-inv-root-null-or-clean, btree-inv-root-null, btree-inv-root-neq-null-fwd, btree-inv-remove-refsize0, btree-inv-format, btree-inv-crash, btree-inv-clean-commit, btree-inv-alloc, btree-imp-dirty, btree-dirty-adr-notin, btree-crash, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-clean-adr-in, btree-as-empty-rev, btree-as-empty, btree-adrs,
heap-sep/zheap/true-and is used by btree-write-other, btree-write-node, btree-ri-unique, btree-repl-dirty-address, btree-mark-dirty, btree-istore-reduce-refed, btree-inv-format, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs,
heap-sep/zheap/true-elim is used by sep-forall-reduce-true, btree-truify-context, btree-reset-root-frame, btree-reset-root, btree-null, btree-inv-root-null-or-clean, btree-inv-remove-refsize0, btree-inv-clean-commit, btree-inv-alloc,
heap-sep/zheap/true-emp is used by sep-forall-reduce-true, btree-reset-root-frame,
heap-sep/zheap/true-rev is used by btree-write-other, btree-write-node, btree-ri-unique, btree-repl-dirty-address, btree-mark-dirty, btree-istore-reduce-refed, btree-inv-format, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs,
heap-sep/zheap/true-true is used by sep-forall-reduce-true, btree-reset-root,
heap-sep/zheap/trueH is used by btree-repl-dirty-address, btree-null, btree-inv-format, btree-inv-crash,

Used from specification ablock-store-inv

ablock-store-inv/index-store/at is used by btree-inv-format,
ablock-store-inv/index-store/in is used by btree-inv-crash,
ablock-store-inv/index-store/in-alloc is used by btree-inv-alloc,
ablock-store-inv/index-store/in-write-explicit is used by btree-inv-format,
ablock-store-inv/index-store/notin-notin is used by btree-inv-crash, btree-inv-adr-lnum-in,
ablock-store-inv/index-store/prefix-at is used by btree-inv-crash,
ablock-store-inv/index-store/prefix-fwd-in is used by btree-inv-crash,
ablock-store-inv/index-store/prefix-in is used by btree-inv-crash,

Used from specification apersistence-base

apersistence-base/crash-index-at is used by btree-inv-crash,
apersistence-base/crash-index-in is used by btree-inv-crash,
apersistence-base/icrash-refsize-cons is used by btree-inv-crash,
apersistence-base/icrash-remove-refsize0-prefix is used by btree-inv-crash,
apersistence-base/inv-crash is used by btree-inv-crash,

Used from specification node-index-restrict

node-index-restrict/in-gt is used by ri-range-ext,
node-index-restrict/in-le is used by ri-range-ext,

Used from specification store

store/index-store-ablock-store-nat-store/At-other is used by btree-inv-format,
store/node-index/Extension is used by ri-range-ext,
store/index-store-address-store/Extension is used by restrict-idem, restrict-2,
store/index-store-address-store/Subset is used by subseteq-restrict, restrict-further, restrict-add-subseteq-in, restrict-add-subseteq-at, restrict-add-in, restrict-add-at, btree-restrict-union-proper, btree-inv-alloc,
store/node-index/k-Extension is used by ri-range-ext,
store/index-store-ablock-store-nat-store/At-same is used by btree-inv-format,
store/index-store-ablock-store-nat-store/In-empty is used by btree-inv-format,
store/index-store-ablock-store-nat-store/in-neq is used by btree-inv-format,
store/node-index/notmemlookup is used by ri-range-ext,
store/index-store-address-store/notmemlookup is used by restrict-2,
store/index-store-address-store/sub-ref is used by btree-write-node, btree-istore-restrict-to-as,
store/index-store-address-store/subset-elem-eq-02 is used by subseteq-restrict,
store/index-store-address-store/subset-empty is used by btree-as-empty-rev,
store/index-store-address-store/subset-new is used by btree-write-node,
store/index-store-address-store/superset-elem-in-01 is used by subseteq-restrict,

Used from specification nat

nat/add-01 is used by btree-ri-unique, btree-refed-subseteq-alladrs, btree-mark-dirty, btree-istore-reduce-refed, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,
nat/anti is used by ri-range-ext, btree-sub-clean-next, btree-clean-fwd-strong, btree-clean-fwd,
nat/elim-pred-c is used by ri-range-ext, btree-write-other, btree-write-node, btree-ri-unique, btree-refed-subseteq-alladrs, btree-mark-dirty, btree-istore-reduce-refed, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,
nat/elim-sub is used by btree-ri-unique, btree-refed-subseteq-alladrs, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,
nat/eq is used by ri-range-ext,
nat/eq-01 is used by sep-forall-reduce-true, sep-forall-reduce,
nat/eqle-one is used by btree-write-other, btree-write-node, btree-ri-unique, btree-refed-subseteq-alladrs, btree-mark-dirty, btree-istore-reduce-refed, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,
nat/fle is used by btree-ri-unique, btree-clean-fwd-strong, btree-clean-fwd,
nat/fle-01 is used by ri-range-ext, btree-write-other, btree-write-node, btree-sub-clean-write-branches, btree-ri-unique, btree-refed-subseteq-alladrs, btree-istore-reduce-refed, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,
nat/le-add is used by nat-le-eq,
nat/le-def is used by btree-refed-subseteq-alladrs, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,
nat/le-ls-simp is used by ri-range-ext, btree-write-other, btree-write-node, btree-ri-unique, btree-refed-subseteq-alladrs, btree-istore-reduce-refed, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,
nat/lels is used by ri-range-ext, btree-write-node, btree-sub-clean-write-branches, btree-sub-clean-next, btree-ri-unique, btree-refed-subseteq-alladrs, btree-istore-reduce-refed, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,
nat/lels-02 is used by btree-sub-clean-write-branches,
nat/lels-03 is used by ri-range-ext, btree-ri-unique, btree-clean-fwd-strong, btree-clean-fwd,
nat/lep is used by ri-range-ext, btree-ri-unique, btree-refed-subseteq-alladrs, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,
nat/lep-02 is used by btree-ri-unique, btree-mark-dirty, btree-istore-reduce-refed, btree-clean-fwd-strong, btree-clean-fwd,
nat/ler is used by ri-range-ext, nat-le-eq, btree-write-other, btree-write-node, btree-sub-clean-write-branches, btree-sub-clean-next, btree-ri-unique, btree-repl-dirty-address, btree-refed-subseteq-alladrs, btree-mark-dirty, btree-leaf-adr, btree-istore-reduce-refed, btree-inv-format, btree-dirty-adr-notin, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-clean-adr-in, btree-adrs,
nat/let is used by btree-clean-fwd-strong, btree-clean-fwd,
nat/lez is used by ri-range-ext, btree-write-node, btree-refed-subseteq-alladrs, btree-istore-reduce-refed, btree-inv-format, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,
nat/lez-01 is used by ri-range-ext,
nat/succ-01 is used by ri-range-ext, btree-write-other, btree-write-node, btree-ri-unique, btree-refed-subseteq-alladrs, btree-mark-dirty, btree-istore-reduce-refed, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,

Used from specification set-union

set-union/node-store/Difference is used by inter-union-diff-subseteq, diff-eq-diff-eq-union,
set-union/node-store/Intersect is used by inter-union-diff,
set-union/node-store/del-in is used by btree-repl-dirty-address,
set-union/node-store/delete-shift is used by btree-write-other, btree-write-node, btree-refed-subseteq-alladrs, btree-istore-reduce-refed, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,
set-union/node-store/diff-del-plus-1 is used by add-rem-same,
set-union/node-store/subdef is used by union-diff-subseteq-union, subseteq-inter-same, inter-union-diff-subseteq, inter-subseteq-simp, diff-subseteq-subseteq, diff-empty-subseteq, btree-inv-alloc,
set-union/node-store/unrax is used by union-diff-same, inter-union-diff-subseteq, diff-eq-diff-eq-union,
set-union/node-store/Delete is used by btree-write-node, btree-repl-dirty-address, btree-mark-dirty,
set-union/node-store/Difference is used by union-diff-subseteq-union, union-diff-same, inter-empty-inter-diff-empty, diff-subseteq-subseteq, diff-eq-diff-eq-union, diff-empty-subseteq, diff-add-same,
set-union/node-store/Intersect is used by subseteq-inter-same, restrict-dom, restrict-2, inter-union-diff-subseteq, inter-union-diff, inter-subseteq-simp, inter-empty-inter-diff-empty,
set-union/node-store/One is used by btree-write-node, btree-ri-unique, btree-mark-dirty, btree-leaf-adr, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs,
set-union/node-store/del-addeq-04 is used by btree-clean-fwd-strong, btree-clean-fwd,
set-union/node-store/del-addeq-05 is used by btree-write-node, btree-ri-unique, btree-repl-dirty-address, btree-mark-dirty, btree-istore-reduce-refed, btree-inv-format, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs,
set-union/node-store/del-addin-01 is used by btree-write-node, btree-repl-dirty-address,
set-union/node-store/del-d is used by btree-mark-dirty,
set-union/node-store/del-e-01 is used by btree-write-node, btree-ri-unique, btree-repl-dirty-address, btree-mark-dirty, btree-istore-reduce-refed, btree-inv-format, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs,
set-union/node-store/del-e-02 is used by btree-write-other, btree-ri-unique, btree-repl-dirty-address, btree-refed-subseteq-alladrs, btree-leaf-adr, btree-istore-reduce-refed, btree-dirty-adr-notin, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-adr-in, btree-adrs,
set-union/node-store/del-in is used by btree-write-other, btree-write-node, btree-ri-unique, btree-repl-dirty-address, btree-refed-subseteq-alladrs, btree-istore-reduce-refed, btree-dirty-adr-notin, btree-adrs,
set-union/node-store/del-in-03 is used by btree-write-node,
set-union/node-store/diff-del-plus-1 is used by diff-add-same,
set-union/node-store/diff-del-plus-2 is used by diff-add-same, add-rem-same,
set-union/node-store/diff-idem is used by add-rem-same,
set-union/node-store/diff-union is used by inter-union-diff,
set-union/node-store/int-a is used by subseteq-inter-same, restrict-idem, restrict-dom, restrict-2, inter-union-diff-subseteq, inter-union-diff, inter-subseteq-weaken, inter-subseteq-simp, inter-empty-inter-diff-empty,
set-union/node-store/int-c is used by subseteq-inter-same, restrict-idem, restrict-dom, restrict-2, inter-union-diff-subseteq, inter-union-diff, inter-subseteq-weaken, inter-subseteq-simp, inter-empty-inter-diff-empty,
set-union/node-store/int-empty-02 is used by inter-empty-inter-diff-empty,
set-union/node-store/int-idem is used by restrict-idem,
set-union/node-store/int-subs01 is used by inter-subseteq-weaken, inter-subseteq-simp,
set-union/node-store/one-min is used by btree-repl-dirty-address, btree-mark-dirty,
set-union/node-store/subset-union-left-rem is used by subseteq-union-simp,
set-union/node-store/una is used by union-diff-subseteq-union, union-diff-same, subseteq-union-simp, inter-union-diff-subseteq, inter-union-diff,
set-union/node-store/unc is used by union-diff-subseteq-union, union-diff-same, subseteq-union-simp, inter-union-diff-subseteq, inter-union-diff,
set-union/node-store/unin is used by union-diff-same,
set-union/node-store/unin-01 is used by union-diff-subseteq-union, union-diff-same, inter-union-diff-subseteq,

Used from specification maplet

maplet/zheap/at-eq is used by btree-write-node, btree-repl-dirty-address, btree-null-or-clean-below, btree-mark-dirty, btree-leaf-fwd, btree-dirty-adr-notin, btree-clean-adr-in,
maplet/zheap/eq-objs is used by btree-ri-unique,
maplet/zheap/map-in is used by btree-write-node, btree-root-in-heap, btree-ri-unique, btree-repl-dirty-address, btree-mark-dirty, btree-dirty-adr-notin, btree-clean-adr-in,
maplet/zheap/map-null is used by maplet-null,
maplet/zheap/map-put-rw is used by btree-write-node, btree-mark-dirty,
maplet/zheap/map-putex is used by btree-write-node, btree-mark-dirty,

Used from specification set-basic

set-basic/node-store/Extension is used by union-diff-same, restrict-dom, inter-union-diff, inter-empty-inter-diff-empty, diff-eq-diff-eq-union, diff-empty-subseteq, btree-clean-alladrs,
set-basic/node-store/sub-add is used by btree-adrs,
set-basic/node-store/sub-insert-01 is used by btree-refed-subseteq-alladrs,
set-basic/node-store/In-empty is used by inter-empty-inter-diff-empty, diff-empty-subseteq, btree-write-node, btree-mark-dirty, btree-inv-format, btree-clean-alladrs, btree-adrs,
set-basic/node-store/In-insert is used by restrict-add-subseteq-in, restrict-add-subseteq-at, btree-write-node,
set-basic/node-store/Size-insert is used by btree-write-node, btree-refed-subseteq-alladrs, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs,
set-basic/node-store/add is used by btree-write-node,
set-basic/node-store/eq-01 is used by btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs,
set-basic/node-store/eq-02 is used by btree-write-node,
set-basic/node-store/eq-03 is used by diff-add-same,
set-basic/node-store/in-03 is used by btree-write-other, btree-write-node, btree-refed-subseteq-alladrs, btree-istore-reduce-refed, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,
set-basic/node-store/in-04 is used by btree-write-other, btree-write-node, btree-ri-unique, btree-refed-subseteq-alladrs, btree-mark-dirty, btree-istore-reduce-refed, btree-inv-format, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,
set-basic/node-store/in-06 is used by btree-write-other, btree-ri-unique, btree-refed-subseteq-alladrs, btree-istore-reduce-refed, btree-adrs,
set-basic/node-store/ne is used by btree-write-other, btree-write-node, btree-ri-unique, btree-refed-subseteq-alladrs, btree-mark-dirty, btree-istore-reduce-refed, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,
set-basic/node-store/ne-01 is used by restrict-further, restrict-dom, restrict-add-in, restrict-add-at, restrict-2, inter-union-diff-subseteq, inter-subseteq-simp, diff-subseteq-subseteq, diff-eq-diff-eq-union, diff-empty-subseteq, btree-write-other, btree-write-node, btree-root-in-heap, btree-ri-unique, btree-restrict-union-proper, btree-reset-root-frame, btree-repl-dirty-address, btree-refed-subseteq-alladrs, btree-null-or-clean-below, btree-null, btree-mark-dirty, btree-leaf-fwd, btree-leaf-adr, btree-istore-reduce-refed, btree-inv-crash, btree-inv-alloc, btree-imp-dirty, btree-dirty-adr-notin, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-clean-adr-in, btree-adrs,
set-basic/node-store/one-size is used by btree-write-other, btree-ri-unique, btree-refed-subseteq-alladrs, btree-mark-dirty, btree-istore-reduce-refed, btree-clean-fwd-strong, btree-clean-fwd, btree-adrs,
set-basic/node-store/size-one-01 is used by btree-write-other, btree-ri-unique, btree-refed-subseteq-alladrs, btree-mark-dirty, btree-istore-reduce-refed, btree-clean-fwd-strong, btree-clean-fwd, btree-adrs,
set-basic/node-store/size-zero is used by inter-empty-inter-diff-empty, btree-clean-alladrs,
set-basic/node-store/size-zero-01 is used by restrict-further, restrict-add-in, restrict-add-at, restrict-2, inter-union-diff-subseteq, inter-subseteq-simp, inter-empty-inter-diff-empty, diff-subseteq-subseteq, diff-empty-subseteq, btree-write-other, btree-write-node, btree-ri-unique, btree-restrict-union-proper, btree-reset-root-frame, btree-repl-dirty-address, btree-refed-subseteq-alladrs, btree-null-or-clean-below, btree-null, btree-mark-dirty, btree-istore-reduce-refed, btree-inv-crash, btree-inv-alloc, btree-imp-dirty, btree-dirty-adr-notin, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-clean-adr-in, btree-adrs,
set-basic/node-store/sub-add is used by btree-istore-reduce-refed, btree-clean-alladrs, btree-adrs,
set-basic/node-store/sub-add-03 is used by btree-istore-reduce-refed, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs,
set-basic/node-store/sub-e is used by btree-write-node, btree-clean-alladrs, btree-as-empty-rev, btree-as-empty, btree-adrs,
set-basic/node-store/sub-idem is used by btree-ri-unique, btree-reset-root-frame, btree-mark-dirty, btree-inv-remove-refsize0, btree-inv-crash, btree-inv-alloc, btree-clean-fwd-strong, btree-clean-fwd,
set-basic/node-store/sub-in is used by restrict-further, diff-subseteq-subseteq, diff-eq-diff-eq-union, btree-write-node, btree-restrict-union-proper, btree-reset-root-frame, btree-repl-dirty-address, btree-null, btree-mark-dirty, btree-istore-reduce-refed, btree-inv-crash, btree-inv-alloc, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-clean-adr-in,
set-basic/node-store/sub-insert is used by btree-refed-subseteq-alladrs, btree-clean-alladrs,
set-basic/node-store/sub-ntrans is used by inter-subseteq-simp, btree-refed-subseteq-alladrs, btree-istore-reduce-refed, btree-inv-crash, btree-inv-alloc, btree-adrs,
set-basic/node-store/sub-ntrans-01 is used by inter-subseteq-weaken,
set-basic/node-store/sub-one-01 is used by btree-clean-alladrs,
set-basic/node-store/sub-one-02 is used by btree-refed-subseteq-alladrs, btree-mark-dirty, btree-istore-reduce-refed, btree-inv-format, btree-clean-fwd-strong, btree-clean-fwd, btree-adrs,
set-basic/node-store/sub-trans is used by diff-eq-diff-eq-union, btree-ri-unique, btree-inv-root-null-or-clean, btree-inv-root-null, btree-inv-crash, btree-inv-clean-commit,
set-basic/node-store/subset-empty is used by btree-refed-subseteq-alladrs,
set-basic/node-store/subset-equal is used by btree-istore-reduce-refed,
set-basic/node-store/subset-insert-same is used by btree-refed-subseteq-alladrs,

Used from specification existential

existential/zheap/exists-shift is used by btree-write-other, btree-write-node, btree-ri-unique, btree-refed-subseteq-alladrs, btree-mark-dirty, btree-istore-reduce-refed, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,

Used from specification constants

constants/branchsize-0 is used by btree-write-other, btree-write-node, btree-ri-unique, btree-reset-root-frame, btree-refed-subseteq-alladrs, btree-mark-dirty, btree-istore-reduce-refed, btree-inv-format, btree-inv-crash, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,

Used from specification iter-n

iter-n/zheap/Sep-rec is used by btree-clean-fwd-strong, btree-clean-fwd,
iter-n/zheap/Sep-unfold is used by sep-forall-reduce-true, sep-forall-reduce, btree-ri-unique, btree-refed-subseteq-alladrs, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,
iter-n/zheap/Sep-base is used by sep-forall-reduce-true, sep-forall-reduce,

Used from specification list

list/laddress-list/in-17 is used by btree-inv-format,

Used from specification zbranch-array-ops

zbranch-array-ops/at-range is used by ri-range-ext,
zbranch-array-ops/key-range-replace-branches is used by btree-clean-fwd-strong, btree-clean-fwd,
zbranch-array-ops/range-first is used by ri-range-ext,
zbranch-array-ops/range-inner is used by ri-range-ext,
zbranch-array-ops/unmodified is used by btree-istore-reduce-refed, btree-inv-format, btree-adrs,
zbranch-array-ops/in-keyrange-in-ri is used by ri-range-ext,
zbranch-array-ops/nsize-size is used by btree-refed-subseteq-alladrs, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,
zbranch-array-ops/nsze-ok is used by btree-ri-unique, btree-reset-root-frame, btree-inv-format, btree-inv-crash,
zbranch-array-ops/payload-base is used by btree-inv-format,
zbranch-array-ops/range-last is used by ri-range-ext,
zbranch-array-ops/range-one is used by ri-range-ext,
zbranch-array-ops/unmodified-clean-eq-adr-subseteq is used by btree-clean-fwd-strong,
zbranch-array-ops/unmodified-clean-eq-keys is used by btree-clean-fwd,
zbranch-array-ops/unmodified-clean-eq-keys-subseteq is used by btree-clean-fwd-strong,
zbranch-array-ops/unmodified-clean-fwd-zbrar is used by btree-write-other, btree-refed-subseteq-alladrs, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,
zbranch-array-ops/unmodified-clean-leaf is used by btree-clean-fwd,
zbranch-array-ops/unmodified-clean-leaf-subseteq is used by btree-clean-fwd-strong,
zbranch-array-ops/unmodified-dirty is used by btree-write-other, btree-write-node, btree-root-in-heap, btree-repl-dirty-address, btree-refed-subseteq-alladrs, btree-mark-dirty, btree-istore-reduce-refed, btree-adrs,
zbranch-array-ops/unmodified-same-payload is used by btree-clean-fwd,
zbranch-array-ops/unmodified-same-payload-subseteq is used by btree-clean-fwd-strong,
zbranch-array-ops/unmodified-save is used by btree-write-node,
zbranch-array-ops/unmodified-write-dirty is used by btree-write-other,
zbranch-array-ops/unmodified-write-other is used by btree-write-other,

Used from specification ablock-store-refsize-cons

ablock-store-refsize-cons/index-store/in-remove-refsize0-refsize-cons is used by btree-inv-remove-refsize0, btree-inv-crash,
ablock-store-refsize-cons/index-store/refsize-cons-def is used by btree-inv-format,
ablock-store-refsize-cons/index-store/refsize-cons-remove-refsize0 is used by btree-inv-crash,
ablock-store-refsize-cons/index-store/remove-refsize0-refsize-cons is used by btree-inv-crash,
ablock-store-refsize-cons/index-store/remove-refsize0-subset-refed is used by btree-inv-remove-refsize0,
ablock-store-refsize-cons/index-store/inv-valid-adrs is used by btree-inv-remove-refsize0,
ablock-store-refsize-cons/index-store/refsize-cons-remove-refsize0 is used by btree-inv-remove-refsize0,
ablock-store-refsize-cons/index-store/refsize-cons-write is used by btree-inv-alloc,
ablock-store-refsize-cons/index-store/remove-refsize0-refsize-cons is used by btree-inv-remove-refsize0,
ablock-store-refsize-cons/group-store/restrict-add is used by btree-inv-format,
ablock-store-refsize-cons/group-store/restrict-add-other is used by btree-inv-format,
ablock-store-refsize-cons/group-store/restrict-empty is used by btree-inv-format,
ablock-store-refsize-cons/index-store/restrict-subseteq is used by btree-istore-restrict,
ablock-store-refsize-cons/group-store/size-emp is used by btree-inv-format, btree-inv-alloc,
ablock-store-refsize-cons/group-store/size-rec-simp is used by btree-inv-format,
ablock-store-refsize-cons/index-store/subseteq-dom-nodes-alloc-restrict-empty is used by btree-inv-alloc,

Used from specification address-data

address-data/elim is used by btree-inv-crash,
address-data/sel-03 is used by btree-inv-format,
address-data/sel-04 is used by btree-inv-format,
address-data/sel-05 is used by btree-inv-format,

Used from specification heap

heap/zheap/ext is used by union-eq-empty, eq-union-disj,
heap/zheap/at-del is used by btree-write-node,
heap/zheap/at-uni is used by eq-union-disj,
heap/zheap/at-write is used by btree-sub-clean-write-branches,
heap/zheap/disj-l is used by eq-union-disj,
heap/zheap/disj-r is used by eq-union-disj,
heap/zheap/in-del is used by btree-write-node,
heap/zheap/in-emp is used by union-eq-empty, btree-inv-format,
heap/zheap/in-uni is used by union-eq-empty, eq-union-disj,
heap/zheap/in-write is used by btree-sub-clean-write-branches,
heap/zheap/nonnull is used by btree-write-node, btree-ri-unique, btree-repl-dirty-address, btree-mark-dirty, btree-leaf-fwd, btree-inv-root-null-or-clean, btree-inv-remove-refsize0, btree-inv-clean-commit, btree-dirty-adr-notin, btree-clean-adr-in,
heap/zheap/uni-emp-l is used by union-eq-empty,

Used from specification separation

separation/zheap/free-known is used by btree-write-node, btree-mark-dirty,
separation/zheap/free-unknown is used by btree-write-node, btree-mark-dirty,
separation/zheap/eq-same is used by btree-write-node, btree-mark-dirty,

Used from specification oelem

oelem/nat-set/irreflexivity is used by sep-forall-reduce-true, sep-forall-reduce, ri-range-ext, btree-sub-clean-write-branches, btree-sub-clean-next, btree-ri-unique, btree-clean-fwd-strong, btree-clean-fwd,
oelem/nat-set/ls-le is used by ri-range-ext,

Used from specification address-set-array-ops

address-set-array-ops/in-index-in-union is used by btree-clean-alladrs,
address-set-array-ops/in-union-ext is used by btree-write-node, btree-clean-alladrs,
address-set-array-ops/in-index-in-union is used by btree-restrict-union-proper,
address-set-array-ops/in-index-in-union-1 is used by btree-write-other,
address-set-array-ops/subseteq-union-one is used by btree-refed-subseteq-alladrs, btree-istore-reduce-refed,
address-set-array-ops/subseteq-union-one-add is used by btree-refed-subseteq-alladrs, btree-istore-reduce-refed,
address-set-array-ops/union-subset is used by btree-write-node, btree-refed-subseteq-alladrs, btree-istore-reduce-refed, btree-clean-fwd-strong, btree-clean-fwd, btree-clean-alladrs, btree-adrs,

Used from specification zbranch-array-sorted

zbranch-array-sorted/le-key is used by ri-range-ext,
zbranch-array-sorted/sorted-base is used by ri-range-ext, btree-inv-format,

Used from specification list-del

list-del/index-store/one-03 is used by btree-inv-format,
list-del/laddress-list/pos-one is used by btree-inv-format,

Used from specification array

array/address-set-array/Extension is used by btree-clean-fwd-strong, btree-clean-fwd,
array/zbranch-array/Put-other is used by btree-sub-clean-write-branches,
array/zbranch-array/Put-same is used by btree-sub-clean-write-branches,
array/zbranch-array/Size-mkarray is used by btree-inv-format,

Used from specification Unknown

Unknown/Unknown is used by btree-write-other,
Unknown/Unknown is used by btree-inv-format, btree-inv-crash,
Unknown/Unknown is used by btree-write-other,
Unknown/Unknown is used by btree-inv-crash,
Unknown/Unknown is used by btree-inv-format,
Unknown/Unknown is used by btree-inv-format, btree-inv-crash,
Unknown/Unknown is used by btree-inv-format,
Unknown/Unknown is used by btree-write-other, btree-inv-format,
Unknown/Unknown is used by btree-inv-format,
Unknown/Unknown is used by btree-inv-format,
Unknown/Unknown is used by btree-inv-format,