Used simplifier rules/spec theorems by specification

Used from specification abstract-file

• abstract-file/inj is used by fsync-pages-overwrite, fsync-pages-keep-abs, at-pcache-overwrite-other,
• abstract-file/elim is used by fsync-pages-overwrite, fsync-pages-others-unchanged, fsync-pages-keep-abs, fsync-pages-err, fsync-others-unchanged, fsync-keep-abs, fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs, fsync-inode-err, fsync-err, fsync-dirs, at-pcache-overwrite-other,
• abstract-file/inj is used by fsync-pages-overwrite, fsync-pages-others-unchanged, fsync-pages-keep-abs, fsync-others-unchanged, fsync-keep-abs, fsync-inode-overwrite, fsync-inode-keep-abs,
• abstract-file/sel-01 is used by fsync-pages-overwrite, fsync-pages-others-unchanged, fsync-pages-keep-abs, fsync-others-unchanged, fsync-inode-overwrite, fsync-inode-keep-abs,
• abstract-file/sel-02 is used by fsync-pages-overwrite, fsync-pages-others-unchanged, fsync-others-unchanged, fsync-keep-abs, fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs,
• abstract-file/sel-06 is used by fsync-pages-overwrite, fsync-pages-others-unchanged, fsync-others-unchanged, fsync-inode-overwrite, fsync-inode-keep-abs,
• abstract-file/sel-07 is used by fsync-pages-overwrite, fsync-pages-others-unchanged, fsync-others-unchanged, fsync-inode-overwrite, fsync-inode-keep-abs,
• abstract-file/upd-04 is used by fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs, fsync-dirs,
• abstract-file/upd-05 is used by fsync-pages-overwrite, fsync-pages-others-unchanged, fsync-pages-keep-abs, fsync-pages-err,
• abstract-file/upd-06 is used by fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs, fsync-dirs,
• abstract-file/updsel-02 is used by fsync-pages-overwrite,
• abstract-file/updsel-04 is used by fsync-pages-overwrite,
• abstract-file/updsel-05 is used by fsync-pages-overwrite,
• abstract-file/updsel-08 is used by fsync-pages-overwrite,

Used from specification nat-basic

• nat-basic/a is used by fsync-pages-overwrite,
• nat-basic/c is used by fsync-pages-overwrite,
• nat-basic/f is used by fsync-pages-overwrite, fsync-pages-others-unchanged, fsync-pages-keep-abs, fsync-pages-err, fsync-dirs,
• nat-basic/ls-02 is used by fsync-pages-overwrite,
• nat-basic/neq-01 is used by fsync-pages-overwrite,
• nat-basic/ref is used by fsync-pages-overwrite,
• nat-basic/s-04 is used by fsync-pages-overwrite,
• nat-basic/zero-01 is used by fsync-pages-overwrite,

Used from specification afs-base

• afs-base/afs-cons-file-nlink is used by fsync-pages-overwrite, fsync-others-unchanged, fsync-keep-abs,
• afs-base/afs-cons-notfile is used by fsync-pages-overwrite,
• afs-base/afs-cons-pagesize is used by fsync-pages-overwrite,
• afs-base/at-upto is used by fsync-pages-overwrite,
• afs-base/getinode is used by fsync-pages-overwrite, fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs,
• afs-base/in-upto is used by fsync-pages-overwrite,
• afs-base/valid-dir-ino is used by fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs, fsync-inode-err, fsync-dirs,
• afs-base/valid-file-ino is used by fsync-pages-overwrite, fsync-pages-others-unchanged, fsync-pages-keep-abs, fsync-pages-err, fsync-others-unchanged, fsync-keep-abs, fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs, fsync-inode-err, fsync-err, fsync-dirs,
• afs-base/valid-ino is used by fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs,
• afs-base/valid-inode is used by fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs,

Used from specification cache-base

