Used simplifier rules/spec theorems by specification

Used from specification root-ino

• root-ino/neq-0 is used by inv-rename-overwrite-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-rmdir, inv-truncate, inv-write-inode, inv-evict, inv-format,

Used from specification store+set

• store+set/node-index/Data-in is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-rmdir, inv-truncate,
• store+set/node-index/Data-in-delput is used by data-notin-del2,
• store+set/node-index/Data-notin-other is used by data-notin-other1,
• store+set/node-index/Data-notin-other-2 is used by data-notin-other2,
• store+set/node-store/Diff-get is used by inv-check-commit, inv-gc,
• store+set/node-index/Diff-base is used by inv-truncate,
• store+set/node-index/Diff-del-rw is used by replayorphans-prepost, replayone-prog, inv-evict,
• store+set/node-store/Diff-ext is used by inv-check-commit,
• store+set/node-index/Diff-get is used by at-diff-ri, inv-replay,
• store+set/node-index/Diff-mems-get is used by at-diff-ri,
• store+set/node-store/Diff-mems-get is used by inv-check-commit, inv-gc,
• store+set/node-index/Dom is used by ubifs-cons-reduce, ubifs-cons-dentry-target-not-in-orphans, inv-replay, inv-create, inv-mkdir, inv-truncate, inv-evict,
• store+set/node-index/In-data-in is used by inv-truncate,
• store+set/node-index/dom-emp is used by inv-format,
• store+set/node-index/dom-ins is used by inv-format,

Used from specification nat-basic

• nat-basic/a is used by replayorphans-prepost, replaylog-prog, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-overwrite-reparent, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-readpage, inv-truncate,
• nat-basic/add-base is used by inv-readpage,
• nat-basic/c is used by replayorphans-prepost, replaylog-prog, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-overwrite-reparent, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-readpage, inv-truncate,
• nat-basic/f is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-overwrite-reparent, inv-readpage, inv-truncate,
• nat-basic/lf-01 is used by inv-readpage, inv-truncate,
• nat-basic/lf-02 is used by inv-rename-new-reparent, inv-readpage, inv-truncate,
• nat-basic/ls-02 is used by inv-readpage, inv-truncate,
• nat-basic/one is used by inv-rename-new-reparent, inv-rmdir,
• nat-basic/one-01 is used by replayorphans-prepost, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-overwrite-reparent,
• nat-basic/one-06 is used by inv-rename-overwrite-keep-parent, inv-rename-overwrite-reparent, inv-unlink,
• nat-basic/oz is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-overwrite-reparent, inv-mkdir, inv-unlink, inv-rmdir, inv-link,
• nat-basic/ref is used by replayorphans-prepost, replaylog-prog,
• nat-basic/s-04 is used by replayorphans-prepost, replaylog-prog,
• nat-basic/succ is used by replaylog-prog,
• nat-basic/zero is used by inv-rename-new-reparent,
• nat-basic/zero-01 is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-overwrite-reparent,

Used from specification aubifs-asm

• aubifs-asm/in-diff-ri is used by replayorphans-prepost, in-diff-ri, inv-replay, inv-truncate, inv-evict,

Used from specification list+set

• list+set/address-list-set/toSet-app is used by inv-gc,

Used from specification node

• node/elim-02 is used by ubifs-cons-reduce, replayone-prog, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode,
• node/elim-03 is used by ubifs-cons-reduce, replayone-prog, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-truncate, inv-write-inode,
• node/elim-04 is used by replayone-prog,
• node/elim-05 is used by ubifs-cons-reduce, replayone-prog, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-replay, inv-create, inv-mkdir, inv-truncate, inv-write-inode,
• node/inj-01 is used by inv-rename-overwrite-keep-parent, inv-rename-overwrite-reparent,
• node/inj-02 is used by inv-truncate,
• node/inj-04 is used by inv-rename-overwrite-keep-parent,
• node/sel-01 is used by replayone-prog, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link,
• node/sel-03 is used by inv-writepage, inv-truncate,
• node/sel-04 is used by replayone-prog, inv-truncate,
• node/sel-05 is used by replayone-prog, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-truncate, inv-write-inode, inv-format,
• node/sel-09 is used by replayone-prog, inv-writepage, inv-truncate,
• node/sel-11 is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-truncate, inv-write-inode, inv-format,
• node/sel-14 is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link,
• node/sel-15 is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-truncate, inv-write-inode,
• node/sel-16 is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-truncate, inv-write-inode,
• node/test-01 is used by replayone-prog, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link,
• node/test-02 is used by ubifs-cons-reduce, replayone-prog, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode,
• node/test-03 is used by replayone-prog, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link,
• node/test-06 is used by ubifs-cons-reduce, replayone-prog, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-truncate, inv-write-inode, inv-format,
• node/test-08 is used by ubifs-cons-reduce, replayone-prog, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-truncate, inv-write-inode,
• node/test-09 is used by ubifs-cons-reduce, replayone-prog, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-truncate, inv-write-inode,
• node/test-11 is used by replayone-prog, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-truncate, inv-write-inode,
• node/test-12 is used by replayone-prog, inv-replay, inv-writepage, inv-truncate,
• node/test-13 is used by ubifs-cons-reduce, replayone-prog, inv-replay, inv-writepage, inv-truncate,
• node/test-14 is used by replayone-prog, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link,
• node/test-15 is used by replayone-prog, inv-truncate,
• node/test-16 is used by replayone-prog, inv-truncate,
• node/test-17 is used by replayone-prog, inv-truncate,
• node/test-18 is used by replayone-prog, inv-truncate,
• node/test-19 is used by replayone-prog, inv-writepage, inv-truncate,
• node/test-22 is used by ubifs-cons-reduce, replayone-prog, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-replay, inv-create, inv-mkdir, inv-writepage, inv-truncate, inv-write-inode,
• node/upd-02 is used by inv-truncate,

