[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-index/Data-in is used by ri-closed-gc, replayone-keep-adr, replay-safe-gc-copy, replay-log-gc-copy, replay-cons-strong-append,
store+set/node-index/Diff-ext is used by replay-orphans-trunc, replay-nonorphans-trunc,
store+set/node-index/Diff-get is used by replayone-keep-adr, replay-orphans-trunc, replay-nonorphans-trunc,
store+set/node-index/Data-in-del is used by replayone-keep-adr,
store+set/node-index/Data-notin-other is used by replayone-keep-adr,
store+set/node-index/Diff-ext is used by replayone-keep-adr, replay-orphans-trunc, replay-nonorphans-trunc, repalyone-monotonic,
store+set/node-store/Diff-ext is used by replay-safe-gc-drop,
store+set/node-store/Diff-get is used by replay-safe-gc-drop, replay-log-gc-drop,
store+set/node-index/Diff-get is used by replay-nonorphans-trunc,
store+set/node-index/Diff-mems-get is used by replayone-keep-adr, replay-orphans-trunc, replay-nonorphans-trunc,
store+set/node-index/Dom is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy, repalyone-monotonic,
store+set/node-index/In-data-in is used by replayone-keep-adr,
store+set/node-index/dom-add-in is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,
store+set/node-index/dom-ins is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,

Used from specification nat-basic

nat-basic/a is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,
nat-basic/c is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,
nat-basic/eq-01 is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,
nat-basic/succ is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,
nat-basic/z-01 is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,

Used from specification list+set

list+set/key-list-set/toSet-app is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,
list+set/address-list-set/toSet-app is used by replay-safe-gc-drop, replay-safe-gc-copy-old, replay-log-gc-drop, replay-log-gc-copy-old,
list+set/key-list-set/toSet-empty is used by ri-closed-gc,
list+set/address-list-set/toSet-empty is used by replay-safe-gc-drop, replay-safe-gc-copy-old, replay-log-gc-drop, replay-log-gc-copy-old,
list+set/address-list-set/toSet-ext is used by replay-safe-gc-copy-old, replay-log-gc-copy-old,
list+set/key-list-set/toSet-one is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,
list+set/address-list-set/toSet-one is used by replay-safe-gc-drop, replay-safe-gc-copy-old, replay-log-gc-drop, replay-log-gc-copy-old,

Used from specification node

node/elim-02 is used by replay-one-update,
node/elim-03 is used by replay-one-update,
node/elim-05 is used by replay-one-update,
node/sel-01 is used by key-cons-dentry,
node/sel-15 is used by replay-one-update,
node/test-02 is used by replay-one-update, key-cons-dentry,
node/test-06 is used by replay-one-update,
node/test-22 is used by replay-one-update,

Used from specification aubifs-inv

aubifs-inv/key-cons is used by replay-one-update, key-cons-dentry,
aubifs-inv/ri-closed is used by replay-one-update,
aubifs-inv/ri-cons is used by replay-safe-gc-copy, replay-one-update,
aubifs-inv/datanode-closed is used by replay-one-update,
aubifs-inv/dentrynode-closed is used by replay-one-update,
aubifs-inv/inodekey-cons is used by replay-one-update,
aubifs-inv/inodes-nodata is used by replay-one-update,
aubifs-inv/inodes-nodentry is used by replay-one-update,
aubifs-inv/key-node-cons is used by replay-safe-gc-copy,
aubifs-inv/log-adr-in is used by replay-cons-strong-append,
aubifs-inv/ri-closed-gc-one is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,
aubifs-inv/ri-cons-gc-one is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,
aubifs-inv/ri-cons-in is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy, replay-cons-strong-append, orphans-cons-gc-one,
aubifs-inv/ri-cons-key is used by replay-safe-gc-copy,

Used from specification key

key/disj-01 is used by replay-orphans-inode, replay-cons-add-page, replay-cons-add-orphan,
key/disj-03 is used by replay-orphans-dentry,
key/disjpred-03 is used by key-cons-dentry,
key/disjpred-04 is used by key-cons-dentry,
key/elim-02 is used by replay-orphans-trunc, replay-orphans-inode, replay-orphans-dentry, replay-orphans-del, replay-orphans-data, replay-nonorphans-trunc, replay-drop-data, replay-cons-add-page, replay-cons-add-orphan,
key/inj-02 is used by replay-drop-data,
key/inj-03 is used by replay-cons-add-orphan,
key/inodekey-id is used by replay-orphans-trunc,
key/sel-02 is used by replay-one-update,
key/sel-03 is used by replay-orphans-trunc, replay-orphans-data, replay-one-update, replay-nonorphans-trunc, replay-drop-data, replay-cons-add-orphan,
key/sel-04 is used by replay-one-update,
key/sel-05 is used by replay-orphans-trunc, replay-nonorphans-trunc,
key/test-01 is used by replay-one-update,
key/test-02 is used by replay-one-update,
key/test-03 is used by replay-one-update,
key/test-04 is used by replay-one-update,
key/test-05 is used by replay-one-update,
key/test-06 is used by replay-one-update,
key/test-07 is used by replay-orphans-dentry, replay-one-update,
key/test-08 is used by replay-orphans-inode, replay-one-update,
key/test-09 is used by replay-orphans-trunc, replay-orphans-inode, replay-orphans-dentry, replay-orphans-del, replay-orphans-data, replay-one-update, replay-nonorphans-trunc, replay-drop-data, replay-cons-add-page, replay-cons-add-orphan,

Used from specification aubifs-base

aubifs-base/at-del-ro-data is used by replay-cons-add-orphan,
aubifs-base/at-dels-ro-data is used by replay-orphans-trunc, replay-orphans-inode, replay-orphans-dentry, replay-orphans-del, replay-orphans-data, replay-nonorphans-trunc, replay-cons-add-page, replay-cons-add-orphan,
aubifs-base/at-dels-ro-nodata is used by replay-orphans-trunc, replay-orphans-inode, replay-orphans-dentry, replay-orphans-del, replay-orphans-data, replay-nonorphans-trunc, replay-drop-data, replay-cons-add-page, replay-cons-add-orphan,
aubifs-base/at-write-other is used by replay-safe-gc-copy,
aubifs-base/in-del-ro is used by replay-cons-add-orphan,
aubifs-base/in-dels-ro is used by replay-orphans-trunc, replay-orphans-inode, replay-orphans-dentry, replay-orphans-del, replay-orphans-data, replay-nonorphans-trunc, replay-drop-data, replay-cons-add-page, replay-cons-add-orphan,
aubifs-base/notin-dels is used by replay-safe-gc-copy, replay-cons-strong-append,
aubifs-base/read-write-other-fs is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,
aubifs-base/write-shift is used by replay-safe-gc-copy, replay-log-gc-copy,
aubifs-base/at-del-ro-nodata is used by replay-cons-add-orphan,
aubifs-base/at-dels-ro-data is used by replay-orphans-trunc, replay-orphans-inode, replay-orphans-dentry, replay-orphans-del, replay-orphans-data, replay-nonorphans-trunc, replay-drop-data,
aubifs-base/at-dels-ro-nodata is used by replay-orphans-trunc, replay-nonorphans-trunc, replay-drop-data,
aubifs-base/at-write-other is used by replay-safe-gc-copy-old, replay-log-gc-copy-old,
aubifs-base/datakeys is used by replayone-keep-adr, replay-orphans-trunc, replay-nonorphans-trunc, repalyone-monotonic,
aubifs-base/datakeys-ge is used by replayone-keep-adr, replay-orphans-trunc, replay-nonorphans-trunc, repalyone-monotonic,
aubifs-base/del-del-again is used by replay-one-update,
aubifs-base/del-put-again is used by replay-one-update,
aubifs-base/in-del-ro is used by replay-cons-add-orphan, repalyone-monotonic,
aubifs-base/in-dels-inode is used by replay-one-update,
aubifs-base/in-dels-ro is used by replay-orphans-trunc, replay-orphans-inode, replay-orphans-dentry, replay-orphans-del, replay-orphans-data, replay-nonorphans-trunc, replay-cons-add-page, replay-cons-add-orphan,
aubifs-base/in-read-in-dom is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,
aubifs-base/in-write is used by replay-safe-gc-copy-old, replay-safe-gc-copy,
aubifs-base/index-lookup-base is used by ri-closed-gc,
aubifs-base/index-lookup-length is used by replay-safe-gc-copy, replay-log-gc-copy,
aubifs-base/index-lookup-rec is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,
aubifs-base/index-update-key-base is used by ri-closed-gc, replay-log-gc-copy,
aubifs-base/index-update-key-rec is used by ri-closed-gc, replay-log-gc-copy,
aubifs-base/new-base is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,
aubifs-base/new-rec is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,
aubifs-base/new-write is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,
aubifs-base/notin-del is used by replayone-keep-adr,
aubifs-base/read-base is used by ri-closed-gc,
aubifs-base/read-length is used by replay-safe-gc-copy, replay-log-gc-copy,
aubifs-base/read-rec is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,
aubifs-base/read-write-other is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,
aubifs-base/write-base is used by ri-closed-gc,
aubifs-base/write-rec is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,

Used from specification store

store/node-index/At-other is used by replay-orphans-inode, replay-orphans-dentry,
store/node-index/In-insert is used by replay-drop-data,
store/node-index/k-Extension is used by replay-orphans-trunc, replay-orphans-inode, replay-orphans-dentry, replay-orphans-del, replay-orphans-data, replay-nonorphans-trunc, replay-drop-data, replay-cons-add-page, replay-cons-add-orphan,
store/node-index/notin-del-notin is used by replay-one-update,
store/node-store/At-other is used by replay-safe-write, replay-log-write, orphans-cons-gc-one,
store/node-index/At-other is used by replay-orphans-inode, replay-orphans-dentry, replay-orphans-data, replay-drop-data, orphans-cons-gc-one,
store/node-index/At-same is used by replay-orphans-inode, replay-orphans-dentry, replay-orphans-data, replay-drop-data, orphans-cons-gc-one,
store/node-store/At-same is used by replay-safe-gc-copy, replay-log-gc-copy, replay-cons-strong-append,
store/node-store/Del-at is used by replay-safe-drop,
store/node-index/Del-at is used by replay-orphans-del, replay-cons-add-page,
store/node-store/Del-at-strong is used by replay-log-drop,
store/node-store/Del-in is used by replay-safe-drop,
store/node-index/Del-in is used by replay-orphans-del, replay-cons-add-page, repalyone-monotonic,
store/node-index/In-insert is used by replay-orphans-inode, replay-orphans-dentry, replay-drop-data, repalyone-monotonic,
store/node-index/in-neq is used by replay-orphans-inode, replay-orphans-dentry, replay-orphans-data, replay-drop-data, repalyone-monotonic, orphans-cons-gc-one,
store/node-index/insin is used by replay-orphans-inode, replay-orphans-dentry, replay-orphans-data, replay-drop-data, orphans-cons-gc-one,
store/node-store/k-At-same is used by orphans-cons-gc-one,

Used from specification set-union

set-union/node-index/subdef is used by repalyone-monotonic,
set-union/node-store/int-a is used by replay-safe-gc-drop, replay-safe-gc-copy-old, replay-log-gc-drop, replay-log-gc-copy-old,
set-union/node-store/int-c is used by replay-safe-gc-drop, replay-safe-gc-copy-old, replay-log-gc-drop, replay-log-gc-copy-old,
set-union/node-store/int-e is used by replay-safe-gc-drop, replay-safe-gc-copy-old, replay-log-gc-drop, replay-log-gc-copy-old,
set-union/node-store/int-ins is used by replay-safe-gc-drop, replay-safe-gc-copy-old, replay-log-gc-drop, replay-log-gc-copy-old,
set-union/node-index/una is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,
set-union/node-store/una is used by replay-safe-gc-drop, replay-safe-gc-copy-old, replay-log-gc-drop, replay-log-gc-copy-old,
set-union/node-store/unadd is used by replay-safe-gc-drop, replay-safe-gc-copy-old, replay-log-gc-drop, replay-log-gc-copy-old,
set-union/node-index/unadd is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,
set-union/node-index/unc is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,
set-union/node-store/unc is used by replay-safe-gc-drop, replay-safe-gc-copy-old, replay-log-gc-drop, replay-log-gc-copy-old,
set-union/node-store/une is used by replay-safe-gc-drop, replay-safe-gc-copy-old, replay-log-gc-drop, replay-log-gc-copy-old,
set-union/node-index/une is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,

Used from specification set-basic

set-basic/node-index/In-insert is used by replay-cons-add-page, replay-cons-add-orphan,
set-basic/node-index/in-02 is used by replay-cons-add-page, replay-cons-add-orphan,
set-basic/node-index/in-03 is used by replay-cons-add-page, replay-cons-add-orphan,
set-basic/node-index/ne-01 is used by replay-orphans-trunc, replay-one-update, replay-drop-data,
set-basic/node-index/size-zero-01 is used by replay-orphans-trunc, replay-one-update, replay-drop-data,
set-basic/node-index/sub-add-03 is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,
set-basic/node-index/sub-e is used by ri-closed-gc,

Used from specification list-data

list-data/address-list-set/l is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,
list-data/key-list-set/l is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,
list-data/address-list-set/size-01 is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,
list-data/key-list-set/size-01 is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,

Used from specification list

list/address-list-set/Nil is used by replay-safe-split, replay-log-split,
list/address-list-set/a is used by ri-closed-gc, replaylog-keep-adr, replay-split, replay-safe-write, replay-safe-split, replay-safe-rec-variant1, replay-safe-one, replay-safe-gc-drop, replay-safe-gc-copy-old, replay-safe-gc-copy, replay-safe-drop, replay-log-write, replay-log-split, replay-log-one, replay-log-gc-drop, replay-log-gc-copy-old, replay-log-gc-copy, replay-log-drop, replay-cons-strong-append,
list/node-list/a is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,
list/key-list-set/a is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,
list/address-list-set/app is used by replay-safe-one, replay-log-one,
list/key-list-set/c is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,
list/address-list-set/c is used by ri-closed-gc, replaylog-keep-adr, replay-safe-write, replay-safe-split, replay-safe-gc-drop, replay-safe-gc-copy-old, replay-safe-gc-copy, replay-safe-drop, replay-log-write, replay-log-split, replay-log-gc-drop, replay-log-gc-copy-old, replay-log-gc-copy, replay-log-drop,
list/node-list/c is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,
list/address-list-set/in-06 is used by replaylog-keep-adr, replay-safe-write, replay-safe-drop, replay-log-write, replay-log-drop,
list/address-list-set/in-empty is used by replaylog-keep-adr,
list/address-list-set/in-rec is used by replay-safe-gc-copy,
list/address-list-set/len-05 is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,
list/key-list-set/len-05 is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,

Used from specification node-store

node-store/in-insert is used by replay-safe-write, replay-cons-strong-append,

Used from specification list-dup

list-dup/address-list-set/dups-cons is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,
list-dup/key-list-set/dups-cons is used by ri-closed-gc, replay-safe-gc-copy, replay-log-gc-copy,
list-dup/key-list-set/e-01 is used by ri-closed-gc,
list-dup/address-list-set/e-01 is used by ri-closed-gc, replay-log-gc-copy,