• cache-base/at-icache-overwrite is used by fsync-pages-keep-abs, fsync-others-unchanged, fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs, at-icache-overwrite-other,
• cache-base/at-icache-overwrite-no-file is used by fsync-pages-keep-abs, fsync-others-unchanged, fsync-inode-keep-abs, at-icache-overwrite-other,
• cache-base/at-icache-overwrite-not-cached is used by fsync-pages-keep-abs, fsync-others-unchanged, at-icache-overwrite-other,
• cache-base/at-overwrite-content-new is used by fsync-pages-overwrite, fsync-pages-others-unchanged, fsync-pages-keep-abs, at-pcache-overwrite-other,
• cache-base/at-overwrite-content-old is used by fsync-pages-overwrite, fsync-pages-others-unchanged, fsync-pages-keep-abs, at-pcache-overwrite-other,
• cache-base/icache-cons is used by fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs,
• cache-base/in-overwrite-content is used by fsync-pages-overwrite, fsync-pages-keep-abs,
• cache-base/pcache-cons is used by fsync-pages-overwrite,
• cache-base/at-icache-overwrite is used by fsync-pages-keep-abs, fsync-others-unchanged, fsync-inode-others-unchanged, fsync-inode-keep-abs, at-icache-overwrite-other,
• cache-base/at-icache-overwrite-no-file is used by fsync-pages-keep-abs, fsync-others-unchanged, fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs, at-icache-overwrite-other,
• cache-base/at-icache-overwrite-not-cached is used by fsync-pages-keep-abs, fsync-others-unchanged, fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs, at-icache-overwrite-other,
• cache-base/at-mkcontent is used by fsync-pages-overwrite, fsync-pages-others-unchanged, fsync-pages-keep-abs, at-pcache-overwrite-other,
• cache-base/at-overwrite-content-new is used by fsync-pages-overwrite, fsync-pages-others-unchanged, fsync-pages-keep-abs, at-pcache-overwrite-other, at-overwrite-content-cut,
• cache-base/at-overwrite-content-old is used by fsync-pages-others-unchanged, fsync-pages-keep-abs, at-pcache-overwrite-other, at-overwrite-content-old-cut,
• cache-base/at-pcache-overwrite is used by fsync-pages-overwrite, fsync-pages-others-unchanged, fsync-pages-keep-abs, fsync-others-unchanged, fsync-inode-keep-abs, at-pcache-overwrite-other,
• cache-base/in-icache-overwrite is used by fsync-pages-keep-abs, fsync-inode-keep-abs,
• cache-base/in-mkcontent is used by fsync-pages-overwrite, fsync-pages-others-unchanged, fsync-pages-keep-abs, at-pcache-overwrite-other,
• cache-base/in-overwrite-content is used by fsync-pages-overwrite, fsync-pages-others-unchanged, fsync-pages-keep-abs, at-pcache-overwrite-other,
• cache-base/in-pcache-overwrite is used by fsync-pages-keep-abs, fsync-inode-keep-abs,

Used from specification pcache-entry

• pcache-entry/elim is used by fsync-pages-overwrite, fsync-pages-others-unchanged, fsync-pages-keep-abs, fsync-pages-err, at-pcache-overwrite-other,
• pcache-entry/inj is used by fsync-pages-overwrite, fsync-pages-keep-abs, fsync-pages-err,
• pcache-entry/sel-01 is used by fsync-pages-overwrite, fsync-pages-others-unchanged, fsync-pages-keep-abs, at-pcache-overwrite-other,
• pcache-entry/sel-02 is used by fsync-pages-overwrite,

Used from specification key

• key/elim-02 is used by fsync-pages-overwrite,
• key/inj-02 is used by fsync-pages-others-unchanged, fsync-pages-keep-abs,
• key/sel-03 is used by fsync-pages-overwrite, at-pcache-overwrite-other,
• key/sel-05 is used by fsync-pages-overwrite,
• key/test-09 is used by fsync-pages-overwrite,

Used from specification store

• store/pcache/At-other is used by fsync-pages-overwrite, fsync-pages-others-unchanged,
• store/file-content/At-other is used by fsync-pages-overwrite, fsync-pages-keep-abs,
• store/file-content/k-Extension is used by fsync-pages-overwrite, fsync-pages-others-unchanged, fsync-pages-keep-abs, at-pcache-overwrite-other,
• store/icache/At-other is used by fsync-inode-keep-abs, at-icache-overwrite-other,
• store/pcache/At-other is used by fsync-pages-overwrite, fsync-pages-keep-abs, at-pcache-overwrite-other,
• store/file-content/At-other is used by fsync-pages-overwrite,
• store/file-content/At-same is used by fsync-pages-overwrite,
• store/pcache/At-same is used by fsync-pages-overwrite, fsync-pages-keep-abs, at-pcache-overwrite-other,
• store/icache/At-same is used by fsync-inode-keep-abs,
• store/file-content/In-insert is used by fsync-pages-overwrite, fsync-pages-keep-abs,
• store/pcache/In-insert is used by fsync-pages-others-unchanged, fsync-pages-keep-abs, at-pcache-overwrite-other,
• store/icache/in-neq is used by fsync-inode-keep-abs, at-icache-overwrite-other,
• store/file-content/in-neq is used by fsync-pages-overwrite,
• store/pcache/in-neq is used by fsync-pages-overwrite, fsync-pages-others-unchanged, fsync-pages-keep-abs, at-pcache-overwrite-other,
• store/icache/ins is used by fsync-inode-keep-abs,
• store/file-content/insin is used by fsync-pages-overwrite,
• store/pcache/insin is used by fsync-pages-overwrite, fsync-pages-keep-abs,
• store/icache/insin is used by fsync-inode-keep-abs,
• store/icache/notmemlookup is used by fsync-pages-keep-abs, fsync-others-unchanged, fsync-inode-others-unchanged, fsync-inode-keep-abs, at-icache-overwrite-other,
• store/file-content/notmemlookup is used by fsync-pages-overwrite, fsync-pages-keep-abs,
• store/pcache/notmemlookup is used by fsync-pages-overwrite, fsync-pages-others-unchanged, fsync-pages-keep-abs, fsync-pages-err, at-pcache-overwrite-other,