Used from specification aubifs-replay

• aubifs-replay/orphans-cons is used by inv-format,
• aubifs-replay/replay-cons-strong is used by inv-replay, inv-truncate, inv-evict, inv-format, inv-gc,
• aubifs-replay/replay-cons-strong-append is used by inv-create, inv-mkdir, inv-link, inv-writepage, inv-write-inode,
• aubifs-replay/replay-orphans-data is used by inv-writepage,
• aubifs-replay/replay-orphans-del is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-rmdir,
• aubifs-replay/replay-orphans-dentry is used by inv-create, inv-mkdir, inv-link,
• aubifs-replay/replay-orphans-inode is used by inv-create, inv-mkdir,
• aubifs-replay/orphans-cons-reduce is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-check-commit, inv-replay, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode, inv-evict, inv-gc,
• aubifs-replay/replay is used by replay-prog, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-replay, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode, inv-evict, inv-format, inv-gc,
• aubifs-replay/replay-cons-strong-empty-log is used by inv-check-commit,
• aubifs-replay/replay-cons-strong-safe is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-replay, inv-unlink, inv-rmdir, inv-truncate, inv-evict, inv-gc,
• aubifs-replay/replay-cons-strong-variant1 is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-replay, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode,
• aubifs-replay/replay-data is used by replayone-prog, inv-writepage, inv-truncate,
• aubifs-replay/replay-dentry is used by replayone-prog, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link,
• aubifs-replay/replay-drop-data is used by inv-writepage, inv-truncate,
• aubifs-replay/replay-ino is used by replayone-prog, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-truncate, inv-write-inode, inv-format,
• aubifs-replay/replay-log-empty is used by replaylog-prog,
• aubifs-replay/replay-log-gc-copy is used by inv-gc,
• aubifs-replay/replay-log-gc-copy-old is used by inv-gc,
• aubifs-replay/replay-log-gc-drop is used by inv-gc,
• aubifs-replay/replay-log-one is used by replaylog-prog, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode, inv-format,
• aubifs-replay/replay-log-rec is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-truncate,
• aubifs-replay/replay-log-split is used by replaylog-prog,
• aubifs-replay/replay-log-write is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-rmdir, inv-truncate,
• aubifs-replay/replay-nonorphans-trunc is used by inv-truncate,
• aubifs-replay/replay-orphans-del is used by inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-link,
• aubifs-replay/replay-orphans-inode is used by inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-truncate, inv-write-inode,
• aubifs-replay/replay-orphans-trunc is used by inv-truncate,
• aubifs-replay/replay-safe-gc-copy is used by inv-gc,
• aubifs-replay/replay-safe-gc-copy-old is used by inv-gc,
• aubifs-replay/replay-safe-gc-drop is used by inv-gc,
• aubifs-replay/replay-safe-one is used by replayone-prog, replaylog-prog, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode, inv-format,
• aubifs-replay/replay-safe-rec is used by replaylog-prog, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-truncate,
• aubifs-replay/replay-safe-split is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode, inv-gc,
• aubifs-replay/replay-safe-write is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-rmdir, inv-truncate,
• aubifs-replay/replay-split is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode, inv-gc,
• aubifs-replay/replay-trunc is used by replayone-prog, inv-truncate,
• aubifs-replay/ri-closed-gc is used by inv-gc,

Used from specification aubifs-inv

