[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, inv-allocate-gnd,
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-add-in is used by inv-add-gnds, inv-set-gblock-refsize,
store+set/group-store-ablock-store-nat-store/dom-del is used by inv-deallocate-gnd,
store+set/group-store-ablock-store-nat-store/dom-emp is used by inv-format, inv-allocate-gnd,
store+set/group-store-ablock-store-nat-store/dom-ins is used by inv-add-gnds, inv-allocate-gnd, inv-set-gblock-refsize,

Used from specification ablock

ablock/group-store/elim is used by inv-add-gnds, crash-neutral-add-gnds,
ablock/group-store/sel-01 is used by inv-add-gnds,
ablock/group-store/sel-02 is used by inv-add-gnds, crash-neutral-add-gnds,
ablock/group-store/upd-01 is used by inv-add-gnds, crash-neutral-add-gnds,
ablock/group-store/upd-02 is used by inv-add-gnds, crash-neutral-add-gnds,
ablock/group-store/upd-03 is used by crash-neutral-set-gblock-refsize,
ablock/group-store/updsel-28 is used by inv-add-gnds, crash-neutral-add-gnds,

Used from specification nat-basic

nat-basic/a is used by inv-add-gnds, inv-allocate-gnd,
nat-basic/c is used by inv-add-gnds, inv-allocate-gnd,
nat-basic/eq-01 is used by inv-add-gnds,
nat-basic/f is used by inv-add-gnds,
nat-basic/s-04 is used by inv-allocate-gnd,

Used from specification aubifs-inv

aubifs-inv/ri-inj-del is used by inv-remove,
aubifs-inv/ri-inj-empty is used by inv-format,
aubifs-inv/ri-inj-rem is used by inv-truncate,
aubifs-inv/ri-inj-write is used by inv-store,

Used from specification ablock-store-inv

ablock-store-inv/group-store/inv-block is used by inv-add-gnds,
ablock-store-inv/group-store/adrs-empty is used by crash-neutral-add-gnds,
ablock-store-inv/group-store/inv-alloc is used by inv-allocate-gnd,
ablock-store-inv/group-store/inv-block-empty is used by inv-allocate-gnd,
ablock-store-inv/group-store/inv-diff-n is used by inv-set-gblock-refsize,
ablock-store-inv/group-store/inv-eq-list-size is used by inv-add-gnds,
ablock-store-inv/group-store/inv-flashsize-app is used by inv-add-gnds,
ablock-store-inv/group-store/inv-flashsize-empty is used by inv-add-gnds, crash-neutral-add-gnds,
ablock-store-inv/group-store/inv-nodups is used by inv-add-gnds, crash-neutral-add-gnds,
ablock-store-inv/group-store/inv-reduce is used by inv-add-gnds, inv-set-gblock-refsize,
ablock-store-inv/group-store/inv-reduce-rem is used by inv-deallocate-gnd,
ablock-store-inv/group-store/inv-remove-refsize0-diff is used by inv-commit,
ablock-store-inv/group-store/inv-set-refsize is used by inv-set-gblock-refsize,
ablock-store-inv/group-store/inv-store-empty is used by inv-format, inv-allocate-gnd,
ablock-store-inv/group-store/remove-refsize0-empty is used by inv-format,
ablock-store-inv/group-store/remove-refsize0-idem is used by inv-commit,

Used from specification store

store/group-store-ablock-store-nat-store/At-same is used by inv-add-gnds, crash-neutral-add-gnds,
store/group-store-ablock-store-nat-store/In-empty is used by inv-allocate-gnd,
store/group-store-ablock-store-nat-store/ins is used by crash-neutral-add-gnds,
store/group-store-ablock-store-nat-store/insin is used by inv-add-gnds, crash-neutral-add-gnds,
store/group-store-ablock-store-nat-store/insins is used by inv-add-gnds, crash-neutral-add-gnds,

Used from specification apersistence-base

apersistence-base/crash-gstore-inv is used by inv-recovery,
apersistence-base/crash-update-reverted is used by crash-neutral-set-gblock-refsize,
apersistence-base/dom-gstore-crash is used by inv-recovery,
apersistence-base/elems-append is used by inv-allocate-gnd,
apersistence-base/elems-def is used by inv-deallocate-gnd,
apersistence-base/elems-empty is used by inv-format, inv-commit,
apersistence-base/elems-in-notin-ginval is used by inv-allocate-gnd,
apersistence-base/fwd-in-gstore-loghead is used by inv-add-gnds, crash-neutral-add-gnds,
apersistence-base/fwd-in-gstore0 is used by crash-neutral-deallocate-gnd, inv-deallocate-gnd,
apersistence-base/fwd-in-log-in-gstore is used by inv-allocate-gnd,
apersistence-base/fwd-inv-gblock-rem is used by inv-add-gnds,
apersistence-base/fwd-inv-loghead is used by inv-add-gnds, crash-neutral-add-gnds,
apersistence-base/inv-journal is used by inv-get-leb-size, crash-neutral-get-leb-size, crash-neutral-recovery, inv-is-log-empty, crash-neutral-is-log-empty, inv-format, inv-get-block-free-size, crash-neutral-get-block-free-size, inv-sync, crash-neutral-sync, inv-add-gnds, crash-neutral-add-gnds, crash-neutral-contains, crash-neutral-lookup, crash-neutral-store, crash-neutral-remove, crash-neutral-truncate, crash-neutral-entries, crash-neutral-read-gnd, crash-neutral-read-gblock, crash-neutral-get-gc-block, crash-neutral-set-gblock-refsize, crash-neutral-get-gblock-refsize, crash-neutral-allocate-gnd, crash-neutral-deallocate-gnd, crash-neutral-commit, crash-neutral-requires-commit, inv-recovery, inv-requires-commit, inv-commit, inv-deallocate-gnd, inv-allocate-gnd, inv-get-gblock-refsize, inv-set-gblock-refsize, inv-get-gc-block, inv-read-gblock, inv-read-gnd, inv-entries, inv-truncate, inv-remove, inv-store, inv-lookup, inv-contains,

Used from specification set-union

set-union/nat-set/del-e-01 is used by inv-allocate-gnd,
set-union/nat-set/int-a is used by inv-format, inv-add-gnds, crash-neutral-add-gnds, inv-commit, inv-deallocate-gnd, inv-allocate-gnd,
set-union/nat-set/int-c is used by inv-format, inv-add-gnds, crash-neutral-add-gnds, inv-commit, inv-deallocate-gnd, inv-allocate-gnd,
set-union/nat-set/int-e is used by inv-format, inv-commit,
set-union/nat-set/int-ins is used by inv-deallocate-gnd,
set-union/nat-set/intersect-add-rem is used by inv-allocate-gnd,
set-union/nat-set/rem-union-ins is used by inv-deallocate-gnd, inv-allocate-gnd,
set-union/nat-set/una is used by inv-format, inv-add-gnds, crash-neutral-add-gnds, crash-neutral-deallocate-gnd, inv-recovery, inv-commit, inv-deallocate-gnd, inv-allocate-gnd,
set-union/nat-set/unadd is used by inv-deallocate-gnd, inv-allocate-gnd,
set-union/nat-set/unc is used by inv-format, inv-add-gnds, crash-neutral-add-gnds, crash-neutral-deallocate-gnd, inv-recovery, inv-commit, inv-deallocate-gnd, inv-allocate-gnd,
set-union/nat-set/une is used by inv-format, inv-commit, inv-allocate-gnd,
set-union/nat-set/uneq is used by inv-recovery,
set-union/nat-set/unin-01 is used by inv-deallocate-gnd,
set-union/nat-set/unsub is used by inv-recovery,

Used from specification nat

nat/gr-def is used by inv-allocate-gnd,
nat/le-def is used by inv-get-block-free-size, inv-add-gnds,
nat/lels-02 is used by inv-add-gnds,
nat/lels-03 is used by inv-add-gnds,
nat/ler is used by inv-add-gnds,
nat/lez is used by crash-neutral-get-block-free-size, inv-add-gnds, crash-neutral-add-gnds,
nat/lez-01 is used by inv-add-gnds, crash-neutral-add-gnds,

Used from specification error-class

error-class/ecommit is used by inv-format, inv-sync, inv-recovery, inv-commit, inv-deallocate-gnd, inv-allocate-gnd, inv-read-gblock, inv-read-gnd, inv-entries, inv-lookup, inv-contains,
error-class/eio is used by crash-neutral-recovery, crash-neutral-sync, inv-add-gnds, crash-neutral-add-gnds, crash-neutral-contains, crash-neutral-lookup, crash-neutral-entries, crash-neutral-read-gnd, crash-neutral-read-gblock, crash-neutral-allocate-gnd, crash-neutral-deallocate-gnd, crash-neutral-commit,
error-class/esuccess is used by inv-format, inv-add-gnds, crash-neutral-add-gnds, inv-recovery, inv-commit, inv-deallocate-gnd, inv-allocate-gnd, inv-read-gblock,
error-class/not-esuccess is used by inv-add-gnds, inv-commit, inv-deallocate-gnd, inv-allocate-gnd,

Used from specification error

Used from specification set-basic

set-basic/nat-set/eq-03 is used by inv-deallocate-gnd,

Used from specification list-prefixn

list-prefixn/group-store/prefixn-0 is used by inv-add-gnds, crash-neutral-add-gnds,
list-prefixn/group-store/prefixn-fulln is used by inv-add-gnds,
list-prefixn/group-store/prefixn-len-n is used by inv-add-gnds,

Used from specification list-data

list-data/laddress-list/l is used by inv-add-gnds, crash-neutral-add-gnds,
list-data/group-store/l is used by inv-add-gnds, crash-neutral-add-gnds,
list-data/laddress-list/size-01 is used by inv-add-gnds, crash-neutral-add-gnds,
list-data/group-store/size-01 is used by inv-add-gnds, crash-neutral-add-gnds,

Used from specification list

list/nat-list-set/Last is used by inv-allocate-gnd,
list/nat-list-set/a is used by inv-allocate-gnd,
list/laddress-list/a is used by inv-add-gnds, crash-neutral-add-gnds,
list/group-store/a is used by inv-add-gnds, crash-neutral-add-gnds,
list/laddress-list/app is used by inv-add-gnds, crash-neutral-add-gnds,
list/group-store/app is used by crash-neutral-add-gnds,
list/group-store/len is used by inv-add-gnds,
list/laddress-list/len is used by inv-add-gnds,

Used from specification list-dup

list-dup/laddress-list/a is used by inv-add-gnds,
list-dup/nat-list-set/e-01 is used by inv-format, inv-commit,
list-dup/nat-list-set/f is used by inv-allocate-gnd,

Used from specification address-data

address-data/elim is used by crash-neutral-read-gnd, inv-read-gnd,
address-data/sel-03 is used by crash-neutral-read-gnd, inv-read-gnd,

Used from specification oelem

oelem/nat-set/irreflexivity is used by inv-get-block-free-size, inv-add-gnds, inv-allocate-gnd,

Used from specification groupnode

groupnode/elim is used by crash-neutral-store, inv-store,
groupnode/sel is used by crash-neutral-store, inv-store,

Used from specification nat-store+set

nat-store+set/group-store/dom-max-in is used by inv-allocate-gnd,