[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/group-store-ablock-store-nat-store/Diff-base is used by inv-commit,
store+set/group-store-ablock-store-nat-store/Diff-del-rw is used by inv-deallocate-gnd,
store+set/group-store-ablock-store-nat-store/Diff-empty is used by inv-format,
store+set/index-store-address-store/Dom is used by inv-io-save, inv-commit-rec-ind, inv-commit-rec,
store+set/group-store-ablock-store-nat-store/Dom is used by inv-deallocate-gnd,
store+set/group-store-ablock-store-nat-store/diff-add-rem is used by inv-deallocate-gnd,
store+set/group-store-ablock-store-nat-store/dom-del is used by inv-deallocate-gnd,
store+set/index-store-address-store/dom-emp is used by inv-commit-rec-ind,
store+set/group-store-ablock-store-nat-store/dom-emp is used by inv-format,
store+set/index-store-address-store/dom-ins is used by inv-io-save,
store+set/index-store-address-store/dom-restrict is used by inv-commit-rec-ind, inv-commit-rec,
store+set/index-store-address-store/restrict-empty is used by inv-commit-rec-ind,

Used from specification ablock

ablock/index-store/elim is used by inv-io-save, inv-commit-rec, inv-commit,
ablock/index-store/inj is used by inv-io-save,
ablock/index-store/sel-01 is used by inv-io-save, inv-commit-rec, inv-format,
ablock/index-store/sel-02 is used by inv-io-save, inv-commit-rec, inv-format,
ablock/index-store/sel-03 is used by inv-io-save, inv-commit,
ablock/index-store/upd-01 is used by inv-io-save, inv-format,
ablock/index-store/upd-02 is used by inv-io-save, inv-format,
ablock/index-store/upd-03 is used by inv-io-save, inv-commit-rec, inv-format, inv-commit,
ablock/index-store/updsel-28 is used by inv-io-save,

Used from specification nat-basic

nat-basic/a is used by inv-io-save, inv-commit-rec-ind,
nat-basic/add-base is used by inv-io-save, inv-commit-rec-ind,
nat-basic/c is used by inv-io-save, inv-commit-rec-ind,
nat-basic/eq-01 is used by inv-commit-rec-ind,
nat-basic/f is used by inv-io-save, inv-commit-rec-ind, inv-format,
nat-basic/l is used by inv-commit-rec-ind,
nat-basic/l-02 is used by inv-commit-rec-ind,
nat-basic/lf is used by inv-commit-rec-ind,
nat-basic/lf-01 is used by inv-io-save, inv-commit-rec-ind,
nat-basic/lf-02 is used by inv-commit-rec-ind,
nat-basic/oz is used by inv-commit-rec-ind,
nat-basic/s-04 is used by inv-commit-rec-ind,
nat-basic/succ is used by inv-commit-rec-ind,

Used from specification btree-inv

btree-inv/bnode is used by inv-commit-rec-ind,
btree-inv/btree is used by inv-commit-rec-ind,
btree-inv/btree-inv is used by inv-commit-rec,
btree-inv/btree-inv-clean-commit is used by inv-commit,
btree-inv/btree-inv-remove-refsize0 is used by inv-commit,
btree-inv/btree-istore-restrict-to-as is used by inv-commit-rec,
btree-inv/btree-mark-dirty is used by inv-commit-rec,
btree-inv/btree-repl-dirty-address is used by inv-commit-rec,
btree-inv/btree-reset-root is used by inv-commit-rec,
btree-inv/btree-write-node is used by inv-io-save,
btree-inv/commit-inv is used by inv-commit-rec-ind,
btree-inv/inter-subseteq-weaken is used by inv-commit-rec-ind,
btree-inv/btree-adrs is used by inv-io-save, inv-commit-rec-ind, inv-commit-rec,
btree-inv/btree-as-empty is used by inv-commit-rec-ind,
btree-inv/btree-as-empty-rev is used by inv-commit-rec-ind,
btree-inv/btree-clean-adr-in is used by inv-commit-rec-ind, inv-commit-rec,
btree-inv/btree-clean-alladrs is used by inv-commit-rec-ind, inv-commit-rec,
btree-inv/btree-crash is used by inv-commit-rec,
btree-inv/btree-dirty-adr-notin is used by inv-io-save, inv-commit-rec-ind, inv-commit-rec,
btree-inv/btree-imp-dirty is used by inv-io-save, inv-commit-rec-ind,
btree-inv/btree-inv-adr-lnum-in is used by inv-commit,
btree-inv/btree-inv-alloc is used by inv-commit,
btree-inv/btree-inv-crash is used by inv-recover,
btree-inv/btree-inv-format is used by inv-format,
btree-inv/btree-inv-root-neq-null-fwd is used by inv-commit,
btree-inv/btree-istore-restrict is used by inv-commit-rec-ind, inv-commit-rec,
btree-inv/btree-istore-restrict-to-as is used by inv-commit-rec-ind, inv-commit-rec,
btree-inv/btree-leaf-adr is used by inv-commit-rec-ind, inv-commit-rec,
btree-inv/btree-leaf-fwd is used by inv-commit-rec-ind,
btree-inv/btree-refed-subseteq-alladrs is used by inv-io-save, inv-commit-rec-ind, inv-commit-rec,
btree-inv/btree-restrict-union-proper is used by inv-commit-rec-ind,
btree-inv/btree-root-in-heap is used by inv-commit-rec-ind,
btree-inv/btree-sub-clean-0 is used by inv-commit-rec-ind,
btree-inv/btree-sub-clean-leaf is used by inv-commit-rec-ind,
btree-inv/btree-sub-clean-next is used by inv-commit-rec-ind,
btree-inv/diff-subseteq-subseteq is used by inv-commit-rec-ind,
btree-inv/inter-empty-inter-diff-empty is used by inv-commit-rec-ind,
btree-inv/inter-subseteq-simp is used by inv-commit-rec-ind,
btree-inv/inter-union-diff is used by inv-commit-rec-ind,
btree-inv/inter-union-diff-subseteq is used by inv-commit-rec-ind,
btree-inv/maplet-null is used by inv-commit-rec-ind,
btree-inv/nat-le-eq is used by inv-commit-rec-ind,
btree-inv/restrict-dom is used by inv-commit-rec-ind, inv-commit-rec,
btree-inv/subseteq-inter-same is used by inv-commit-rec-ind, inv-commit-rec,
btree-inv/union-diff-same is used by inv-commit-rec-ind,

Used from specification ablock-nodes

ablock-nodes/index-store/in-nodes is used by inv-io-save, inv-commit-rec-ind, inv-commit-rec,
ablock-nodes/index-store/insert-inter-notin-dom-nodes is used by inv-commit-rec-ind,
ablock-nodes/index-store/nodes-alloc is used by inv-io-save,
ablock-nodes/index-store/nodes-alloc-append is used by inv-io-save,
ablock-nodes/index-store/nodes-append is used by inv-io-save,
ablock-nodes/index-store/nodes-write-refsize is used by inv-commit-rec,
ablock-nodes/index-store/prefix-imp-dom-nodes-subset is used by inv-commit-rec-ind, inv-commit-rec,

Used from specification zbranch

zbranch/elim-01 is used by inv-commit-rec-ind,
zbranch/sel-02 is used by inv-commit-rec-ind,
zbranch/test-03 is used by inv-commit-rec-ind,
zbranch/upd-03 is used by inv-commit-rec-ind,

Used from specification znode

znode/elim is used by inv-io-save, inv-commit-rec-ind, inv-commit-rec, inv-commit,
znode/inj is used by inv-commit-rec-ind,
znode/sel-02 is used by inv-commit-rec-ind,
znode/sel-03 is used by inv-commit-rec-ind,
znode/sel-04 is used by inv-commit-rec-ind, inv-commit-rec, inv-commit,
znode/sel-05 is used by inv-commit-rec-ind,
znode/upd-02 is used by inv-commit-rec-ind,
znode/upd-04 is used by inv-io-save, inv-commit-rec, inv-commit,
znode/updsel-01 is used by inv-io-save,
znode/updsel-08 is used by inv-commit-rec-ind,
znode/updsel-18 is used by inv-commit-rec-ind,
znode/updsel-33 is used by inv-commit-rec-ind,

Used from specification heap-sep

heap-sep/zheap/and is used by inv-commit-rec-ind,
heap-sep/zheap/and-ass is used by inv-commit-rec-ind,
heap-sep/zheap/and-com is used by inv-commit-rec-ind,
heap-sep/zheap/prop is used by inv-commit-rec-ind,
heap-sep/zheap/prop-shift is used by inv-commit-rec-ind,
heap-sep/zheap/sep-ass is used by inv-io-save, inv-commit-rec-ind, inv-commit-rec,
heap-sep/zheap/sep-com is used by inv-io-save, inv-commit-rec-ind, inv-commit-rec,

Used from specification ablock-store-inv

ablock-store-inv/index-store/in-alloc is used by inv-commit-rec,
ablock-store-inv/index-store/prefix-append-in is used by inv-io-save,
ablock-store-inv/index-store/flashsize-neq-0 is used by inv-io-save, inv-format,
ablock-store-inv/index-store/in-in-adr is used by inv-io-save,
ablock-store-inv/index-store/in-write-explicit is used by inv-io-save, inv-format,
ablock-store-inv/index-store/in-write-same is used by inv-commit-rec,
ablock-store-inv/group-store/inv-reduce-rem is used by inv-deallocate-gnd,
ablock-store-inv/index-store/inv-remove-refsize0 is used by inv-commit,
ablock-store-inv/group-store/inv-store-empty is used by inv-format,
ablock-store-inv/index-store/inv-store-empty is used by inv-format,
ablock-store-inv/index-store/notin-notin is used by inv-io-save, inv-commit-rec,
ablock-store-inv/index-store/prefix-alloc is used by inv-io-save,
ablock-store-inv/index-store/prefix-append-notin is used by inv-io-save, inv-commit,
ablock-store-inv/index-store/prefix-at is used by inv-commit-rec-ind, inv-commit-rec,
ablock-store-inv/index-store/prefix-empty-left is used by inv-format,
ablock-store-inv/index-store/prefix-fwd-in is used by inv-commit-rec-ind, inv-commit-rec,
ablock-store-inv/index-store/prefix-in is used by inv-commit-rec-ind, inv-commit-rec,
ablock-store-inv/index-store/prefix-notin-fwd is used by inv-io-save, inv-commit-rec-ind,
ablock-store-inv/index-store/prefix-refl is used by inv-io-save, inv-commit-rec-ind, inv-format, inv-commit,
ablock-store-inv/index-store/prefix-trans is used by inv-commit-rec-ind, inv-commit-rec, inv-commit,
ablock-store-inv/group-store/remove-refsize0-empty is used by inv-format,
ablock-store-inv/index-store/remove-refsize0-empty is used by inv-format,
ablock-store-inv/index-store/remove-refsize0-idem is used by inv-commit,
ablock-store-inv/group-store/remove-refsize0-idem is used by inv-commit,
ablock-store-inv/index-store/remove-refsize0-one is used by inv-format,

Used from specification apersistence-base

apersistence-base/crash-gstore-inv is used by inv-recover,
apersistence-base/dom-gstore-crash is used by inv-recover,
apersistence-base/elems-def is used by inv-deallocate-gnd,
apersistence-base/elems-empty is used by inv-format, inv-commit,
apersistence-base/fwd-in-gstore-loghead is used by inv-add-gnds, inv-deallocate-gnd,
apersistence-base/fwd-in-gstore0 is used by inv-deallocate-gnd,
apersistence-base/fwd-inv-iblock is used by inv-io-save, inv-commit-rec, inv-commit,
apersistence-base/fwd-inv-loghead is used by inv-add-gnds, inv-deallocate-gnd,
apersistence-base/icrash-inv is used by inv-recover,
apersistence-base/icrash-remove-refsize0-prefix is used by inv-recover,
apersistence-base/inv-index is used by inv-io-save, inv-commit-rec-ind, inv-commit-rec, inv-get-leb-size, inv-get-block-free-size, inv-sync, inv-format, inv-read-gnd, inv-read-gblock, inv-get-gc-block, inv-add-gnds, inv-set-gblock-refsize, inv-get-gblock-refsize, inv-allocate-gnd, inv-deallocate-gnd, inv-commit, inv-recover, inv-is-log-empty,
apersistence-base/inv-journal is used by inv-io-save, inv-commit-rec-ind, inv-commit-rec, inv-get-leb-size, inv-get-block-free-size, inv-sync, inv-format, inv-read-gnd, inv-read-gblock, inv-get-gc-block, inv-add-gnds, inv-set-gblock-refsize, inv-get-gblock-refsize, inv-allocate-gnd, inv-deallocate-gnd, inv-commit, inv-recover, inv-is-log-empty,
apersistence-base/inv-state is used by inv-io-save, inv-commit-rec-ind, inv-commit-rec, inv-get-leb-size, inv-get-block-free-size, inv-sync, inv-format, inv-read-gnd, inv-read-gblock, inv-get-gc-block, inv-add-gnds, inv-set-gblock-refsize, inv-get-gblock-refsize, inv-allocate-gnd, inv-deallocate-gnd, inv-commit, inv-recover, inv-is-log-empty,

Used from specification nat

nat/add-01 is used by inv-commit-rec-ind,
nat/anti is used by inv-commit-rec-ind,
nat/elim-pred-c is used by inv-commit-rec-ind,
nat/elim-sub is used by inv-commit-rec-ind,
nat/fle-01 is used by inv-commit-rec-ind,
nat/ge is used by inv-commit,
nat/gr-def is used by inv-format,
nat/le-ls-simp is used by inv-commit-rec-ind,
nat/lels is used by inv-io-save, inv-commit-rec-ind, inv-format,
nat/lels-03 is used by inv-commit-rec-ind,
nat/lep is used by inv-commit-rec-ind,
nat/ler is used by inv-commit-rec-ind,
nat/let is used by inv-io-save, inv-commit-rec-ind,
nat/lez is used by inv-io-save, inv-commit-rec-ind, inv-get-block-free-size,
nat/ls is used by inv-commit-rec-ind,
nat/ls-01 is used by inv-commit-rec-ind,
nat/ls-le-simp is used by inv-commit-rec-ind,
nat/prop-07 is used by inv-commit-rec-ind,
nat/succ-01 is used by inv-commit-rec-ind,

Used from specification store

store/index-store-ablock-store-nat-store/At-same is used by inv-io-save, inv-format,
store/group-store-ablock-store-nat-store/Del-in is used by inv-deallocate-gnd,
store/index-store-ablock-store-nat-store/In-empty is used by inv-format,
store/index-store-ablock-store-nat-store/In-insert is used by inv-io-save, inv-format, inv-commit,
store/index-store-ablock-store-nat-store/insin is used by inv-io-save, inv-format, inv-commit,
store/index-store-ablock-store-nat-store/insins is used by inv-io-save, inv-format,
store/index-store-ablock-store-nat-store/notmemlookup is used by inv-commit-rec, inv-commit,

Used from specification set-union

set-union/node-store/delete-shift is used by inv-commit-rec-ind,
set-union/node-store/sub-del-03 is used by inv-commit-rec-ind,
set-union/node-store/subdef is used by inv-commit-rec-ind, inv-commit-rec,
set-union/node-store/unsub-union-01 is used by inv-commit-rec-ind,
set-union/node-store/Difference is used by inv-commit-rec-ind,
set-union/node-store/Intersect is used by inv-commit-rec-ind, inv-commit-rec,
set-union/node-store/One is used by inv-io-save, inv-commit-rec-ind, inv-commit-rec,
set-union/node-store/del-addeq-04 is used by inv-commit-rec-ind,
set-union/node-store/del-addeq-05 is used by inv-commit-rec-ind,
set-union/node-store/del-e-01 is used by inv-commit-rec-ind,
set-union/node-store/del-in is used by inv-commit-rec-ind,
set-union/node-store/diff-union-01 is used by inv-commit-rec-ind,
set-union/nat-set/int-a is used by inv-format, inv-add-gnds, inv-deallocate-gnd, inv-commit,
set-union/node-store/int-a is used by inv-commit-rec-ind, inv-commit-rec,
set-union/nat-set/int-c is used by inv-format, inv-add-gnds, inv-deallocate-gnd, inv-commit,
set-union/node-store/int-c is used by inv-commit-rec-ind, inv-commit-rec,
set-union/nat-set/int-e is used by inv-format, inv-commit,
set-union/node-store/int-e is used by inv-commit-rec-ind, inv-commit-rec,
set-union/nat-set/int-ins is used by inv-deallocate-gnd,
set-union/node-store/int-notempty is used by inv-commit-rec-ind,
set-union/node-store/int-subs01 is used by inv-commit-rec-ind, inv-commit-rec,
set-union/node-store/intu-empty is used by inv-commit-rec-ind,
set-union/node-store/one-min is used by inv-commit-rec-ind, inv-commit-rec,
set-union/nat-set/rem-union-ins is used by inv-deallocate-gnd,
set-union/node-store/sub-ade-02 is used by inv-commit-rec-ind,
set-union/node-store/sub-del-03 is used by inv-commit-rec,
set-union/node-store/sub-union is used by inv-commit-rec-ind, inv-commit-rec,
set-union/node-store/subseteq-inter-empty-empty is used by inv-commit-rec-ind,
set-union/nat-set/una is used by inv-format, inv-add-gnds, inv-deallocate-gnd, inv-commit, inv-recover,
set-union/node-store/una is used by inv-io-save, inv-commit-rec-ind, inv-commit-rec,
set-union/node-store/unadd is used by inv-io-save, inv-commit-rec-ind,
set-union/nat-set/unadd is used by inv-deallocate-gnd,
set-union/nat-set/unc is used by inv-format, inv-add-gnds, inv-deallocate-gnd, inv-commit, inv-recover,
set-union/node-store/unc is used by inv-io-save, inv-commit-rec-ind, inv-commit-rec,
set-union/node-store/undel-02 is used by inv-commit-rec-ind,
set-union/nat-set/une is used by inv-format, inv-commit,
set-union/node-store/une is used by inv-io-save, inv-commit-rec-ind, inv-commit-rec,
set-union/nat-set/uneq is used by inv-recover,
set-union/nat-set/unin-01 is used by inv-deallocate-gnd,
set-union/node-store/uninsert is used by inv-commit-rec-ind,
set-union/node-store/union-rem-unchdg is used by inv-commit-rec-ind,
set-union/nat-set/unsub is used by inv-recover,
set-union/node-store/unsub is used by inv-commit-rec-ind, inv-commit-rec,
set-union/node-store/unsub-union-01 is used by inv-io-save, inv-commit-rec-ind, inv-commit-rec,
set-union/node-store/unsubins-01 is used by inv-commit-rec-ind,

Used from specification error-class

error-class/ecommit is used by inv-sync, inv-format, inv-read-gnd, inv-read-gblock, inv-deallocate-gnd,
error-class/enospc is used by inv-format,
error-class/esuccess is used by inv-io-save, inv-format, inv-read-gblock, inv-deallocate-gnd, inv-commit, inv-recover,
error-class/not-esuccess is used by inv-io-save, inv-commit-rec-ind, inv-format, inv-deallocate-gnd, inv-commit,

Used from specification maplet

maplet/zheap/at-eq is used by inv-commit-rec-ind,
maplet/zheap/map-in is used by inv-commit-rec-ind,
maplet/zheap/map-putex is used by inv-commit-rec-ind,

Used from specification error

error/disj-120 is used by inv-commit,
error/disj-35 is used by inv-format,
error/disj-91 is used by inv-sync, inv-format, inv-read-gnd, inv-read-gblock, inv-deallocate-gnd,

Used from specification set-basic

set-basic/node-store/Extension is used by inv-commit-rec-ind,
set-basic/node-store/sub-add is used by inv-commit-rec,
set-basic/node-store/In-empty is used by inv-commit-rec-ind,
set-basic/node-store/In-insert is used by inv-commit-rec-ind,
set-basic/node-store/Size-insert is used by inv-commit-rec-ind,
set-basic/node-store/eq is used by inv-commit-rec-ind,
set-basic/node-store/eq-02 is used by inv-commit-rec-ind,
set-basic/nat-set/eq-03 is used by inv-deallocate-gnd,
set-basic/node-store/in-03 is used by inv-commit-rec-ind,
set-basic/node-store/in-04 is used by inv-commit-rec-ind,
set-basic/node-store/ne is used by inv-commit-rec-ind,
set-basic/nat-set/ne-01 is used by inv-deallocate-gnd,
set-basic/node-store/ne-01 is used by inv-io-save, inv-commit-rec-ind, inv-commit-rec,
set-basic/node-store/one-size is used by inv-commit-rec-ind,
set-basic/node-store/size-one-01 is used by inv-commit-rec-ind,
set-basic/node-store/size-zero is used by inv-commit-rec-ind,
set-basic/node-store/size-zero-01 is used by inv-commit-rec-ind, inv-commit-rec,
set-basic/node-store/sub-add is used by inv-commit-rec-ind,
set-basic/node-store/sub-add-03 is used by inv-commit-rec-ind,
set-basic/node-store/sub-e is used by inv-commit-rec-ind, inv-commit-rec,
set-basic/node-store/sub-idem is used by inv-commit-rec-ind, inv-commit-rec,
set-basic/node-store/sub-in is used by inv-io-save, inv-commit-rec-ind, inv-commit-rec,
set-basic/node-store/sub-insert is used by inv-commit-rec-ind,
set-basic/node-store/sub-insert-01 is used by inv-commit-rec-ind,
set-basic/node-store/sub-ntrans is used by inv-commit-rec-ind, inv-commit-rec,
set-basic/node-store/sub-ntrans-01 is used by inv-commit-rec-ind, inv-commit-rec,
set-basic/node-store/sub-one-02 is used by inv-commit-rec-ind, inv-commit-rec,
set-basic/node-store/sub-trans is used by inv-io-save, inv-commit-rec-ind, inv-commit-rec,
set-basic/node-store/subset-empty is used by inv-commit-rec-ind,
set-basic/node-store/subset-equal is used by inv-commit-rec-ind, inv-commit-rec,
set-basic/node-store/subset-insert-same is used by inv-commit-rec-ind,

Used from specification list-last

list-last/nat-list-set/lin-01 is used by inv-deallocate-gnd,

Used from specification existential

existential/zheap/exists-shift is used by inv-commit-rec-ind,

Used from specification constants

constants/branchsize-0 is used by inv-commit-rec-ind,

Used from specification laddress

laddress/sel-01 is used by inv-io-save,
laddress/sel-02 is used by inv-io-save,

Used from specification persistence-state

persistence-state/disj-01 is used by inv-io-save, inv-commit-rec-ind, inv-commit-rec, inv-format,
persistence-state/disj-02 is used by inv-add-gnds,
persistence-state/disj-03 is used by inv-io-save, inv-sync, inv-format, inv-commit,
persistence-state/disj-05 is used by inv-io-save, inv-format,
persistence-state/elim-01 is used by inv-add-gnds,
persistence-state/elim-02 is used by inv-io-save, inv-commit-rec-ind, inv-commit-rec,
persistence-state/not-journal-or-index is used by inv-commit-rec,
persistence-state/sel-01 is used by inv-add-gnds,
persistence-state/sel-02 is used by inv-io-save, inv-commit-rec-ind, inv-commit-rec, inv-format, inv-commit,
persistence-state/test-01 is used by inv-io-save, inv-commit-rec-ind, inv-commit-rec, inv-format, inv-commit,
persistence-state/test-02 is used by inv-io-save, inv-sync, inv-format, inv-commit,
persistence-state/test-03 is used by inv-add-gnds,
persistence-state/test-04 is used by inv-io-save, inv-sync, inv-format, inv-commit,
persistence-state/test-07 is used by inv-io-save, inv-commit-rec-ind, inv-commit-rec, inv-format, inv-commit,
persistence-state/test-09 is used by inv-add-gnds,
persistence-state/test-10 is used by inv-sync, inv-format, inv-add-gnds, inv-commit, inv-recover,
persistence-state/test-11 is used by inv-io-save, inv-commit-rec-ind, inv-commit-rec, inv-sync, inv-format, inv-commit, inv-recover,

Used from specification list

list/index-store/Last is used by inv-io-save, inv-format,
list/laddress-list/Last is used by inv-io-save, inv-format,
list/laddress-list/Nil is used by inv-io-save, inv-format,
list/index-store/Nil is used by inv-io-save, inv-format,
list/laddress-list/a is used by inv-io-save, inv-format,
list/index-store/a is used by inv-io-save, inv-format,
list/laddress-list/in-15 is used by inv-io-save,
list/index-store/in-15 is used by inv-io-save,
list/index-store/in-17 is used by inv-io-save,
list/laddress-list/in-17 is used by inv-io-save,
list/laddress-list/in-append is used by inv-io-save,
list/index-store/in-append is used by inv-io-save,
list/laddress-list/in-empty is used by inv-io-save, inv-format,
list/laddress-list/len-02 is used by inv-io-save,
list/index-store/len-02 is used by inv-io-save,

Used from specification zbranch-array-ops

zbranch-array-ops/nsze-ok is used by inv-commit-rec-ind,
zbranch-array-ops/unmodified-dirty is used by inv-commit-rec-ind,

Used from specification list-dup

list-dup/nat-list-set/e-01 is used by inv-format, inv-commit,

Used from specification address-data

address-data/elim is used by inv-io-save, inv-commit-rec, inv-read-gnd, inv-commit,
address-data/inj is used by inv-io-save,
address-data/sel-03 is used by inv-io-save, inv-format, inv-read-gnd,
address-data/sel-04 is used by inv-io-save, inv-format,
address-data/sel-05 is used by inv-io-save, inv-format,

Used from specification ablock-store-refsize-cons

ablock-store-refsize-cons/index-store/refsize-cons-alloc is used by inv-io-save,
ablock-store-refsize-cons/index-store/refsize-cons-append is used by inv-io-save,
ablock-store-refsize-cons/index-store/refsize-cons-remove-index-0 is used by inv-commit-rec,
ablock-store-refsize-cons/index-store/refsize-cons-write is used by inv-io-save,
ablock-store-refsize-cons/group-store/restrict-union is used by inv-io-save,
ablock-store-refsize-cons/group-store/size-emp is used by inv-io-save,
ablock-store-refsize-cons/index-store/subseteq-dom-nodes-alloc-restrict-empty is used by inv-io-save,

Used from specification heap

heap/zheap/at-write is used by inv-io-save, inv-commit-rec,
heap/zheap/in-write is used by inv-io-save, inv-commit-rec,
heap/zheap/in-write-strong is used by inv-commit-rec-ind,
heap/zheap/nonnull is used by inv-commit-rec-ind, inv-commit,

Used from specification separation

separation/zheap/free-known is used by inv-commit-rec-ind,
separation/zheap/free-unknown is used by inv-commit-rec-ind,
separation/zheap/eq-same is used by inv-commit-rec-ind,

Used from specification oelem

oelem/nat-set/irreflexivity is used by inv-commit-rec-ind,
oelem/nat-set/transitivity is used by inv-commit-rec-ind,

Used from specification address-set-array-ops

address-set-array-ops/disj-unique is used by inv-commit-rec-ind,
address-set-array-ops/disj-write is used by inv-commit-rec-ind,
address-set-array-ops/in-index-in-union is used by inv-commit-rec-ind,
address-set-array-ops/inter-union-empty-one-empty is used by inv-commit-rec-ind,
address-set-array-ops/union-subset is used by inv-commit-rec-ind,
address-set-array-ops/union-union-one is used by inv-commit-rec-ind,
address-set-array-ops/union-write is used by inv-commit-rec-ind,

Used from specification array

array/address-set-array/Size-put is used by inv-commit-rec-ind,
array/zbranch-array/Size-put is used by inv-commit-rec-ind,

Used from specification Unknown

Unknown/Unknown is used by inv-add-gnds,
Unknown/Unknown is used by inv-commit,
Unknown/Unknown is used by inv-commit-rec-ind,

Used from specification debug

debug/debug is used by inv-format,

Used from specification iter-n

iter-n/zheap/Sep-unfold is used by inv-commit-rec-ind,

Used from specification apersistence-asm

apersistence-asm/inv-add-ind is used by inv-io-save, inv-format,
apersistence-asm/inv-allocate-gnd is used by inv-allocate-gnd,
apersistence-asm/inv-allocate-ind is used by inv-io-save, inv-format, inv-commit,
apersistence-asm/inv-format is used by inv-format,
apersistence-asm/inv-recovery is used by inv-recover,
apersistence-asm/inv-set-gblock-refsize is used by inv-set-gblock-refsize,
apersistence-asm/inv-set-iblock-refsize is used by inv-io-save, inv-format, inv-commit,
apersistence-asm/inv-sync is used by inv-io-save, inv-format, inv-commit,

Used from specification zbranch-array-sorted

zbranch-array-sorted/keep-sorted is used by inv-commit-rec-ind,