• aubifs-inv/file-node-cons is used by inv-format,
• aubifs-inv/key-cons is used by ubifs-cons-reduce, inv-replay,
• aubifs-inv/log-cons is used by ubifs-cons-reduce,
• aubifs-inv/log-cons-variant1-01 is used by inv-link,
• aubifs-inv/node-closed is used by ubifs-cons-reduce, inv-replay,
• aubifs-inv/node-cons is used by ubifs-cons-reduce,
• aubifs-inv/ri-closed is used by ubifs-cons-reduce, ubifs-cons-dentry-target-not-in-orphans, inv-truncate, inv-format,
• aubifs-inv/ri-closed-drop is used by inv-gc,
• aubifs-inv/ri-closed-variant1-01 is used by inv-replay,
• aubifs-inv/ri-cons is used by ubifs-cons-reduce, inode-ubifs-cons, dentry-ubifs-cons, data-ubifs-cons, inv-replay, inv-truncate, inv-format,
• aubifs-inv/ri-cons-variant1-01 is used by inv-create, inv-mkdir, inv-link,
• aubifs-inv/ubifs-cons is used by ubifs-cons-reduce, ubifs-cons-dentry-target-not-in-orphans, inode-ubifs-cons, dentry-ubifs-cons, data-ubifs-cons, inv-replay, inv-truncate, inv-format, inv-gc,
• aubifs-inv/datakey-cons is used by ubifs-cons-reduce, replayone-prog, data-ubifs-cons, inv-writepage, inv-truncate,
• aubifs-inv/datalkeys-drop-orphans is used by inv-truncate,
• aubifs-inv/datalkeys-drop-orphans-in is used by inv-truncate,
• aubifs-inv/datanode-closed is used by ubifs-cons-reduce, inv-truncate,
• aubifs-inv/datanode-cons is used by replayone-prog, inv-writepage, inv-truncate,
• aubifs-inv/datanode-pagesize is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-readpage, inv-writepage, inv-truncate, inv-write-inode, inv-evict,
• aubifs-inv/dentrykey-cons is used by ubifs-cons-reduce, replayone-prog, dentry-ubifs-cons, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-link,
• aubifs-inv/dentrynode-closed is used by ubifs-cons-reduce, ubifs-cons-dentry-target-not-in-orphans,
• aubifs-inv/dentrynode-cons is used by replayone-prog, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link,
• aubifs-inv/empty-inodes is used by replayorphans-prepost, inv-replay, inv-format,
• aubifs-inv/file-node-cons-variant1-01 is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-check-commit, inv-replay, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode, inv-evict, inv-gc,
• aubifs-inv/inodekey-cons is used by ubifs-cons-reduce, replayone-prog, inode-ubifs-cons, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-truncate, inv-write-inode, inv-format,
• aubifs-inv/inodenode-closed is used by inv-format,
• aubifs-inv/inodenode-cons is used by replayone-prog, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-truncate, inv-write-inode, inv-format,
• aubifs-inv/inodes-del is used by replayorphans-prepost, inv-evict,
• aubifs-inv/inodes-in is used by replayorphans-prepost,
• aubifs-inv/inodes-nodata is used by replayorphans-prepost, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-replay, inv-unlink, inv-rmdir, inv-writepage, inv-truncate, inv-evict,
• aubifs-inv/inodes-nodentry is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-replay, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link,
• aubifs-inv/inodes-put is used by inv-rename-overwrite-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-rmdir,
• aubifs-inv/log-adr-in is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-truncate,
• aubifs-inv/log-cons-app is used by inv-create, inv-mkdir, inv-link, inv-gc,
• aubifs-inv/log-cons-one is used by inv-create, inv-mkdir, inv-link, inv-format,
• aubifs-inv/log-cons-variant1-01 is used by inv-create, inv-mkdir, inv-link,
• aubifs-inv/log-node-cons is used by inv-create, inv-mkdir, inv-link,
• aubifs-inv/nodups-new-nodups is used by inv-gc,
• aubifs-inv/read-lookup-copy is used by inv-gc,
• aubifs-inv/ri-cons-del-orphans is used by inv-replay,
• aubifs-inv/ri-cons-empty is used by inv-format,
• aubifs-inv/ri-cons-in is used by ubifs-cons-reduce, inv-rename-overwrite-keep-parent, inv-rename-overwrite-reparent, inv-replay, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-truncate,
• aubifs-inv/ri-cons-inj is used by inv-truncate, inv-gc,
• aubifs-inv/ri-cons-key is used by ubifs-cons-reduce, inv-rename-overwrite-keep-parent, inv-rename-overwrite-reparent, inv-replay, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-truncate,
• aubifs-inv/ri-cons-variant1-01 is used by inv-create, inv-mkdir, inv-link, inv-truncate, inv-gc,
• aubifs-inv/ri-inj-empty is used by inv-format,
• aubifs-inv/ri-key-cons is used by inv-create, inv-mkdir, inv-link,
• aubifs-inv/truncnode-cons is used by replayone-prog, inv-truncate,
• aubifs-inv/ubifs-adr-in-ri is used by data-notin-other2, data-notin-other1, data-notin-del2, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode,
• aubifs-inv/ubifs-cons-dom-fi is used by ubifs-cons-reduce, inv-replay, inv-gc,
• aubifs-inv/ubifs-cons-dom-ri is used by ubifs-cons-reduce, inv-truncate, inv-evict,
• aubifs-inv/ubifs-cons-fo-inodes is used by ubifs-cons-reduce, inv-check-commit, inv-replay, inv-renam, inv-truncate, inv-format, inv-gc,
• aubifs-inv/ubifs-cons-ino0 is used by ubifs-cons-reduce, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-check-commit, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode, inv-evict,
• aubifs-inv/ubifs-cons-log-cons is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-check-commit, inv-replay, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-renam, inv-writepage, inv-truncate, inv-write-inode, inv-format, inv-gc,
• aubifs-inv/ubifs-cons-logadr-in is used by ubifs-cons-reduce,
• aubifs-inv/ubifs-cons-notin-dels is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-rmdir, inv-truncate,
• aubifs-inv/ubifs-cons-ri-inj is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-check-commit, inv-replay, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-renam, inv-writepage, inv-truncate, inv-write-inode, inv-evict, inv-format, inv-gc,
• aubifs-inv/ubifs-cons-ro-inodes is used by ubifs-cons-reduce, inv-rename-overwrite-keep-parent, inv-rename-overwrite-reparent, inv-replay, inv-unlink, inv-rmdir, inv-renam, inv-truncate, inv-evict, inv-format, inv-gc,
• aubifs-inv/ubifs-file-in is used by data-ubifs-cons, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-readpage, inv-truncate, inv-write-inode, inv-evict,
• aubifs-inv/ubifs-file-notdir is used by data-ubifs-cons, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-readpage, inv-truncate, inv-write-inode, inv-evict,
• aubifs-inv/ubifs-fo-subset is used by ubifs-cons-reduce, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode, inv-evict,
• aubifs-inv/ubifs-in-fs is used by ubifs-cons-reduce, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-iget, inv-lookup, inv-create, inv-mkdir, inv-unlink, inv-link, inv-readpage, inv-writepage, inv-truncate, inv-write-inode, inv-evict,
• aubifs-inv/ubifs-log-nodups is used by ubifs-cons-reduce, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-check-commit, inv-replay, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode, inv-evict,
• aubifs-inv/ubifs-log-nodups-add1 is used by inv-writepage, inv-write-inode,
• aubifs-inv/ubifs-log-nodups-add2 is used by inv-truncate,
• aubifs-inv/ubifs-log-nodups-add3 is used by inv-rename-new-keep-parent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-truncate,
• aubifs-inv/ubifs-log-nodups-add4 is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent,
• aubifs-inv/ubifs-log-nodups-add5 is used by inv-rename-overwrite-reparent,
• aubifs-inv/ubifs-parent-dir is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-renam, inv-writepage, inv-truncate, inv-write-inode,
• aubifs-inv/ubifs-parent-in is used by ubifs-cons-dentry-target-not-in-orphans, dentry-ubifs-cons, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-renam, inv-writepage, inv-truncate, inv-write-inode,
• aubifs-inv/ubifs-ri-cons is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-check-commit, inv-iget, inv-lookup, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-readpage, inv-writepage, inv-truncate, inv-write-inode, inv-gc,
• aubifs-inv/ubifs-ro-subset is used by ubifs-cons-reduce, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-check-commit, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode, inv-evict,

