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

Lemma dependency for Specification cache-asm

A lemma (entry) may depend on lemmas (entries) below its position, but never on lemmas above its position. This means the list is a topological order of the dependency graph. An entry 'all subs proved' means that all used lemmas are (transitively) proved.

Name: Status: Subs proved? Used:
inv-renamprovedall subs proved inv-rename-dentry, inv-rename-negdentry,
inv-rename-negdentryprovedall subs proved inv-rename-file-negdentry, inv-rename-dir-negdentry,
inv-rename-dentryprovedall subs proved inv-rename-file-dentry, inv-rename-dir-dentry,
inv-fsyncprovedall subs proved fsync-inode-inv, fsync-pages-inv, fsync,
inv-truncateprovedall subs proved inv-truncate-buff-none-uncached, inv-truncate-buff-none-cached, inv-truncate-buff-some,
inv-rename-dir-negdentryprovedall subs proved renam,
inv-rename-file-negdentryprovedall subs proved renam,
inv-rename-dir-dentryprovedall subs proved renam,
inv-rename-file-dentryprovedall subs proved renam,
fsync-pages-invprovedall subs proved fsync-pages,
fsync-inode-invprovedall subs proved fsync-inode,
inv-truncate-buff-someprovedall subs proved truncate,
inv-truncate-buff-none-cachedprovedall subs proved truncate,
inv-truncate-buff-none-uncachedprovedall subs proved truncate,
inv-fsyncdirprovedall subs proved fsyncdir,
inv-formatprovedall subs proved format,
inv-syncprovedall subs proved sync,
inv-write_inodeprovedall subs proved write_inode,
inv-evictprovedall subs proved evict,
inv-readdirprovedall subs proved readdir,
inv-writepageprovedall subs proved writepage,
inv-readpageprovedall subs proved readpage,
inv-linkprovedall subs proved link,
inv-rmdirprovedall subs proved rmdir,
inv-mkdirprovedall subs proved mkdir,
inv-unlinkprovedall subs proved unlink,
inv-createprovedall subs proved create,
inv-lookupprovedall subs proved lookup,
inv-check-commitprovedall subs proved check-commit,
inv-recoverprovedall subs proved recover,
inv-igetprovedall subs proved iget,
truncateaxiom
renamaxiom
fsync-pagesaxiom
fsync-inodeaxiom
fsyncdiraxiom
fsyncaxiom
formataxiom
syncaxiom
write_inodeaxiom
evictaxiom
readdiraxiom
writepageaxiom
readpageaxiom
linkaxiom
rmdiraxiom
mkdiraxiom
unlinkaxiom
createaxiom
lookupaxiom
check-commitaxiom
recoveraxiom
igetaxiom