[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-empty is used by initialization,
store+set/group-store-ablock-store-nat-store/Dom is used by refine-get-gc-block,
store+set/group-store-ablock-store-nat-store/dom-add-in is used by refine-add-gnds,
store+set/group-store-ablock-store-nat-store/dom-emp is used by initialization,
store+set/group-store-ablock-store-nat-store/dom-ins is used by refine-allocate-gnd, refine-add-gnds,
store+set/group-store-ablock-store-nat-store/dom-isemp is used by initialization,

Used from specification nat-basic

nat-basic/f is used by refine-add-gnds,

Used from specification ablock

ablock/group-store/elim is used by refine-get-gblock-refsize, refine-read-gblock,
ablock/group-store/sel-01 is used by refine-read-gblock,
ablock/group-store/sel-02 is used by refine-read-gblock,
ablock/group-store/sel-03 is used by refine-get-gblock-refsize,
ablock/group-store/updsel-26 is used by refine-add-gnds,

Used from specification btree-inv

btree-inv/btree-inv-crash is used by recovery,

Used from specification ablock-store-inv

ablock-store-inv/group-store/inv-reduce is used by refine-add-gnds,
ablock-store-inv/group-store/inv-store-empty is used by initialization,
ablock-store-inv/group-store/remove-refsize0-empty is used by initialization,
ablock-store-inv/group-store/to-adrs-eq is used by refine-read-gblock,

Used from specification store

store/group-store-ablock-store-nat-store/At-same is used by refine-add-gnds,
store/group-store-ablock-store-nat-store/In-insert is used by refine-allocate-gnd,
store/group-store-ablock-store-nat-store/insins is used by refine-add-gnds,

Used from specification apersistence-base

apersistence-base/dom-gstore-crash is used by recovery,
apersistence-base/elems-append is used by refine-allocate-gnd,
apersistence-base/elems-empty is used by initialization,
apersistence-base/elems-in-notin-ginval is used by refine-add-gnds,
apersistence-base/fwd-in-gstore-loghead is used by refine-get-block-free-size,
apersistence-base/fwd-in-gstore0 is used by refine-deallocate-gnd, refine-get-gc-block,
apersistence-base/fwd-in-log-in-gstore is used by refine-add-gnds,
apersistence-base/fwd-inv-gblock-rem is used by refine-add-gnds, refine-read-gblock,
apersistence-base/fwd-inv-loghead is used by refine-get-block-free-size,
apersistence-base/icrash-inv is used by recovery,
apersistence-base/icrash-remove-refsize0-prefix is used by recovery,
apersistence-base/inv-index is used by refine-get-leb-size, refine-is-log-empty, refine-get-block-free-size, refine-sync, recovery, initialization, refine-requires-commit, refine-deallocate-gnd, refine-allocate-gnd, refine-get-gblock-refsize, refine-set-gblock-refsize, refine-get-gc-block, refine-read-gblock, refine-read-gnd,
apersistence-base/inv-journal is used by refine-get-leb-size, refine-is-log-empty, refine-get-block-free-size, refine-sync, recovery, initialization, refine-requires-commit, refine-deallocate-gnd, refine-allocate-gnd, refine-get-gblock-refsize, refine-set-gblock-refsize, refine-get-gc-block, refine-read-gblock, refine-read-gnd,
apersistence-base/inv-state is used by refine-get-leb-size, refine-is-log-empty, refine-get-block-free-size, refine-sync, recovery, initialization, refine-requires-commit, refine-deallocate-gnd, refine-allocate-gnd, refine-get-gblock-refsize, refine-set-gblock-refsize, refine-get-gc-block, refine-read-gblock, refine-read-gnd,

Used from specification set-union

set-union/nat-set/del-e-01 is used by refine-allocate-gnd,
set-union/nat-set/int-a is used by refine-get-block-free-size, initialization, refine-allocate-gnd, refine-add-gnds,
set-union/nat-set/int-c is used by refine-get-block-free-size, initialization, refine-allocate-gnd, refine-add-gnds,
set-union/nat-set/int-e is used by initialization,
set-union/nat-set/intersect-add-rem is used by refine-allocate-gnd,
set-union/nat-set/rem-union-ins is used by refine-allocate-gnd,
set-union/nat-set/una is used by refine-get-block-free-size, recovery, initialization, refine-deallocate-gnd, refine-allocate-gnd, refine-add-gnds, refine-get-gc-block,
set-union/nat-set/unadd is used by refine-allocate-gnd,
set-union/nat-set/unc is used by refine-get-block-free-size, recovery, initialization, refine-deallocate-gnd, refine-allocate-gnd, refine-add-gnds, refine-get-gc-block,
set-union/nat-set/une is used by initialization,
set-union/nat-set/uneq is used by recovery,
set-union/nat-set/unsub is used by recovery,

Used from specification nat

nat/anti is used by refine-add-gnds,
nat/lels-02 is used by refine-add-gnds,
nat/lels-03 is used by refine-add-gnds,
nat/ler is used by refine-add-gnds,
nat/let is used by refine-add-gnds,
nat/lez is used by refine-get-block-free-size,

Used from specification error-class

error-class/ecommit is used by refine-sync, refine-deallocate-gnd, refine-read-gblock, refine-read-gnd,
error-class/erofs is used by refine-sync, refine-allocate-gnd,
error-class/esuccess is used by refine-sync, recovery, initialization, refine-deallocate-gnd, refine-allocate-gnd, refine-add-gnds, refine-read-gblock, refine-read-gnd,
error-class/not-esuccess is used by refine-sync, recovery, initialization, refine-deallocate-gnd, refine-allocate-gnd, refine-add-gnds, refine-read-gblock, refine-read-gnd,

Used from specification error

error/disj-120 is used by refine-sync, refine-allocate-gnd,
error/disj-35 is used by refine-get-gc-block,
error/disj-91 is used by refine-sync, refine-deallocate-gnd, refine-read-gblock, refine-read-gnd,

Used from specification list-last

list-last/nat-list-set/last-def is used by refine-allocate-gnd,

Used from specification persistence-state

persistence-state/disj-02 is used by refine-get-block-free-size,
persistence-state/disj-03 is used by refine-sync,
persistence-state/elim-01 is used by refine-get-block-free-size,
persistence-state/sel-01 is used by refine-allocate-gnd,
persistence-state/test-02 is used by refine-sync, refine-allocate-gnd,
persistence-state/test-03 is used by refine-get-block-free-size, refine-allocate-gnd,
persistence-state/test-04 is used by refine-sync, refine-allocate-gnd,
persistence-state/test-09 is used by refine-get-block-free-size, refine-allocate-gnd,
persistence-state/test-10 is used by refine-get-block-free-size, refine-sync, recovery,
persistence-state/test-11 is used by refine-get-block-free-size, refine-sync, recovery,

Used from specification list

list/nat-list-set/Last is used by refine-allocate-gnd,
list/nat-list-set/a is used by refine-allocate-gnd,
list/address-list-set/a is used by refine-read-gblock,
list/laddress-list/a is used by refine-add-gnds,
list/group-store/a is used by refine-read-gblock,
list/address-list-set/app-01 is used by refine-read-gblock,
list/group-store/app-01 is used by refine-read-gblock,
list/nat-list-set/e-02 is used by refine-allocate-gnd,

Used from specification list-dup

list-dup/laddress-list/a is used by refine-add-gnds,
list-dup/nat-list-set/e-01 is used by initialization,
list-dup/nat-list-set/f is used by refine-allocate-gnd,

Used from specification address-data

address-data/elim is used by refine-read-gnd,
address-data/sel-03 is used by refine-read-gnd,

Used from specification oelem

oelem/nat-set/irreflexivity is used by refine-add-gnds,

Used from specification Unknown

Unknown/Unknown is used by recovery,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,
Unknown/Unknown is used by refine-add-gnds,

Used from specification btree-asm

btree-asm/inv-format is used by initialization,

Used from specification apersistence-asm

apersistence-asm/inv-allocate-gnd is used by refine-allocate-gnd,