Used from specification aubifs-base

• aubifs-base/at-del-ro-data is used by inv-rename-overwrite-keep-parent, inv-rename-overwrite-reparent, inv-unlink,
• aubifs-base/at-del-ro-nodata is used by inv-rename-overwrite-keep-parent, inv-rename-overwrite-reparent, inv-unlink,
• aubifs-base/at-dels-ro-data is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-rmdir, inv-truncate,
• aubifs-base/at-dels-ro-nodata is used by replayorphans-prepost, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-replay, inv-unlink, inv-rmdir, inv-truncate, inv-evict,
• aubifs-base/del-with-data is used by replayone-prog,
• aubifs-base/dels-with-data is used by replayorphans-prepost, inv-replay, inv-evict,
• aubifs-base/in-del-ro is used by inv-rename-overwrite-keep-parent, inv-rename-overwrite-reparent, inv-unlink,
• aubifs-base/in-dels-ro is used by replayorphans-prepost, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-rmdir, inv-truncate, inv-evict,
• aubifs-base/new-inode-exists is used by inv-create, inv-mkdir,
• aubifs-base/at-del-ro-nodata is used by inv-truncate,
• aubifs-base/at-dels-ro-data is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent,
• aubifs-base/at-dels-ro-nodata is used by replayorphans-prepost, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent,
• aubifs-base/data-in-empty is used by inv-format,
• aubifs-base/datakeys is used by replayorphans-prepost, inv-truncate, inv-evict,
• aubifs-base/datakeys-0 is used by replayorphans-prepost, replayone-prog, inv-evict,
• aubifs-base/datakeys-ge is used by inv-truncate,
• aubifs-base/datakeys-put-inode-01 is used by inv-truncate,
• aubifs-base/datakeys-set is used by replayorphans-prepost, inv-replay, inv-evict,
• aubifs-base/datakeys-set-del is used by replayorphans-prepost, inv-evict,
• aubifs-base/del-del-again is used by inv-truncate, inv-write-inode,
• aubifs-base/del-put-again is used by inv-create, inv-mkdir, inv-truncate, inv-write-inode,
• aubifs-base/del-this is used by inv-rename-overwrite-reparent,
• aubifs-base/del-with-emp is used by replayorphans-prepost, inv-replay, inv-format,
• aubifs-base/dentrykeys is used by inv-rename-overwrite-keep-parent, inv-rename-overwrite-reparent, inv-rmdir,
• aubifs-base/in-del-ro is used by inv-rename-overwrite-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-truncate,
• aubifs-base/in-dels-inode is used by inv-rename-overwrite-keep-parent, inv-rename-overwrite-reparent, inv-replay, inv-writepage, inv-truncate, inv-write-inode,
• aubifs-base/in-dels-ro is used by replayorphans-prepost, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-replay, inv-unlink, inv-rmdir, inv-truncate, inv-evict,
• aubifs-base/index-lookup-length is used by inv-gc,
• aubifs-base/index-update-dom is used by inv-gc,
• aubifs-base/index-update-in is used by inv-gc,
• aubifs-base/links is used by inv-rename-overwrite-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-rmdir,
• aubifs-base/new-one is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode, inv-format,
• aubifs-base/new-rec is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-truncate,
• aubifs-base/notin-dels is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent,
• aubifs-base/range-inter-empty-in is used by inv-check-commit, inv-gc,
• aubifs-base/read-length is used by inv-gc,
• aubifs-base/toSet-subseteq-domri-notin is used by inv-gc,
• aubifs-base/valid-dentry is used by inv-link,
• aubifs-base/valid-dentry-with-parent is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-rmdir, inv-link, inv-renam,
• aubifs-base/valid-dir-ino is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-lookup, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-renam, inv-readdir, inv-write-inode,
• aubifs-base/valid-file-ino is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-link, inv-renam, inv-readpage, inv-writepage, inv-truncate, inv-write-inode,
• aubifs-base/valid-ino is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-iget, inv-unlink, inv-rmdir, inv-link, inv-renam, inv-evict,
• aubifs-base/valid-negdentry-with-parent is used by inv-rename-new-reparent, inv-rename-new-keep-parent, inv-create, inv-mkdir, inv-link, inv-renam,
• aubifs-base/valid-parent-ino is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-lookup, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-renam,

