[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 alink

alink/inj is used by dups-eqsize-ls,

Used from specification store+set

store+set/node-index/Data-in is used by abs-files-unused-adrs, abs-dirs-unused-adrs,
store+set/node-index/Diff-ext is used by abs-files-evict, abs-dirs-orphans, Diff-union-comm,
store+set/node-index/Diff-get is used by abs-files-orphans, abs-dirs-orphans, abs-dirs-deldatakeys-2, Diff-union-comm,
store+set/node-index/Diff-ext is used by abs-orphans-diff-datakeys, abs-files-orphans, abs-files-evict, abs-dirs-orphans, abs-dirs-deldatakeys-2, abs-dirs-deldatakeys-1, Diff-union-comm,
store+set/node-index/Diff-get is used by abs-orphans-diff-datakeys, abs-files-orphans, abs-dirs-orphans, abs-dirs-deldatakeys-2, Diff-union-comm,
store+set/node-store/Diff-get is used by abs-files-unused-adrs, abs-dirs-unused-adrs,
store+set/node-store/Diff-mems-get is used by abs-files-unused-adrs, abs-dirs-unused-adrs,
store+set/node-index/Diff-mems-get is used by abs-files-orphans, abs-dirs-orphans, abs-dirs-deldatakeys-2, Diff-union-comm,
store+set/node-index/In-data-in is used by abs-files-trunc, abs-files-drop, abs-dirs-trunc, abs-dirs-drop,

Used from specification abstract-file

abstract-file/elim is used by afs-cons-remove-orphans,
abstract-file/inj is used by abs-files-orphans, F-inj,
abstract-file/sel-01 is used by abs-orphans,
abstract-file/sel-02 is used by abs-orphans,

Used from specification nat-basic

nat-basic/a is used by dups-eqsize-ls, dups-eqsize-entries,
nat-basic/c is used by dups-eqsize-ls, dups-eqsize-entries,
nat-basic/eq-01 is used by dups-eqsize-ls, dups-eqsize-entries,
nat-basic/oz is used by dups-eqsize-ls, dups-eqsize-entries,
nat-basic/ref is used by dups-eqsize-ls, dups-eqsize-entries,
nat-basic/s-04 is used by dups-eqsize-ls, dups-eqsize-entries,

Used from specification afs-base

afs-base/afs-cons is used by afs-cons-remove-orphans, abs-orphans,
afs-base/orphans is used by afs-cons-remove-orphans, abs-orphans-diff-datakeys, abs-orphans,
afs-base/afs-cons-dir-nlink is used by afs-cons-remove-orphans,
afs-base/afs-cons-file-nlink is used by afs-cons-remove-orphans,
afs-base/afs-cons-links-rmorphans is used by afs-cons-remove-orphans,
afs-base/afs-cons-notfile is used by afs-cons-remove-orphans,
afs-base/afs-cons-pagesize is used by afs-cons-remove-orphans,
afs-base/afs-cons-root-dir is used by afs-cons-remove-orphans,
afs-base/dir-empty is used by afs-cons-remove-orphans, abs-orphans,
afs-base/links-nonempty is used by afs-cons-remove-orphans,
afs-base/root-not-orphan is used by afs-cons-remove-orphans, abs-orphans-diff-datakeys, abs-orphans,
afs-base/subdirs-delete-orphans is used by afs-cons-remove-orphans,
afs-base/valid-ino is used by afs-cons-remove-orphans, abs-orphans-diff-datakeys, abs-orphans,
afs-base/valid-pagesize is used by afs-cons-remove-orphans, abs-orphans,

Used from specification aubifs-inv

aubifs-inv/read-lookup-copy is used by abs-files-gc-copy, abs-dirs-gc-copy,
aubifs-inv/inodes-in is used by abs-keys-orphans-add, abs-keys-orphans,
aubifs-inv/orphans is used by abs-orphans, abs-keys-orphans2, abs-keys-orphans-add2, abs-keys-orphans-add, abs-keys-orphans, abs-files-orphans, abs-files-del-orphans, abs-dirs-orphans, abs-dirs-del-orphans,

Used from specification key

key/disj-01 is used by abs-files-del-file, abs-files-del-dir, abs-files-del-data, abs-dirs-del-data,
key/disj-02 is used by abs-files-del-dentry, abs-dirs-del-file, abs-dirs-del-dir, abs-dirs-del-dentry,
key/disj-03 is used by abs-files-del-dentry, abs-dirs-del-data,
key/elim-01 is used by abs-keys-orphans2, abs-keys-orphans-add2, abs-keys-orphans-add, abs-keys-orphans,
key/elim-03 is used by dups-eqsize-ls, dups-eqsize-entries,
key/inj-01 is used by dups-eqsize-ls, dups-eqsize-entries, abs-dirs-del-dentry,
key/inj-02 is used by abs-files-del-data,
key/inj-03 is used by abs-keys-orphans-add2, abs-keys-orphans-add, abs-keys-del, abs-keys-add, abs-files-del-file, abs-files-del-dir, abs-dirs-del-file, abs-dirs-del-dir,
key/sel-01 is used by dups-eqsize-ls, dups-eqsize-entries,
key/sel-02 is used by dups-eqsize-ls, dups-eqsize-entries,
key/sel-03 is used by abs-files-evict, abs-files-del-orphans,
key/sel-04 is used by abs-orphans, abs-keys-orphans2, abs-keys-orphans-add2, abs-keys-orphans-add, abs-keys-orphans, abs-files-orphans, abs-files-evict, abs-files-del-orphans, abs-dirs-orphans, abs-dirs-del-orphans,
key/test-01 is used by dups-eqsize-ls, dups-eqsize-entries,
key/test-02 is used by abs-orphans, abs-keys-orphans2, abs-keys-orphans-add2, abs-keys-orphans-add, abs-keys-orphans, abs-files-orphans, abs-files-evict, abs-files-del-orphans, abs-dirs-orphans, abs-dirs-del-orphans,
key/test-04 is used by abs-files-orphans, abs-files-del-orphans,
key/test-06 is used by abs-dirs-orphans, abs-dirs-del-orphans,
key/test-07 is used by abs-dirs-deldatakeys-2, abs-dirs-deldatakeys-1, abs-dirs-del-orphans,
key/test-08 is used by abs-orphans-diff-datakeys, abs-files-evict, abs-files-del-orphans, abs-dirs-deldatakeys-2, abs-dirs-deldatakeys-1, abs-dirs-del-orphans,
key/test-09 is used by abs-files-evict, abs-files-del-orphans,

Used from specification aubifs-base

aubifs-base/at-dels-ro-data is used by abs-files-del-orphans,
aubifs-base/at-dels-ro-nodata is used by abs-files-del-orphans, abs-dirs-del-orphans,
aubifs-base/in-dels-ro is used by abs-files-del-orphans, abs-dirs-del-orphans,
aubifs-base/data-at-del-datakeys is used by abs-files-evict,
aubifs-base/datakeys is used by abs-orphans-diff-datakeys, abs-files-evict, abs-dirs-deldatakeys-2, abs-dirs-deldatakeys-1,
aubifs-base/datakeys-ge is used by abs-orphans-diff-datakeys, abs-dirs-deldatakeys-2,
aubifs-base/dentry-at-del-datakeys is used by abs-dirs-deldatakeys-1,
aubifs-base/in-dels-inode is used by abs-files-del-orphans, abs-dirs-del-orphans,
aubifs-base/index-update-in is used by abs-files-gc-copy, abs-dirs-gc-copy,
aubifs-base/inode-at-del-datakeys is used by abs-files-evict, abs-dirs-deldatakeys-1,
aubifs-base/range is used by abs-files-unused-adrs, abs-dirs-unused-adrs,
aubifs-base/range-inter-empty-in is used by abs-files-unused-adrs, abs-dirs-unused-adrs,
aubifs-base/toSet-subseteq-domri-notin is used by abs-files-gc-copy, abs-dirs-gc-copy,

Used from specification set-union

set-union/dir-heap-refset/Delete is used by abs-keys-del,
set-union/node-index/Delete is used by abs-keys-del,
set-union/node-store/Intersect is used by abs-files-unused-adrs, abs-dirs-unused-adrs,
set-union/node-store/int-a is used by abs-files-unused-adrs, abs-dirs-unused-adrs,
set-union/node-store/int-c is used by abs-files-unused-adrs, abs-dirs-unused-adrs,
set-union/node-index/una is used by Diff-union-comm,
set-union/node-index/unc is used by Diff-union-comm,
set-union/node-index/unin is used by Diff-union-comm,
set-union/node-index/unin-01 is used by Diff-union-comm,

Used from specification store

store/node-index/Del-in is used by abs-files-del-data,
store/dir-entries/exin is used by dups-eqsize-entries,
store/dir-entries/k-Extension is used by dups-eqsize-entries, C-ext,
store/file-content/k-Extension is used by P-ext,
store/node-index/k-Extension is used by Diff-union-comm,
store/node-store/At-other is used by abs-files-trunc, abs-files-drop, abs-dirs-trunc, abs-dirs-drop,
store/node-store/At-same is used by abs-files-trunc, abs-files-drop, abs-dirs-trunc, abs-dirs-drop,
store/file-content/Del-at is used by abs-files-del-data,
store/node-index/Del-at is used by abs-files-del-data, abs-dirs-del-dentry,
store/dir-entries/Del-at is used by abs-dirs-del-dentry,
store/node-index/Del-at-strong is used by abs-files-del-file, abs-files-del-dir, abs-files-del-dentry, abs-files-del-data, abs-dirs-del-file, abs-dirs-del-dir, abs-dirs-del-dentry, abs-dirs-del-data,
store/node-index/Del-in is used by abs-files-del-file, abs-files-del-dir, abs-files-del-dentry, abs-files-del-data, abs-dirs-del-file, abs-dirs-del-dir, abs-dirs-del-dentry, abs-dirs-del-data,
store/dir-entries/Del-in is used by abs-dirs-del-dentry,
store/file-content/Del-in is used by abs-files-del-data,
store/dir-entries/In-empty is used by dups-eqsize-entries, afs-cons-remove-orphans,
store/dir-entries/In-insert is used by dups-eqsize-entries,
store/dir-entries/Size-empty is used by afs-cons-remove-orphans,
store/dir-entries/Size-insert is used by dups-eqsize-entries,
store/dir-entries/empty is used by dups-eqsize-entries,
store/node-index/notmemlookup is used by abs-files-unused-adrs, abs-files-evict, abs-dirs-unused-adrs, abs-dirs-deldatakeys-1,

Used from specification nat

nat/one-02 is used by abs-orphans,

Used from specification set-basic

set-basic/node-store/Extension is used by abs-files-unused-adrs, abs-dirs-unused-adrs,
set-basic/alink-set/Extension is used by dups-eqsize-ls,
set-basic/dir-heap-refset/Extension is used by abs-orphans-diff-datakeys, abs-orphans, abs-keys-orphans2, abs-keys-orphans-add2, abs-keys-orphans-add, abs-keys-orphans, abs-keys-empty, abs-keys-del, abs-keys-add,
set-basic/node-index/Extension is used by dups-eqsize-ls, dups-eqsize-entries, abs-keys-orphans2, abs-keys-orphans-add2, abs-keys-orphans-add, abs-keys-orphans,
set-basic/alink-set/indef is used by dups-eqsize-ls,
set-basic/node-index/indef is used by dups-eqsize-ls, dups-eqsize-entries,
set-basic/node-store/In-empty is used by abs-files-unused-adrs, abs-dirs-unused-adrs,
set-basic/alink-set/In-empty is used by dups-eqsize-ls,
set-basic/node-index/In-empty is used by dups-eqsize-ls, dups-eqsize-entries, abs-keys-empty,
set-basic/dir-heap-refset/In-empty is used by abs-keys-empty,
set-basic/node-index/In-insert is used by dups-eqsize-ls, dups-eqsize-entries, abs-keys-orphans-add2, abs-keys-orphans-add, abs-keys-add,
set-basic/alink-set/In-insert is used by dups-eqsize-ls,
set-basic/dir-heap-refset/In-insert is used by abs-keys-orphans-add2, abs-keys-orphans-add, abs-keys-add,
set-basic/node-index/Size-empty is used by dups-eqsize-ls, dups-eqsize-entries,
set-basic/alink-set/Size-insert is used by dups-eqsize-ls,
set-basic/node-index/Size-insert is used by dups-eqsize-ls, dups-eqsize-entries,
set-basic/alink-set/ne is used by dups-eqsize-ls,
set-basic/node-index/ne-01 is used by dups-eqsize-ls,
set-basic/alink-set/ne-01 is used by dups-eqsize-ls,
set-basic/node-store/ne-01 is used by abs-files-unused-adrs, abs-dirs-unused-adrs,
set-basic/node-index/size-zero is used by dups-eqsize-ls, dups-eqsize-entries,
set-basic/dir-heap-refset/size-zero is used by abs-keys-empty,
set-basic/alink-set/size-zero is used by dups-eqsize-ls, abs-orphans,
set-basic/node-store/size-zero-01 is used by abs-files-unused-adrs, abs-dirs-unused-adrs,
set-basic/node-index/size-zero-01 is used by dups-eqsize-ls, dups-eqsize-entries,
set-basic/dir-heap-refset/size-zero-01 is used by abs-keys-empty,
set-basic/alink-set/size-zero-01 is used by dups-eqsize-ls, abs-orphans,
set-basic/alink-set/size-zero-02 is used by abs-orphans,

Used from specification abstract-dir

abstract-dir/elim is used by afs-cons-remove-orphans,
abstract-dir/inj is used by D-inj,
abstract-dir/sel-03 is used by afs-cons-remove-orphans, abs-orphans,
abstract-dir/sel-05 is used by afs-cons-remove-orphans, abs-orphans,
abstract-dir/sel-08 is used by afs-cons-remove-orphans, abs-orphans,
abstract-dir/sel-09 is used by afs-cons-remove-orphans, abs-orphans,

Used from specification heap

heap/file-heap/at-diffs is used by abs-files-orphans, abs-files-del-orphans,
heap/dir-heap/at-diffs is used by abs-dirs-orphans, abs-dirs-del-orphans,
heap/dir-heap/ext is used by D-ext,
heap/file-heap/ext is used by abs-files-orphans, abs-files-evict, F-ext,
heap/dir-heap/at-del is used by abs-dirs-del-dir,
heap/file-heap/at-del is used by abs-files-evict, abs-files-del-file,
heap/dir-heap/at-diffs is used by afs-cons-remove-orphans,
heap/file-heap/at-diffs is used by afs-cons-remove-orphans,
heap/dir-heap/at-write is used by abs-dirs-del-dentry,
heap/file-heap/at-write is used by abs-files-del-data,
heap/dir-heap/in-del is used by abs-dirs-del-dir,
heap/file-heap/in-del is used by abs-files-evict, abs-files-del-file,
heap/file-heap/in-diffs is used by afs-cons-remove-orphans, abs-files-orphans, abs-files-del-orphans,
heap/dir-heap/in-diffs is used by afs-cons-remove-orphans, abs-dirs-orphans, abs-dirs-del-orphans,
heap/dir-heap/in-write is used by abs-dirs-del-dentry,
heap/file-heap/in-write is used by abs-files-del-data,