Used simplifier rules/spec theorems by specification

Used from specification linked-tree

• linked-tree/tr-fold is used by delete-prepost-loop,
• linked-tree/tr-fold-singleton is used by insert-prepost,
• linked-tree/tr-rec is used by insert-prepost, delete-prepost-loop, delete-prepost,
• linked-tree/tr-unfold is used by insert-prepost, delete-prepost-loop,
• linked-tree/tr-base is used by root-nonnull, insert-prepost, delete-prepost-loop,
• linked-tree/tr-branch is used by delete-prepost-loop,
• linked-tree/tr-fold is used by insert-prepost, delete-prepost,
• linked-tree/tr-null is used by insert-prepost, delete-prepost-loop, delete-prepost,

Used from specification node

• node/elim is used by insert-prepost, delete-prepost-loop, delete-prepost,
• node/inj is used by insert-prepost, delete-prepost-loop, delete-prepost,
• node/sel-01 is used by delete-prepost,
• node/sel-02 is used by insert-prepost, delete-prepost,
• node/sel-03 is used by delete-prepost-loop,
• node/upd-01 is used by mknode-prepost, insert-prepost,
• node/upd-02 is used by mknode-prepost,
• node/upd-03 is used by mknode-prepost, insert-prepost, delete-prepost-loop, delete-prepost,

Used from specification heap-sep

• heap-sep/node-heap/and is used by insert-prepost, delete-prepost-loop, delete-prepost,
• heap-sep/node-heap/and-ass is used by root-nonnull, insert-prepost, delete-prepost-loop, delete-prepost,
• heap-sep/node-heap/and-com is used by root-nonnull, insert-prepost, delete-prepost-loop, delete-prepost,
• heap-sep/node-heap/emp-sep is used by insert-prepost, delete-prepost-loop, delete-prepost,
• heap-sep/node-heap/false-and is used by root-nonnull, delete-prepost-loop,
• heap-sep/node-heap/false-rev is used by root-nonnull, delete-prepost-loop,
• heap-sep/node-heap/false-sep is used by root-nonnull, delete-prepost-loop,
• heap-sep/node-heap/falseH is used by root-nonnull, delete-prepost-loop,
• heap-sep/node-heap/prop is used by insert-prepost, delete-prepost-loop, delete-prepost,
• heap-sep/node-heap/prop-shift is used by insert-prepost, delete-prepost-loop, delete-prepost,
• heap-sep/node-heap/sep-ass is used by root-nonnull, mknode-prepost, insert-prepost, delete-prepost-min, delete-prepost-loop, delete-prepost,
• heap-sep/node-heap/sep-com is used by root-nonnull, mknode-prepost, insert-prepost, delete-prepost-min, delete-prepost-loop, delete-prepost,
• heap-sep/node-heap/sep-mp-p is used by delete-prepost-loop,
• heap-sep/node-heap/sep-partial-mp-2 is used by delete-prepost-loop,
• heap-sep/node-heap/wand-same-emp-p is used by delete-prepost-loop,

Used from specification nat

• nat/add-num-03 is used by insert-prepost, delete-prepost,

Used from specification maplet

• maplet/node-heap/ex2-shiftw-inst is used by delete-prepost-loop,
• maplet/node-heap/mapex is used by mknode-prepost,
• maplet/node-heap/at-eq is used by insert-prepost, delete-prepost-loop, delete-prepost,
• maplet/node-heap/ex2-shift is used by insert-prepost, delete-prepost,
• maplet/node-heap/ex3-shift is used by mknode-prepost,

Used from specification tree

• tree/disj is used by leftmost-ismin, leftmost-in, delete-prepost-min, delete-prepost-loop, delete-prepost, butleftmost-in, butleftmost-bst,
• tree/inj is used by insert-prepost, delete-prepost-min, delete-prepost,
• tree/size-01 is used by insert-prepost, delete-prepost,

Used from specification nat-basic2

• nat-basic2/a is used by insert-prepost, delete-prepost,
• nat-basic2/c is used by insert-prepost, delete-prepost,
• nat-basic2/l is used by insert-prepost, delete-prepost,
• nat-basic2/succ is used by insert-prepost, delete-prepost,

Used from specification heap

• heap/node-heap/nonnull is used by insert-prepost, delete-prepost-loop, delete-prepost,

Used from specification separation

• separation/node-heap/assign-known is used by mknode-prepost, insert-prepost, delete-prepost-loop, delete-prepost,
• separation/node-heap/eq-cong-injl is used by delete-prepost,
• separation/node-heap/free-known is used by delete-prepost-loop, delete-prepost,

Used from specification oelem

• oelem/irreflexivity is used by leftmost-ismin, insert-bst, delete-prepost-min, butleftmost-in, bst-elem-in-branch,
• oelem/lel is used by insert-prepost,
• oelem/ls-le is used by insert-prepost, insert-in, insert-bst,
• oelem/nen is used by insert-in, insert-bst,
• oelem/nll is used by insert-bst, delete-prepost-min,
• oelem/seq is used by insert-prepost, insert-in, insert-bst,
• oelem/sls is used by leftmost-ismin,
• oelem/transitivity is used by leftmost-ismin, insert-bst, delete-prepost-min, butleftmost-in,

Used from specification nat-basic1

• nat-basic1/one is used by insert-prepost, delete-prepost,

Used from specification ops

• ops/node-heap/alloc is used by mknode-prepost,