Used from specification key

• key/disj-01 is used by replayorphans-prepost, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode, inv-evict,
• key/disj-02 is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-truncate, inv-write-inode,
• key/disj-03 is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-rmdir, inv-writepage, inv-truncate,
• key/disjpred-02 is used by inv-truncate, inv-evict,
• key/disjpred-04 is used by inv-truncate, inv-evict,
• key/inj-01 is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-link,
• key/inj-02 is used by inv-writepage, inv-truncate,
• key/inj-03 is used by replayone-prog, elim-inode, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-truncate, inv-write-inode, inv-evict, inv-format,
• key/inodekey-id is used by replayorphans-prepost, inv-rename-new-reparent, inv-replay, inv-unlink, inv-link, inv-truncate,
• key/sel-02 is used by ubifs-cons-reduce, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-replay, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode,
• key/sel-03 is used by ubifs-cons-reduce, replayorphans-prepost, replayone-prog, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-replay, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode, inv-evict,
• key/sel-04 is used by ubifs-cons-reduce, replayorphans-prepost, replayone-prog, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-replay, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode, inv-evict, inv-format,
• key/sel-05 is used by inv-truncate,
• key/test-01 is used by ubifs-cons-reduce, elim-dentry, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-replay, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode,
• key/test-02 is used by ubifs-cons-reduce, elim-inode, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode, inv-evict, inv-format,
• key/test-03 is used by ubifs-cons-reduce, elim-dentry, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-replay, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode, inv-evict,
• key/test-04 is used by ubifs-cons-reduce, elim-inode, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-replay, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode, inv-evict,
• key/test-05 is used by ubifs-cons-reduce, elim-dentry, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode,
• key/test-06 is used by ubifs-cons-reduce, elim-inode, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-replay, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode,
• key/test-07 is used by ubifs-cons-reduce, elim-data, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode,
• key/test-08 is used by ubifs-cons-reduce, elim-data, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-replay, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode, inv-evict,
• key/test-09 is used by ubifs-cons-reduce, replayorphans-prepost, elim-data, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-replay, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode, inv-evict,

