[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-ext is used by inv-gc,
store+set/node-store/Diff-base is used by crash-neutral-gc,
store+set/node-store/Diff-get is used by inv-gc,
store+set/node-index/Dom is used by crash-neutral-newino, inv-newino,

Used from specification list+set

list+set/address-list-set/toSet-app is used by inv-gc,
list+set/address-list-set/toSet-empty is used by crash-neutral-gc, inv-gc,
list+set/key-list-set/toSet-empty is used by crash-neutral-gc, inv-gc,
list+set/address-list-set/toSet-ext is used by inv-gc,

Used from specification aubifs-inv

aubifs-inv/log-cons-drop is used by inv-gc,
aubifs-inv/log-cons-variant1-01 is used by inv-add2, inv-add3, inv-add4,
aubifs-inv/ri-cons-drop is used by inv-gc,
aubifs-inv/ri-cons-variant1-01 is used by inv-add2, inv-add3, inv-add4,
aubifs-inv/empty-inodes is used by inv-format,
aubifs-inv/inodes-del is used by inv-orphans-remove,
aubifs-inv/inodes-put is used by inv-orphans-insert,
aubifs-inv/log-adr-in is used by inv-add1, inv-gc,
aubifs-inv/log-cons-app is used by inv-add5, inv-add1, inv-add2, inv-add3, inv-add4, inv-gc,
aubifs-inv/log-cons-copy-new is used by inv-gc,
aubifs-inv/log-cons-emp is used by inv-commit, inv-format,
aubifs-inv/log-cons-one is used by inv-add5, inv-add1, inv-add2, inv-add3, inv-add4,
aubifs-inv/log-cons-variant1-01 is used by inv-add5, inv-add1, inv-gc,
aubifs-inv/log-node-cons is used by inv-add5, inv-add1, inv-add2, inv-add3, inv-add4, inv-gc,
aubifs-inv/ri-cons-copy-new is used by inv-gc,
aubifs-inv/ri-cons-in is used by inv-lookup, inv-add1,
aubifs-inv/ri-cons-inj is used by inv-gc, inv-check-commit, inv-commit,
aubifs-inv/ri-cons-variant1-01 is used by inv-add5, crash-neutral-lookup, crash-neutral-gc, crash-neutral-check-commit, crash-neutral-commit, inv-lookup, inv-add1, inv-gc, inv-check-commit, inv-commit,
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,
aubifs-inv/ri-key-cons is used by inv-add5, inv-add1, inv-add2, inv-add3, inv-add4,

Used from specification key

key/inj-03 is used by crash-neutral-newino, inv-newino,

Used from specification aubifs-base

aubifs-base/at-write-other is used by inv-gc,
aubifs-base/new-inode-exists is used by crash-neutral-newino, inv-newino,
aubifs-base/in-write is used by inv-gc,
aubifs-base/index-lookup-base is used by crash-neutral-gc,
aubifs-base/index-lookup-length is used by inv-gc,
aubifs-base/index-update-key-base is used by crash-neutral-gc,
aubifs-base/new-base is used by crash-neutral-gc, inv-gc,
aubifs-base/new-in-fs is used by inv-gc,
aubifs-base/new-one is used by inv-add5, crash-neutral-add5, crash-neutral-add1, crash-neutral-add2, crash-neutral-add3, crash-neutral-add4, inv-add1, inv-add2, inv-add3, inv-add4,
aubifs-base/new-rec is used by inv-add5, crash-neutral-add5, crash-neutral-add2, crash-neutral-add3, crash-neutral-add4, inv-add2, inv-add3, inv-add4,
aubifs-base/read-base is used by crash-neutral-gc,
aubifs-base/read-length is used by inv-gc,
aubifs-base/write-base is used by crash-neutral-gc,

Used from specification set-union

set-union/node-store/Intersect is used by inv-gc,
set-union/node-index/One is used by crash-neutral-newino, inv-newino,
set-union/node-store/int-a is used by crash-neutral-gc, inv-gc, inv-commit,
set-union/node-store/int-c is used by crash-neutral-gc, inv-gc, inv-commit,
set-union/node-store/int-e is used by crash-neutral-gc, inv-gc, inv-commit,
set-union/node-store/intu-empty is used by inv-gc,
set-union/node-store/una is used by inv-gc,
set-union/node-index/una is used by crash-neutral-newino, inv-newino,
set-union/node-index/unadd is used by crash-neutral-newino, inv-newino,
set-union/node-store/unc is used by inv-gc,
set-union/node-index/unc is used by crash-neutral-newino, inv-newino,
set-union/node-index/une is used by crash-neutral-newino, inv-newino,
set-union/node-index/unin-01 is used by crash-neutral-newino, inv-newino,

Used from specification store

store/node-store/At-other is used by inv-add5, inv-add2, inv-add3, inv-add4,
store/node-store/At-in-out is used by inv-add5, inv-add1, inv-add2, inv-add3, inv-add4,
store/node-store/At-same is used by inv-add5, inv-add1, inv-add2, inv-add3, inv-add4,
store/node-store/in-neq is used by inv-add5, inv-add2, inv-add3, inv-add4,

Used from specification error-class

error-class/ecommit is used by inv-add5, inv-recover, inv-contains, inv-lookup, inv-entries, inv-get, inv-add1, inv-add2, inv-add3, inv-add4, inv-commit, inv-sync, inv-format,
error-class/eio is used by crash-neutral-add5, crash-neutral-contains, crash-neutral-lookup, crash-neutral-entries, crash-neutral-add1, crash-neutral-add2, crash-neutral-add3, crash-neutral-add4, crash-neutral-commit,
error-class/esuccess is used by inv-recover, crash-neutral-recover, inv-lookup, crash-neutral-sync, inv-format,

Used from specification error

error/disj-66 is used by crash-neutral-contains, crash-neutral-lookup, crash-neutral-entries,
error/disj-91 is used by inv-recover, inv-contains, inv-lookup, inv-entries, inv-sync, inv-format,

Used from specification set-basic

set-basic/node-store/Extension is used by inv-gc,
set-basic/node-store/In-empty is used by inv-gc,
set-basic/node-index/add is used by crash-neutral-newino, inv-newino,
set-basic/node-store/ne-01 is used by inv-gc,
set-basic/node-store/size-zero-01 is used by inv-gc,
set-basic/node-index/sub-e is used by crash-neutral-gc, inv-gc,

Used from specification list-data

list-data/address-list-set/size-01 is used by crash-neutral-gc, inv-gc,
list-data/key-list-set/size-01 is used by crash-neutral-gc, inv-gc,

Used from specification list

list/address-list-set/Last is used by inv-add5, crash-neutral-add5, crash-neutral-add1, crash-neutral-add2, crash-neutral-add3, crash-neutral-add4, inv-add1, inv-add2, inv-add3, inv-add4,
list/address-list-set/a is used by inv-add5, crash-neutral-add5, crash-neutral-add2, crash-neutral-add3, crash-neutral-add4, crash-neutral-gc, inv-add1, inv-add2, inv-add3, inv-add4, inv-gc,
list/address-list-set/app is used by crash-neutral-gc,
list/address-list-set/in-17 is used by inv-add5, crash-neutral-add5, crash-neutral-add3, crash-neutral-add4, inv-add3, inv-add4,
list/address-list-set/in-rec is used by inv-add5, crash-neutral-add5, crash-neutral-add3, crash-neutral-add4, inv-add3, inv-add4,

Used from specification node-store

node-store/in-insert is used by inv-add5, inv-add1, inv-add2, inv-add3, inv-add4,

Used from specification list-dup

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