[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 abstract-file

Used from specification pcache-entry

Used from specification key

key/inj-02 is used by pcache-overwrite-read-page, overwrite-write-page-dirty, overwrite-write-page-clean,

Used from specification store

store/file-content/At-other is used by overwrite-write-page-clean,
store/file-content/At-other-num is used by overwrite-write-page-clean,
store/file-content/Extension is used by pcache-overwrite-read-page, overwrite-write-page-dirty, overwrite-write-page-clean, overwrite-pcache-empty,
store/pcache/In-insert is used by pcache-overwrite-read-page, overwrite-write-page-dirty, overwrite-write-page-clean,
store/file-content/In-insert is used by overwrite-write-page-clean,
store/icache/At-in-out is used by synced-files-add-new-clean-inode, synced-dirs-add-new-clean-inode,
store/icache/At-other is used by synced-files-update-clean-inode, synced-files-add-new-clean-inode, synced-dirs-add-update-clean-inode, synced-dirs-add-new-clean-inode, overwrite-write-inode-dirty, overwrite-write-inode-clean-file, overwrite-write-inode-clean-dir,
store/pcache/At-other is used by pcache-overwrite-read-page, overwrite-write-page-dirty, overwrite-write-page-clean,
store/file-content/At-other is used by overwrite-write-page-dirty, overwrite-write-page-clean,
store/icache/At-same is used by synced-files-update-clean-inode, synced-files-add-new-clean-inode, synced-dirs-add-update-clean-inode, synced-dirs-add-new-clean-inode, overwrite-write-inode-dirty, overwrite-write-inode-clean-file, overwrite-write-inode-clean-dir,
store/pcache/At-same is used by pcache-overwrite-read-page, overwrite-write-page-dirty, overwrite-write-page-clean,
store/file-content/At-same is used by overwrite-write-page-dirty, overwrite-write-page-clean,
store/icache/In-empty is used by synced-files-empty, synced-dirs-empty, overwrite-icache-empty,
store/pcache/In-empty is used by synced-files-empty, synced-dirs-empty, overwrite-pcache-empty,
store/icache/In-insert is used by synced-files-add-new-clean-inode, synced-dirs-add-new-clean-inode, overwrite-write-inode-dirty, overwrite-write-inode-clean-file, overwrite-write-inode-clean-dir,
store/pcache/in-neq is used by pcache-overwrite-read-page, overwrite-write-page-dirty, overwrite-write-page-clean,
store/file-content/in-neq is used by overwrite-write-page-dirty, overwrite-write-page-clean,
store/icache/in-neq is used by synced-files-update-clean-inode, synced-files-add-new-clean-inode, synced-dirs-add-update-clean-inode, synced-dirs-add-new-clean-inode, overwrite-write-inode-dirty, overwrite-write-inode-clean-file, overwrite-write-inode-clean-dir,
store/icache/insin is used by synced-files-update-clean-inode, synced-files-add-new-clean-inode, synced-dirs-add-update-clean-inode, synced-dirs-add-new-clean-inode, overwrite-write-inode-dirty, overwrite-write-inode-clean-file, overwrite-write-inode-clean-dir,
store/pcache/insin is used by overwrite-write-page-dirty, overwrite-write-page-clean,
store/file-content/insin is used by overwrite-write-page-dirty, overwrite-write-page-clean,
store/icache/notmemlookup is used by synced-files-add-new-clean-inode, synced-dirs-add-new-clean-inode,
store/file-content/notmemlookup is used by overwrite-write-page-clean,
store/pcache/notmemlookup is used by synced-files-add-new-clean-inode, synced-dirs-add-new-clean-inode, pcache-overwrite-read-page, overwrite-write-page-dirty, overwrite-write-page-clean,

Used from specification heap

heap/file-heap/ext is used by pcache-overwrite-read-page, overwrite-write-page-dirty, overwrite-write-page-clean, overwrite-write-inode-dirty, overwrite-write-inode-clean-file, overwrite-write-inode-clean-dir, overwrite-pcache-empty, overwrite-icache-empty,
heap/file-heap/at-write is used by overwrite-write-page-dirty, overwrite-write-page-clean, overwrite-write-inode-dirty, overwrite-write-inode-clean-file,
heap/file-heap/in-write is used by overwrite-write-page-dirty, overwrite-write-page-clean, overwrite-write-inode-dirty, overwrite-write-inode-clean-file,

Used from specification icache-entry

Used from specification inode

inode/elim is used by overwrite-write-page-dirty, overwrite-write-page-clean, overwrite-write-inode-dirty, overwrite-write-inode-clean-file, overwrite-write-inode-clean-dir,
inode/inj is used by overwrite-write-inode-clean-dir,
inode/sel-02 is used by overwrite-write-inode-clean-file, overwrite-write-inode-clean-dir,
inode/sel-03 is used by overwrite-write-inode-dirty, overwrite-write-inode-clean-file, overwrite-write-inode-clean-dir,
inode/sel-04 is used by overwrite-write-inode-dirty, overwrite-write-inode-clean-file, overwrite-write-inode-clean-dir,
inode/sel-11 is used by overwrite-write-inode-clean-file, overwrite-write-inode-clean-dir,
inode/upd-02 is used by overwrite-write-inode-clean-file, overwrite-write-inode-clean-dir,
inode/upd-11 is used by overwrite-write-inode-clean-file,
inode/updsel-07 is used by overwrite-write-inode-dirty,
inode/updsel-12 is used by overwrite-write-inode-dirty,
inode/updsel-17 is used by overwrite-write-inode-dirty,
inode/updsel-29 is used by overwrite-write-inode-dirty,
inode/updsel-31 is used by overwrite-write-inode-dirty,
inode/updsel-33 is used by overwrite-write-inode-dirty,
inode/updsel-41 is used by overwrite-write-inode-dirty,