Used from specification store

• store/node-index/Extension is used by replayorphans-prepost, inv-evict,
• store/node-index/k-Extension is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-rmdir, inv-truncate,
• store/node-index/notin-del-notin is used by inv-write-inode,
• store/node-store/At-in-out is used by inv-create, inv-mkdir, inv-link,
• store/node-index/At-other is used by at-ri, inv-rename-overwrite-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-rmdir, inv-truncate,
• store/node-store/At-other is used by at-fs, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-truncate,
• store/node-index/At-same is used by at-ri,
• store/node-store/At-same is used by at-fs,
• store/node-index/Del-at is used by at-del-ri, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-rmdir, inv-evict,
• store/node-index/Del-in is used by replayorphans-prepost, in-del-ri, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-rmdir, inv-evict,
• store/node-index/Del-rec-same is used by inv-rename-overwrite-reparent,
• store/node-store/In-empty is used by inv-format,
• store/node-index/In-empty is used by inv-format,
• store/node-index/In-insert is used by in-ri, inv-rename-overwrite-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-truncate,
• store/node-store/In-insert is used by inv-create, inv-mkdir, inv-link,
• store/node-index/del-put is used by inv-rename-overwrite-keep-parent,
• store/node-index/deldel is used by inv-rename-overwrite-keep-parent,
• store/node-index/in-neq is used by in-ri, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-rmdir, inv-truncate,
• store/node-store/in-neq is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-truncate,
• store/node-index/lookupisempty is used by at-del-ri,
• store/node-index/notmemlookup is used by replayorphans-prepost, inv-rename-overwrite-keep-parent, inv-check-commit, inv-writepage, inv-write-inode, inv-evict,
• store/node-store/notmemlookup is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode,

Used from specification set-union

• set-union/node-index/Difference is used by replayorphans-prepost, inv-evict,
• set-union/node-index/size-eq-ext is used by size-eq,
• set-union/node-index/subdef is used by ubifs-cons-reduce,
• set-union/node-index/Delete is used by replayorphans-prepost, inv-evict,
• set-union/node-index/Difference is used by inv-evict,
• set-union/node-index/One is used by inv-rename-overwrite-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-renam,
• set-union/node-index/del-size is used by replayorphans-prepost,
• set-union/node-store/int-a is used by inv-check-commit, inv-gc,
• set-union/node-store/int-c is used by inv-check-commit, inv-gc,
• set-union/node-store/int-e is used by inv-check-commit,
• set-union/node-store/intu-empty is used by inv-gc,
• set-union/node-index/sub-del-03 is used by replayorphans-prepost,
• set-union/node-index/sub-union is used by inv-gc,
• set-union/node-store/una is used by inv-gc,
• set-union/node-index/una is used by inv-create, inv-mkdir, inv-gc,
• set-union/node-index/unadd is used by inv-create, inv-mkdir,
• set-union/node-store/unc is used by inv-gc,
• set-union/node-index/unc is used by inv-create, inv-mkdir, inv-gc,
• set-union/node-index/une is used by inv-create, inv-mkdir,
• set-union/node-index/unin-01 is used by inv-create, inv-mkdir,

Used from specification nat

