[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/node-store/Diff-base is used by refine-gc,
store+set/group-store-ablock-store-nat-store/Diff-del-rw is used by refine-gc,
store+set/group-store-ablock-store-nat-store/Diff-ext is used by refine-commit,
store+set/group-store-ablock-store-nat-store/Diff-mems-get is used by refine-commit,
store+set/group-store-ablock-store-nat-store/Dom is used by prepost-restore-log, refine-commit, refine-check-commit, refine-gc,
store+set/node-store/Dom is used by refine-gc,
store+set/group-store-ablock-store-nat-store/diff-add-rem is used by refine-gc,
store+set/group-store-ablock-store-nat-store/dom-add-in is used by refine-remove,
store+set/group-store-ablock-store-nat-store/dom-del is used by refine-gc,
store+set/group-store-ablock-store-nat-store/dom-ins is used by refine-remove,

Used from specification nat-basic

nat-basic/a is used by prepost-restore-log, prepost-remove-nonend-blocks, refine-add5, refine-add4, refine-add3, refine-add2, refine-add1, refine-remove,
nat-basic/add-base is used by prepost-remove-nonend-blocks,
nat-basic/c is used by prepost-restore-log, prepost-remove-nonend-blocks, refine-add5, refine-add4, refine-add3, refine-add2, refine-add1, refine-remove,
nat-basic/eq-01 is used by prepost-remove-nonend-blocks,
nat-basic/f is used by refine-add5, refine-add4, refine-add3, refine-remove,
nat-basic/l-02 is used by prepost-remove-nonend-blocks,
nat-basic/lf-01 is used by refine-add5, refine-add4, refine-add3,
nat-basic/nls-fst is used by prepost-remove-nonend-blocks,
nat-basic/one is used by refine-add5, refine-add4, refine-add3, refine-add2,
nat-basic/one-01 is used by prepost-remove-nonend-blocks,
nat-basic/one-06 is used by refine-add5, refine-add4, refine-add3, refine-add2, refine-add1,
nat-basic/oz is used by prepost-remove-nonend-blocks,
nat-basic/s-04 is used by prepost-restore-log, prepost-remove-nonend-blocks,
nat-basic/succ is used by prepost-restore-log, prepost-remove-nonend-blocks, refine-add5, refine-add4, refine-add3, refine-add2, refine-add1,
nat-basic/z-01 is used by prepost-remove-nonend-blocks,
nat-basic/zero is used by prepost-remove-nonend-blocks, refine-add5, refine-add4, refine-add3, refine-add2, refine-add1,

Used from specification ablock

ablock/group-store/elim is used by prepost-restore-log, prepost-remove-nonend-blocks, refine-commit, refine-check-commit, refine-gc, refine-remove,
ablock/group-store/inj is used by refine-commit, refine-gc, refine-remove,
ablock/group-store/sel-01 is used by prepost-remove-nonend-blocks, refine-gc, refine-remove,
ablock/group-store/sel-02 is used by prepost-restore-log, prepost-remove-nonend-blocks, refine-gc, refine-remove,
ablock/group-store/upd-03 is used by refine-remove,

Used from specification list+set

list+set/address-list-set/toSet-empty is used by refine-gc,
list+set/key-list-set/toSet-empty is used by refine-gc,
list+set/address-list-set/toSet-ext is used by refine-gc,

Used from specification aubifs-inv

aubifs-inv/ri-cons-in is used by refine-lookup,
aubifs-inv/ri-cons-inj is used by refine-add5, refine-check-commit, refine-gc, refine-add4, refine-add3, refine-add2, refine-add1,
aubifs-inv/ri-cons-range-ri is used by refine-gc,
aubifs-inv/ri-cons-variant1-01 is used by refine-commit, refine-check-commit, refine-gc, refine-lookup,
aubifs-inv/ri-inj-del is used by refine-remove,

Used from specification aubifs-base

aubifs-base/read-split is used by refine-gc,
aubifs-base/index-lookup-base is used by refine-gc,
aubifs-base/index-update-key-base is used by refine-gc,
aubifs-base/new-base is used by refine-add5, refine-gc, refine-add4, refine-add3, refine-add2, refine-add1,
aubifs-base/new-one is used by refine-add5, refine-add4, refine-add3, refine-add2, refine-add1,
aubifs-base/new-rec is used by refine-add5, refine-add4, refine-add3, refine-add2, refine-add1,
aubifs-base/range is used by refine-commit, refine-gc,
aubifs-base/read-base is used by refine-gc,
aubifs-base/read-length is used by refine-gc,
aubifs-base/write-base is used by refine-gc,
aubifs-base/write-dom is used by refine-gc,
aubifs-base/write-one is used by refine-add5, refine-add4, refine-add3, refine-add2, refine-add1,
aubifs-base/write-rec is used by refine-add5, refine-add4, refine-add3, refine-add2,

Used from specification key

key/elim-01 is used by refine-orphans-contains,
key/inodekey-id is used by refine-orphans-remove, refine-orphans-insert,
key/test-02 is used by refine-orphans-contains,

Used from specification ablock-store-inv

ablock-store-inv/group-store/prefixn-to-adrs is used by prepost-remove-nonend-blocks,
ablock-store-inv/group-store/addresslist-length is used by prepost-remove-nonend-blocks, refine-gc,
ablock-store-inv/group-store/adrs-empty is used by prepost-remove-nonend-blocks,
ablock-store-inv/group-store/in-remove-refsize0 is used by refine-commit, refine-check-commit,
ablock-store-inv/group-store/inv-eq-list-size is used by prepost-remove-nonend-blocks, refine-gc,
ablock-store-inv/group-store/inv-nodups is used by refine-gc,
ablock-store-inv/group-store/inv-prefixn-lax is used by prepost-remove-nonend-blocks,
ablock-store-inv/group-store/inv-reduce-rem is used by refine-gc,
ablock-store-inv/group-store/prefixn-to-adrs is used by prepost-restore-log, prepost-remove-nonend-blocks,
ablock-store-inv/group-store/to-adrs-eq is used by prepost-remove-nonend-blocks, refine-gc,
ablock-store-inv/group-store/to-adrs-eq-empty is used by prepost-remove-nonend-blocks,
ablock-store-inv/group-store/to-ards-no-dups is used by refine-gc,

Used from specification apersistence-base

apersistence-base/crash-gstore-inv is used by recovery,
apersistence-base/dom-gstore-crash is used by recovery,
apersistence-base/elems-def is used by prepost-restore-log, refine-gc,
apersistence-base/elems-in-notin-ginval is used by refine-gc,
apersistence-base/elems-log-subset-gstore-union-ginval is used by recovery,
apersistence-base/fwd-in-gstore0 is used by refine-gc,
apersistence-base/fwd-in-log-in-gstore is used by refine-gc,
apersistence-base/fwd-inv-gblock-rem is used by prepost-restore-log, prepost-remove-nonend-blocks, refine-gc,
apersistence-base/inv-journal is used by refine-add5, refine-sync, recovery, refine-orphans-remove, refine-orphans-insert, refine-orphans-contains, refine-commit, refine-check-commit, refine-gc, refine-add4, refine-add3, refine-add2, refine-add1, refine-get, refine-entries, refine-truncate, refine-remove, refine-store, refine-lookup, refine-contains, refine-newino,

Used from specification nat

nat/add-01 is used by prepost-remove-nonend-blocks,
nat/add-num-04 is used by refine-add5, refine-add4, refine-add3, refine-add2,
nat/elim-pred-c is used by prepost-remove-nonend-blocks,
nat/elim-sub is used by refine-remove,
nat/eq-02 is used by prepost-remove-nonend-blocks,
nat/fle is used by refine-add5, refine-add4,
nat/ge is used by refine-remove,
nat/le-def is used by prepost-remove-nonend-blocks, refine-remove,
nat/le-ls-simp is used by refine-newino,
nat/lels is used by prepost-remove-nonend-blocks, refine-add5, refine-add4, refine-add3,
nat/lep is used by refine-remove,
nat/let is used by refine-gc,
nat/ls-01 is used by prepost-remove-nonend-blocks,
nat/not-zero is used by refine-add5, refine-add4, refine-add3,
nat/succ-01 is used by prepost-remove-nonend-blocks,

Used from specification store

store/group-store-ablock-store-nat-store/At-other is used by refine-remove,
store/group-store-ablock-store-nat-store/At-same is used by refine-remove,
store/group-store-ablock-store-nat-store/In-insert is used by refine-remove,
store/group-store-ablock-store-nat-store/in-neq is used by refine-remove,
store/group-store-ablock-store-nat-store/insin is used by refine-remove,
store/node-index/notin-del-notin is used by refine-remove,

Used from specification set-union

set-union/nat-set/subdef is used by prepost-restore-log, refine-gc,
set-union/node-store/union-inter-inter-union is used by refine-gc,
set-union/nat-set/Intersect is used by prepost-restore-log, refine-commit, refine-check-commit,
set-union/node-store/Intersect is used by refine-commit, refine-gc,
set-union/node-store/int-a is used by refine-commit, refine-gc,
set-union/nat-set/int-a is used by prepost-restore-log, recovery, refine-commit, refine-check-commit, refine-gc,
set-union/nat-set/int-c is used by prepost-restore-log, recovery, refine-commit, refine-check-commit, refine-gc,
set-union/node-store/int-c is used by refine-commit, refine-gc,
set-union/node-store/int-e is used by refine-gc,
set-union/nat-set/int-ins is used by refine-gc,
set-union/nat-set/rem-union-ins is used by refine-gc,
set-union/nat-set/sub-del-04 is used by refine-gc,
set-union/nat-set/una is used by recovery, refine-gc,
set-union/node-store/una is used by refine-gc,
set-union/nat-set/unadd is used by refine-gc,
set-union/nat-set/unc is used by recovery, refine-gc,
set-union/node-store/unc is used by refine-gc,
set-union/node-store/une is used by refine-gc,

Used from specification error-class

error-class/ecommit is used by prepost-remove-nonend-blocks, refine-sync, recovery, refine-commit, refine-get, refine-entries, refine-lookup, refine-contains, initialization,
error-class/esuccess is used by prepost-remove-nonend-blocks, refine-sync, recovery, refine-commit, refine-gc, refine-get, refine-entries, refine-lookup, refine-contains, initialization,
error-class/not-esuccess is used by prepost-remove-nonend-blocks, refine-add5, refine-sync, recovery, refine-commit, refine-check-commit, refine-gc, refine-add4, refine-add3, refine-add2, refine-add1, refine-get, refine-entries, refine-lookup, refine-contains, initialization,

Used from specification error

error/disj-35 is used by refine-gc,
error/disj-91 is used by prepost-remove-nonend-blocks, refine-sync, recovery, refine-commit, refine-get, refine-entries, refine-lookup, refine-contains, initialization,

Used from specification set-basic

set-basic/nat-set/Extension is used by prepost-restore-log, refine-commit, refine-check-commit,
set-basic/node-store/Extension is used by refine-commit, refine-gc,
set-basic/nat-set/In-empty is used by prepost-restore-log, refine-commit, refine-check-commit,
set-basic/node-store/In-empty is used by refine-commit, refine-gc,
set-basic/nat-set/add-01 is used by refine-gc,
set-basic/nat-set/eq is used by refine-gc,
set-basic/nat-set/eq-03 is used by refine-gc,
set-basic/node-store/ne-01 is used by refine-commit,
set-basic/nat-set/ne-01 is used by prepost-restore-log, refine-commit, refine-check-commit, refine-gc, refine-get, refine-newino,
set-basic/nat-set/size-zero is used by refine-commit, refine-check-commit,
set-basic/node-store/size-zero is used by refine-commit, refine-gc,
set-basic/nat-set/size-zero-01 is used by prepost-restore-log, refine-commit, refine-check-commit, refine-gc, refine-get, refine-newino,
set-basic/node-store/size-zero-01 is used by refine-commit, refine-gc,
set-basic/node-index/sub-e is used by refine-gc,
set-basic/nat-set/sub-trans is used by refine-add5, refine-gc, refine-add4, refine-add3, refine-add2, refine-add1,

Used from specification list-last

list-last/address-list-set/bapp is used by prepost-remove-nonend-blocks,
list-last/group-store/butlast-def is used by prepost-remove-nonend-blocks,
list-last/group-store/last-def is used by prepost-remove-nonend-blocks,
list-last/group-store/lb is used by prepost-remove-nonend-blocks,

Used from specification gjournal-base

gjournal-base/index-update-range is used by refine-gc,
gjournal-base/new-inter-empty is used by refine-gc,
gjournal-base/referenced-adrs-lookup-keys-nodups is used by refine-gc,
gjournal-base/referenced-adrs-split is used by refine-gc,
gjournal-base/inos-greater-notin is used by refine-newino,
gjournal-base/inos-greater-rem is used by refine-truncate,
gjournal-base/inos-write is used by refine-store,
gjournal-base/keys-app is used by refine-gc,
gjournal-base/keys-base is used by initialization,
gjournal-base/keys-base-01 is used by refine-gc,
gjournal-base/keys-inodekey-in is used by refine-orphans-contains, refine-newino,
gjournal-base/keys-inodekeys is used by refine-check-commit,
gjournal-base/keys-len is used by refine-gc,
gjournal-base/keys-rec-full is used by refine-orphans-insert,
gjournal-base/keys-rem is used by refine-orphans-remove,
gjournal-base/lebs-in-ri-in-gstore is used by refine-commit, refine-gc,
gjournal-base/lebs-in-ri-in-gstore-explicit is used by refine-remove, refine-lookup,
gjournal-base/lebs-index is used by refine-gc,
gjournal-base/referenced-adrs-lookup-key-cons is used by refine-gc,
gjournal-base/referenced-adrs-lookup-keys-in-dom is used by refine-gc,
gjournal-base/referenced-adrs-lookup-keys-lookup is used by refine-gc,

Used from specification list-prefixn

list-prefixn/laddress-list/prefixn is used by prepost-remove-nonend-blocks,
list-prefixn/address-list-set/prefixn-butlast is used by prepost-remove-nonend-blocks,
list-prefixn/laddress-list/prefixn-0 is used by prepost-remove-nonend-blocks,
list-prefixn/laddress-list/prefixn-empty is used by prepost-remove-nonend-blocks,
list-prefixn/laddress-list/prefixn-eq-empty is used by prepost-remove-nonend-blocks,
list-prefixn/laddress-list/prefixn-fulln is used by prepost-remove-nonend-blocks,
list-prefixn/group-store/prefixn-le-eq is used by refine-remove,
list-prefixn/laddress-list/prefixn-neq-empty-plusone is used by prepost-remove-nonend-blocks,
list-prefixn/laddress-list/prefixn-prepend-one is used by prepost-remove-nonend-blocks,

Used from specification list-data

list-data/nat-list-set/elim-list-c is used by prepost-restore-log,
list-data/address-list-set/elim-list-c is used by refine-add5, refine-add4, refine-add3, refine-add2, refine-add1,
list-data/group-store/l is used by prepost-remove-nonend-blocks,
list-data/address-list-set/l is used by refine-add5, refine-add4, refine-add3, refine-add2, refine-add1,
list-data/address-list-set/size-01 is used by refine-add5, refine-gc, refine-add4, refine-add3, refine-add2, refine-add1,
list-data/laddress-list/size-01 is used by prepost-remove-nonend-blocks,
list-data/key-list-set/size-01 is used by refine-gc,
list-data/group-store/size-01 is used by prepost-remove-nonend-blocks,

Used from specification list

list/group-store/lastdiv-rew is used by prepost-remove-nonend-blocks,
list/address-list-set/Last is used by refine-add5, refine-add4, refine-add3, refine-add2, refine-add1,
list/group-store/Nil is used by prepost-remove-nonend-blocks, refine-gc,
list/address-list-set/Nil is used by refine-gc,
list/nat-list-set/a is used by prepost-restore-log,
list/key-list-set/a is used by refine-gc,
list/address-list-set/a is used by prepost-restore-log, prepost-remove-nonend-blocks, refine-add5, refine-gc, refine-add4, refine-add3, refine-add2, refine-add1,
list/laddress-list/a is used by prepost-remove-nonend-blocks, refine-gc,
list/node-list/a is used by refine-add5, refine-gc, refine-add4, refine-add3, refine-add2,
list/group-store/a is used by prepost-remove-nonend-blocks, refine-gc,
list/address-list-set/app is used by prepost-remove-nonend-blocks, refine-add5, refine-gc, refine-add4, refine-add3, refine-add2, refine-add1,
list/nat-list-set/app is used by prepost-restore-log,
list/key-list-set/app is used by refine-gc,
list/node-list/app is used by refine-gc,
list/address-list-set/app-01 is used by prepost-restore-log, prepost-remove-nonend-blocks,
list/group-store/app-01 is used by prepost-remove-nonend-blocks,
list/laddress-list/app-02 is used by prepost-remove-nonend-blocks,
list/address-list-set/app-02 is used by prepost-remove-nonend-blocks,
list/nat-list-set/app-03 is used by prepost-restore-log,
list/group-store/app-04 is used by prepost-remove-nonend-blocks,
list/nat-list-set/app-05 is used by prepost-restore-log,
list/nat-list-set/c is used by prepost-restore-log,
list/address-list-set/c is used by refine-add5, refine-add4, refine-add3, refine-add2, refine-add1,
list/group-store/c is used by prepost-remove-nonend-blocks,
list/node-list/c is used by refine-add5, refine-add4, refine-add3, refine-add2,
list/laddress-list/c is used by prepost-remove-nonend-blocks,
list/laddress-list/e is used by prepost-remove-nonend-blocks,
list/address-list-set/e-01 is used by refine-add5, refine-add4, refine-add3, refine-add2, refine-add1,
list/nat-list-set/e-01 is used by prepost-restore-log,
list/address-list-set/in-06 is used by refine-add5, refine-add4, refine-add3, refine-add2,
list/address-list-set/in-12 is used by refine-gc,
list/address-list-set/in-15 is used by refine-add5, refine-add4, refine-add3, refine-add2, refine-add1,
list/address-list-set/in-17 is used by refine-add5, refine-add4, refine-add3,
list/nat-list-set/in-append is used by prepost-restore-log,
list/address-list-set/in-empty is used by refine-add5, refine-add4, refine-add3, refine-add2, refine-add1,
list/nat-list-set/in-rec is used by prepost-restore-log,
list/address-list-set/in-rec is used by refine-add5, refine-add4, refine-add3,
list/group-store/len is used by prepost-remove-nonend-blocks,
list/laddress-list/len is used by refine-gc,
list/node-list/len-02 is used by refine-add5, refine-add4, refine-add3, refine-add2, refine-add1,
list/group-store/len-02 is used by prepost-remove-nonend-blocks,
list/nat-list-set/len-05 is used by prepost-restore-log,
list/address-list-set/len-05 is used by refine-add5, refine-add4, refine-add3, refine-add2, refine-add1,
list/group-store/len-05 is used by prepost-remove-nonend-blocks,
list/node-list/len-05 is used by refine-add5, refine-add4, refine-add3, refine-add2,
list/laddress-list/len-05 is used by prepost-remove-nonend-blocks,

Used from specification list-dup

list-dup/key-list-set/a is used by refine-gc,
list-dup/address-list-set/c is used by refine-add1,
list-dup/address-list-set/dups-cons is used by refine-add5, refine-add4, refine-add3, refine-add2, refine-add1,
list-dup/key-list-set/e-01 is used by refine-gc,
list-dup/address-list-set/e-01 is used by refine-add5, refine-gc, refine-add4, refine-add3, refine-add2, refine-add1,
list-dup/address-list-set/rec is used by refine-add5, refine-add4, refine-add3,
list-dup/address-list-set/two-01 is used by refine-add5, refine-add4, refine-add3, refine-add2,

Used from specification address-data

address-data/elim is used by refine-commit, refine-gc, refine-get, refine-remove, refine-lookup,
address-data/sel-03 is used by refine-commit, refine-get, refine-remove, refine-lookup,

Used from specification ablock-store-refsize-cons

ablock-store-refsize-cons/group-store/restrict-leb is used by refine-gc,
ablock-store-refsize-cons/group-store/restrict-union is used by refine-gc,
ablock-store-refsize-cons/group-store/restrict-union-inter-empty-left is used by refine-gc,

Used from specification oelem

oelem/nat-set/irreflexivity is used by prepost-restore-log, prepost-remove-nonend-blocks, refine-remove,

Used from specification gjournal-abs

gjournal-abs/abs-log-new is used by refine-gc,
gjournal-abs/abs-log-no-change-eq is used by refine-remove,
gjournal-abs/down-block is used by refine-commit,
gjournal-abs/ladr-split is used by refine-gc,
gjournal-abs/nodes-gstore-in is used by refine-get,
gjournal-abs/nodes-referenced-adrs-leb is used by refine-gc,
gjournal-abs/nodes-remove-refsize0 is used by refine-commit,
gjournal-abs/nodes-write-nochange is used by refine-remove,
gjournal-abs/refsize0-addresses is used by refine-commit,
gjournal-abs/abs-log-adr-explicit-in-leb-notin is used by refine-gc,
gjournal-abs/abs-log-append-one is used by prepost-restore-log,
gjournal-abs/abs-log-base is used by prepost-restore-log, refine-commit, initialization,
gjournal-abs/abs-log-del is used by refine-gc,
gjournal-abs/abs-log-except-refsize-down is used by refine-truncate, refine-store,
gjournal-abs/abs-log-gcrash-down is used by recovery,
gjournal-abs/abs-log-toset-inter-restr-empty is used by refine-gc,
gjournal-abs/adr-in-ri-in-gstore is used by refine-lookup,
gjournal-abs/adr-in-ri-leb-notin-ginval is used by refine-lookup,
gjournal-abs/adresses-restr-subseteq is used by refine-gc,
gjournal-abs/dom-remove-refsize0-down is used by refine-commit,
gjournal-abs/down-block-explicit is used by prepost-restore-log, refine-remove,
gjournal-abs/down-empty is used by initialization,
gjournal-abs/down-store-adr-in-explicit is used by refine-commit, refine-get,
gjournal-abs/down-store-at is used by prepost-restore-log, refine-commit, refine-get, refine-remove,
gjournal-abs/down-store-at-diff is used by refine-commit,
gjournal-abs/down-store-dealloc is used by refine-gc,
gjournal-abs/down-store-in is used by refine-gc, refine-remove,
gjournal-abs/down-store-write is used by refine-remove,
gjournal-abs/ginval-down is used by refine-commit,
gjournal-abs/in-nodes-down-at-same is used by refine-get, refine-store, refine-lookup,
gjournal-abs/lebs-dom-remove-refsize0 is used by refine-commit, refine-check-commit,
gjournal-abs/nodes-crash-down is used by recovery,
gjournal-abs/nodes-dealloc is used by refine-gc,
gjournal-abs/nodes-empty is used by initialization,
gjournal-abs/nodes-except-refsize-down is used by refine-truncate, refine-store,
gjournal-abs/nodes-gstore-at is used by refine-get, refine-store, refine-lookup,
gjournal-abs/notin-notin-nodes-down is used by refine-get, refine-store,
gjournal-abs/refsize-0-notin-index is used by refine-commit, refine-gc,
gjournal-abs/refsize-nonzero-notin-ginval is used by refine-commit, refine-check-commit, refine-gc,
gjournal-abs/remove-nonend-inv is used by prepost-remove-nonend-blocks,
gjournal-abs/remove-refsize0-down is used by refine-commit,
gjournal-abs/restore-log-inv is used by prepost-restore-log,
gjournal-abs/valid-group-nodes-base is used by prepost-remove-nonend-blocks,
gjournal-abs/valid-group-nodes-last-end is used by prepost-remove-nonend-blocks,
gjournal-abs/valid-group-nodes-ls is used by refine-remove,
gjournal-abs/valid-group-nodes-rec is used by prepost-remove-nonend-blocks,

Used from specification list-del

list-del/laddress-list/firstN-empty is used by prepost-remove-nonend-blocks,
list-del/address-list-set/get-numrec is used by refine-add5, refine-add4, refine-add3, refine-add2,
list-del/address-list-set/get-zero is used by refine-add5, refine-add4, refine-add3, refine-add2, refine-add1,
list-del/address-list-set/get-zero-01 is used by refine-add5, refine-add4, refine-add3, refine-add2,

Used from specification groupnode

groupnode/elim is used by prepost-remove-nonend-blocks, refine-get, refine-store, refine-lookup,
groupnode/inj is used by refine-store,
groupnode/sel is used by refine-get, refine-store, refine-lookup,
groupnode/sel-05 is used by prepost-remove-nonend-blocks,

Used from specification index-asm

index-asm/inv-set-gblock-refsize is used by refine-remove,

Used from specification debug

debug/debug is used by recovery, refine-gc, initialization,

Used from specification gjournal-asm

gjournal-asm/inv-addn is used by refine-add5, refine-add4, refine-add3, refine-add2, refine-add1,
gjournal-asm/inv-gc is used by refine-gc,
gjournal-asm/inv-gc-copy is used by refine-gc,
gjournal-asm/inv-store is used by refine-store,
gjournal-asm/inv-truncate is used by refine-truncate,
gjournal-asm/prepost-gc-referenced-nodes is used by refine-gc,

Used from specification oset

oset/nat-set/Greater is used by refine-newino,