Used from specification nat

• nat/anti is used by fsync-pages-overwrite,
• nat/fle is used by fsync-pages-overwrite,
• nat/le-ls-simp is used by fsync-pages-overwrite,
• nat/lels is used by fsync-pages-overwrite, fsync-dirs,
• nat/ler is used by fsync-pages-overwrite,

Used from specification error-class

• error-class/efail is used by fsync-inode-err,
• error-class/esuccess is used by fsync-pages-overwrite, fsync-pages-others-unchanged, fsync-pages-keep-abs, fsync-pages-err, fsync-inode-overwrite,
• error-class/not-esuccess is used by fsync-pages-overwrite, fsync-pages-others-unchanged, fsync-pages-keep-abs, fsync-pages-err, fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs, fsync-inode-err, fsync-dirs,

Used from specification error

• error/disj-45 is used by fsync-inode-err, fsync-dirs,

Used from specification page

• page/page-size is used by fsync-pages-overwrite,

Used from specification abstract-dir

• abstract-dir/elim is used by fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs, fsync-inode-err, fsync-dirs,
• abstract-dir/upd-04 is used by fsync-dirs,

Used from specification nat-mult

• nat-mult/ls is used by fsync-pages-overwrite,
• nat-mult/mult-a is used by fsync-pages-overwrite,
• nat-mult/mult-c is used by fsync-pages-overwrite,

Used from specification icache-entry

• icache-entry/elim is used by fsync-pages-keep-abs, fsync-others-unchanged, fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs, fsync-inode-err, fsync-dirs, at-icache-overwrite-other,
• icache-entry/inj is used by fsync-others-unchanged, fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs, fsync-inode-err, fsync-dirs,
• icache-entry/sel-01 is used by fsync-pages-keep-abs, fsync-others-unchanged, fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs, at-icache-overwrite-other,
• icache-entry/sel-02 is used by fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs,
• icache-entry/upd-02 is used by fsync-inode-keep-abs,

Used from specification heap

• heap/file-heap/ext is used by fsync-pages-keep-abs, fsync-inode-keep-abs,
• heap/file-heap/at-write is used by fsync-pages-overwrite, fsync-pages-others-unchanged, fsync-pages-keep-abs, fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs, fsync-dirs,
• heap/file-heap/in-write is used by fsync-pages-overwrite, fsync-pages-others-unchanged, fsync-pages-keep-abs, fsync-inode-others-unchanged, fsync-inode-keep-abs,
• heap/file-heap/overwrite is used by fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs, fsync-dirs,

Used from specification inode

• inode/elim is used by fsync-pages-overwrite, fsync-pages-others-unchanged, fsync-pages-keep-abs, fsync-pages-err, fsync-others-unchanged, fsync-keep-abs, fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs, fsync-inode-err, fsync-err, fsync-dirs, at-icache-overwrite-other,
• inode/inj is used by fsync-pages-overwrite, fsync-others-unchanged, fsync-inode-overwrite, fsync-inode-keep-abs,
• inode/sel-01 is used by fsync-pages-overwrite, fsync-pages-others-unchanged, fsync-pages-keep-abs, fsync-pages-err, fsync-others-unchanged, fsync-keep-abs, fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs, fsync-err, fsync-dirs,
• inode/sel-02 is used by fsync-others-unchanged, fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs,
• inode/sel-03 is used by fsync-pages-keep-abs, fsync-others-unchanged, fsync-keep-abs, fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs, fsync-err, fsync-dirs, at-icache-overwrite-other,
• inode/sel-04 is used by fsync-others-unchanged, fsync-keep-abs, fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs, fsync-err, fsync-dirs,
• inode/sel-10 is used by fsync-others-unchanged, fsync-keep-abs, fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs, fsync-err, fsync-dirs,
• inode/sel-11 is used by fsync-pages-overwrite, fsync-pages-others-unchanged, fsync-others-unchanged, fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs, fsync-dirs,

Used from specification afs-pre

• afs-pre/pre-write-inode is used by fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs, fsync-inode-err, fsync-dirs,
• afs-pre/pre-writepage is used by fsync-pages-overwrite, fsync-pages-others-unchanged, fsync-pages-keep-abs, fsync-pages-err,
• afs-pre/valid-dir-inode is used by fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs, fsync-inode-err, fsync-dirs,
• afs-pre/valid-file-inode is used by fsync-pages-overwrite, fsync-others-unchanged, fsync-keep-abs, fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs, fsync-inode-err, fsync-err, fsync-dirs,
• afs-pre/valid-wb-inode is used by fsync-inode-overwrite, fsync-inode-others-unchanged, fsync-inode-keep-abs, fsync-inode-err, fsync-dirs,

Used from specification cache-asm

• cache-asm/fsync-pages-inv is used by fsync-others-unchanged, fsync-keep-abs,

Used from specification afs-asm

• afs-asm/inv-writepage is used by fsync-pages-overwrite,