• nat/anti is used by inv-truncate,
• nat/elim-pred-c is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-overwrite-reparent, inv-unlink, inv-rmdir,
• nat/elim-sub is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-overwrite-reparent, inv-truncate,
• nat/eq-02 is used by inv-truncate,
• nat/fle is used by inv-truncate,
• nat/fle-01 is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-overwrite-reparent,
• nat/ge is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-rmdir, inv-renam, inv-truncate,
• nat/le is used by inv-truncate,
• nat/le-def is used by replayorphans-prepost, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-overwrite-reparent, inv-readpage, inv-truncate,
• nat/lels-02 is used by inv-rmdir, inv-truncate,
• nat/lep is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-overwrite-reparent, inv-unlink, inv-rmdir,
• nat/lep-02 is used by inv-truncate,
• nat/ler is used by inv-readpage, inv-truncate,
• nat/ls-01 is used by replayorphans-prepost,
• nat/ls-le-simp is used by inv-truncate,
• nat/not-zero is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-rmdir, inv-renam,
• nat/zero-02 is used by inv-rmdir, inv-truncate,

Used from specification min-max

• min-max/min-comm is used by inv-truncate,
• min-max/min-le-left is used by inv-truncate,

Used from specification error-class

• error-class/ecommit is used by replayone-prog, replay-prog, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-sync, inv-check-commit, inv-iget, inv-lookup, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-readpage, inv-writepage, inv-readdir, inv-truncate, inv-write-inode, inv-format,
• error-class/esuccess is used by replayone-prog, replay-prog, inv-iget, inv-lookup, inv-readpage, inv-truncate, inv-format,
• error-class/not-esuccess is used by replayone-prog, replay-prog, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode, inv-format,

Used from specification error

• error/disj-35 is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode, inv-format,
• error/disj-91 is used by replayone-prog, replay-prog, inv-sync, inv-iget, inv-lookup, inv-readpage, inv-readdir, inv-format,

Used from specification set-basic

• set-basic/node-index/Extension is used by replayorphans-prepost, inv-rename-overwrite-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-rmdir,
• set-basic/node-index/In-empty is used by replayorphans-prepost, inv-rename-overwrite-keep-parent, inv-rename-overwrite-reparent, inv-replay, inv-rmdir, inv-format,
• set-basic/node-index/In-insert is used by inv-rename-overwrite-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-rmdir,
• set-basic/node-index/add is used by inv-rename-overwrite-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir,
• set-basic/node-index/in-02 is used by inv-unlink, inv-rmdir,
• set-basic/node-index/in-03 is used by inv-rename-overwrite-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-rmdir,
• set-basic/node-index/in-04 is used by inv-rename-overwrite-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-rmdir,
• set-basic/node-store/ne-01 is used by inv-check-commit,
• set-basic/node-index/ne-01 is used by ubifs-cons-reduce, ubifs-cons-dentry-target-not-in-orphans, size-eq, replayorphans-prepost, inv-rename-overwrite-keep-parent, inv-rename-overwrite-reparent, inv-replay, inv-unlink, inv-rmdir, inv-link, inv-truncate, inv-write-inode, inv-evict,
• set-basic/node-index/one-size is used by inv-rename-overwrite-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-rmdir,
• set-basic/node-index/size-one-01 is used by inv-rename-overwrite-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-rmdir,
• set-basic/node-index/size-zero is used by replayorphans-prepost, inv-evict,
• set-basic/node-store/size-zero-01 is used by inv-check-commit,
• set-basic/node-index/size-zero-01 is used by ubifs-cons-reduce, ubifs-cons-dentry-target-not-in-orphans, size-eq, replayorphans-prepost, inv-rename-overwrite-keep-parent, inv-rename-overwrite-reparent, inv-replay, inv-unlink, inv-link, inv-write-inode, inv-evict,
• set-basic/node-index/sub-e is used by replayorphans-prepost, inv-replay, inv-format,
• set-basic/node-index/sub-idem is used by replayorphans-prepost,
• set-basic/node-index/sub-in is used by ubifs-cons-dentry-target-not-in-orphans, replayorphans-prepost, inv-replay, inv-truncate, inv-evict,

Used from specification list-data

• list-data/address-list-set/elim-list-c is used by replaylog-prog,

Used from specification dentry

• dentry/elim is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-rmdir, inv-link, inv-renam,
• dentry/elim-02 is used by inv-rename-new-reparent, inv-rename-new-keep-parent, inv-create, inv-mkdir, inv-link, inv-renam,
• dentry/inj is used by inv-rename-overwrite-keep-parent,
• dentry/sel-03 is used by inv-rename-new-reparent, inv-rename-new-keep-parent, inv-create, inv-mkdir, inv-link, inv-renam,
• dentry/sel-04 is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-rmdir, inv-link, inv-renam,
• dentry/sel-05 is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-rmdir, inv-link, inv-renam,
• dentry/test-01 is used by inv-rename-new-reparent, inv-rename-new-keep-parent, inv-create, inv-mkdir, inv-link, inv-renam,
• dentry/test-02 is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-rmdir, inv-link, inv-renam,
• dentry/test-03 is used by inv-renam,
• dentry/test-04 is used by inv-renam,

