[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 functions

functions/at-apply-succ is used by copy-map,
functions/closed is used by copy-new-node,
functions/closeds is used by copy-new-node, copy-edges-nonempty-term,
functions/dom-alloc is used by smaller, copy-new-node,
functions/dom-write is used by smaller,
functions/inj is used by copy-new-node,
functions/reachable-closed is used by copy-all-reachable-are-fresh,
functions/apply-succ-empty is used by copy-map,
functions/closed-empty is used by copy-node-prepost-empty,
functions/closed-succ is used by copy-new-node,
functions/closed-succ-in is used by copy-new-node, copy-edges-nonempty-term,
functions/closed-succ-rm is used by copy-edges-nonempty-term,
functions/closeds-empty is used by copy-prepost-init, copy-new-node, copy-edges-nonempty-term,
functions/dom is used by smaller, copy-new-node, copy-edges-nonempty-term,
functions/dom-empty is used by smaller, copy-node-prepost-empty,
functions/dom-write is used by copy-new-node,
functions/empty-node is used by copy-new-node, copy-monotone, copy-map,
functions/in-apply-succ is used by copy-map,
functions/inj-empty is used by copy-node-prepost-empty,
functions/inj-eq is used by copy-new-node,
functions/ran is used by copy-edges-nonempty-term,
functions/ran-empty is used by copy-node-prepost-empty,
functions/ran-in-heap-eq is used by copy-new-node, copy-edges-nonempty-term, copy-all-reachable-are-fresh,
functions/ran-put-new is used by copy-new-node,

Used from specification nat-basic1

nat-basic1/f is used by smaller, prove-recursion, copy-new-node,
nat-basic1/lf is used by copy-new-node,
nat-basic1/lf-01 is used by copy-new-node,
nat-basic1/lf-02 is used by copy-new-node,
nat-basic1/ls-02 is used by copy-new-node,
nat-basic1/one is used by copy-new-node,
nat-basic1/one-01 is used by copy-edges-nonempty-term,
nat-basic1/ref-1 is used by smaller, copy-monotone, copy-map, copy-edges-nonempty-term,
nat-basic1/trans-1 is used by copy-new-node,
nat-basic1/zero is used by smaller,

Used from specification heap

heap/node-heap/at-alloc is used by copy-new-node, copy-monotone,
heap/node-heap/disj is used by copy-new-node,
heap/node-heap/exin is used by smaller,
heap/node-heap/ext is used by smaller,
heap/node-heap/in-alloc is used by smaller, copy-new-node,
heap/node-heap/subset is used by subset-trans, subset-eq, copy-new-node, copy-monotone, copy-edges-nonempty-term,
heap/node-heap/subset-uni is used by copy-edges-nonempty-term,
heap/node-heap/uni-ass is used by copy-edges-nonempty-term,
heap/node-heap/uni-inj is used by copy-edges-nonempty-term,
heap/node-heap/uni-write is used by copy-new-node,
heap/node-heap/at-alloc is used by copy-new-node,
heap/node-heap/at-uni is used by copy-new-node, copy-edges-nonempty-term,
heap/node-heap/at-write is used by copy-new-node, copy-monotone,
heap/node-heap/disj-alloc is used by copy-new-node,
heap/node-heap/disj-distr-uni is used by copy-edges-nonempty-term,
heap/node-heap/disj-emp-r is used by copy-node-prepost-empty,
heap/node-heap/disj-l is used by copy-new-node, copy-edges-nonempty-term,
heap/node-heap/disj-r is used by copy-new-node, copy-edges-nonempty-term, copy-all-reachable-are-fresh,
heap/node-heap/disj-swap is used by copy-edges-nonempty-term,
heap/node-heap/disj-write is used by copy-new-node,
heap/node-heap/in-alloc is used by smaller, copy-new-node, copy-monotone, copy-map,
heap/node-heap/in-emp is used by smaller,
heap/node-heap/in-uni is used by in-propagate, copy-new-node, copy-edges-nonempty-term, copy-all-reachable-are-fresh,
heap/node-heap/in-write-strong is used by copy-new-node, copy-monotone,
heap/node-heap/nonnull is used by smaller, copy-new-node, copy-monotone, copy-map,
heap/node-heap/sanity is used by smaller,
heap/node-heap/size-alloc is used by smaller,
heap/node-heap/size-emp is used by smaller,
heap/node-heap/size-write is used by smaller,
heap/node-heap/uni-alloc is used by copy-new-node,
heap/node-heap/uni-emp-r is used by copy-node-prepost-empty,
heap/node-heap/uni-inj is used by copy-prepost-propagate, copy-prepost-init, copy-edges-nonempty-term,
heap/node-heap/write-left is used by copy-new-node,
heap/node-heap/write-right is used by copy-new-node,

Used from specification nat-basic2

nat-basic2/addex is used by copy-new-node,
nat-basic2/a is used by smaller, copy-new-node, copy-monotone, copy-map, copy-edges-nonempty-term,
nat-basic2/ax-08 is used by copy-new-node,
nat-basic2/c is used by smaller, copy-new-node, copy-monotone, copy-map, copy-edges-nonempty-term,
nat-basic2/eq is used by copy-new-node,
nat-basic2/eq-01 is used by copy-new-node,
nat-basic2/l is used by copy-new-node,
nat-basic2/l-01 is used by copy-new-node,
nat-basic2/nls-fst is used by smaller,
nat-basic2/one is used by copy-new-node,
nat-basic2/oz is used by copy-monotone, copy-map,
nat-basic2/s is used by smaller, copy-monotone, copy-map, copy-edges-nonempty-term,
nat-basic2/succ is used by copy-new-node,

Used from specification set-basic

set-basic/refset/Extension is used by copy-edges-nonempty-term,
set-basic/refset/in-03 is used by smaller,
set-basic/refset/rax is used by smaller,
set-basic/refset/sub-add-03 is used by smaller, copy-new-node,
set-basic/refset/sub-e is used by copy-node-prepost-empty,
set-basic/refset/sub-insert-01 is used by smaller,
set-basic/refset/sub-ntrans is used by smaller,
set-basic/refset/subset-empty is used by smaller,

Used from specification store

store/successors/At-other is used by copy-map, copy-edges-nonempty-term,
store/ref-map/At-other is used by copy-new-node,
store/successors/In-insert is used by copy-map,
store/ref-map/Subset is used by copy-new-node, copy-monotone, copy-map,
store/ref-map/exin is used by smaller,
store/successors/exnotempty is used by copy-edges-nonempty-term,
store/successors/k-Extension is used by copy-map,
store/ref-map/At-in-out is used by copy-new-node, copy-monotone,
store/successors/At-same is used by copy-map, copy-edges-nonempty-term,
store/ref-map/At-same is used by copy-new-node, copy-map,
store/successors/Del-at is used by copy-map,
store/successors/Del-in is used by copy-map,
store/ref-map/In-empty is used by copy-term, copy-no-effects, copy-all-reachable-are-fresh,
store/successors/In-insert is used by copy-edges-nonempty-term,
store/ref-map/In-insert is used by copy-new-node, copy-monotone,
store/ref-map/Size-insert is used by smaller, copy-new-node,
store/ref-map/empty is used by smaller, copy-new-node,
store/successors/empty is used by copy-edges-nonempty-term,
store/ref-map/in-neq is used by copy-new-node,
store/successors/in-neq is used by copy-edges-nonempty-term,
store/ref-map/insin is used by copy-new-node, copy-map,
store/successors/insin is used by copy-edges-nonempty-term,
store/successors/size is used by copy-edges-nonempty-term,
store/ref-map/sub-ref is used by copy-monotone, copy-edges-nonempty-term,
store/ref-map/sub-trans is used by copy-monotone, copy-map, copy-edges-nonempty-term,
store/ref-map/subset-elem-eq-02 is used by copy-map,
store/ref-map/subset-empty is used by copy-all-reachable-are-fresh,
store/ref-map/subset-size is used by subset-smaller,

Used from specification nat

nat/elim-pred-c is used by copy-monotone, copy-map,
nat/elim-sub is used by copy-new-node,
nat/eq-02 is used by copy-new-node,
nat/fle is used by copy-new-node,
nat/le-add is used by copy-new-node,
nat/le-ls-simp is used by copy-new-node,
nat/lels is used by smaller, copy-new-node,
nat/lels-01 is used by subset-smaller, smaller, copy-new-node, copy-edges-nonempty-term,
nat/lels-02 is used by copy-new-node,
nat/lels-03 is used by copy-new-node,
nat/lep is used by copy-new-node,
nat/lep-02 is used by copy-new-node,
nat/let is used by copy-new-node,
nat/ls-01 is used by copy-edges-nonempty-term,
nat/ls-03 is used by copy-new-node,
nat/pred-03 is used by copy-monotone, copy-map, copy-edges-nonempty-term,
nat/succ-01 is used by smaller, copy-new-node,
nat/zero-01 is used by copy-new-node,
nat/zero-02 is used by copy-new-node,

Used from specification node

node/elim is used by copy-new-node, copy-monotone, copy-map,
node/inj is used by copy-new-node,

Used from specification store+set

store+set/ref-map-store+set-r/Dom is used by smaller, copy-edges-nonempty-term,
store+set/ref-map-store+set-r/In-data-in is used by copy-edges-nonempty-term,
store+set/ref-map-store+set-r/dom-emp is used by copy-node-prepost-empty,
store+set/ref-map-store+set-r/dom-ins is used by smaller, copy-new-node,
store+set/ref-map-store+set-r/dom-isemp is used by smaller,

Used from specification ops-impl

ops-impl/node-heap/infinite-mem is used by copy-new-node,

Used from specification set-union

set-union/refset/subdef is used by smaller, copy-edges-nonempty-term,