Used from specification page

• page/page-size is used by inv-readpage, inv-truncate,

Used from specification list

• list/address-list-set/a is used by inv-truncate,
• list/address-list-set/Last is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode, inv-format,
• list/address-list-set/Nil is used by inv-format,
• list/address-list-set/a is used by replaylog-prog, inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode, inv-format, inv-gc,
• list/address-list-set/app is used by replaylog-prog,
• list/address-list-set/app-03 is used by replaylog-prog,
• list/address-list-set/app-05 is used by replaylog-prog,
• list/address-list-set/c is used by replaylog-prog,
• list/address-list-set/e-01 is used by replaylog-prog,
• list/address-list-set/in-17 is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode,
• list/address-list-set/in-append is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode,
• list/address-list-set/in-empty is used by inv-check-commit,
• list/address-list-set/in-rec is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-truncate,
• list/address-list-set/len-05 is used by replaylog-prog,

Used from specification node-store

• node-store/in-insert is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write-inode, inv-format,

Used from specification array-copy

• array-copy/buffer/size-fill-h is used by inv-truncate,

Used from specification list-dup

• list-dup/address-list-set/c is used by inv-writepage, inv-write-inode, inv-format,
• list-dup/address-list-set/dups-cons is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-truncate,
• list-dup/address-list-set/e-01 is used by inv-check-commit,
• list-dup/address-list-set/rec is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-truncate,
• list-dup/address-list-set/two-01 is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-truncate,

Used from specification nat-mult

• nat-mult/mult-a is used by inv-truncate,
• nat-mult/mult-c is used by inv-truncate,

Used from specification inode

• inode/elim is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-renam, inv-readpage, inv-writepage, inv-readdir, inv-truncate, inv-write-inode, inv-evict,
• inode/inj is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-renam, inv-truncate,
• inode/sel-01 is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-renam, inv-readpage, inv-writepage, inv-truncate, inv-write-inode,
• inode/sel-02 is used by inv-renam, inv-truncate, inv-write-inode,
• inode/sel-03 is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-renam, inv-truncate, inv-write-inode,
• inode/sel-04 is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-renam, inv-truncate, inv-write-inode,
• inode/sel-10 is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-renam, inv-truncate, inv-write-inode,
• inode/sel-11 is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-renam, inv-truncate, inv-write-inode,

Used from specification nat-div

• nat-div/rax is used by inv-truncate,
• nat-div/cond is used by inv-truncate,
• nat-div/cond-01 is used by inv-truncate,
• nat-div/mod-le-02 is used by inv-truncate,

Used from specification aubifs-pre

• aubifs-pre/pre-create is used by inv-create,
• aubifs-pre/pre-mkdir is used by inv-mkdir,
• aubifs-pre/pre-evict is used by inv-evict,
• aubifs-pre/pre-iget is used by inv-iget,
• aubifs-pre/pre-link is used by inv-link,
• aubifs-pre/pre-lookup is used by inv-lookup,
• aubifs-pre/pre-readdir is used by inv-readdir,
• aubifs-pre/pre-readpage is used by inv-readpage,
• aubifs-pre/pre-rename is used by inv-renam,
• aubifs-pre/pre-rename-new-keep-parent is used by inv-rename-new-keep-parent, inv-renam,
• aubifs-pre/pre-rename-new-reparent is used by inv-rename-new-reparent, inv-renam,
• aubifs-pre/pre-rename-overwrite-keep-parent is used by inv-rename-overwrite-keep-parent, inv-renam,
• aubifs-pre/pre-rename-overwrite-reparent is used by inv-rename-overwrite-reparent, inv-renam,
• aubifs-pre/pre-rmdir is used by inv-rmdir,
• aubifs-pre/pre-truncate is used by inv-truncate,
• aubifs-pre/pre-unlink is used by inv-unlink,
• aubifs-pre/pre-write-inode is used by inv-write-inode,
• aubifs-pre/pre-writepage is used by inv-writepage,
• aubifs-pre/valid-dir-inode is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-create, inv-mkdir, inv-unlink, inv-rmdir, inv-link, inv-renam, inv-write-inode,
• aubifs-pre/valid-file-inode is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-unlink, inv-link, inv-renam, inv-truncate, inv-write-inode,
• aubifs-pre/valid-wb-inode is used by inv-rename-overwrite-keep-parent, inv-rename-new-reparent, inv-rename-new-keep-parent, inv-rename-overwrite-reparent, inv-renam,

Used from specification aubifs-internal-asm

• aubifs-internal-asm/inv-gc is used by inv-gc,
• aubifs-internal-asm/inv-lookup is used by inv-truncate,