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-renam | proved | all subs proved
| afs-cons-rename-dentry,
afs-cons-rename-negdentry,
|
| afs-cons-rename-negdentry | proved | all subs proved
| afs-cons-rename-file-negdentry,
afs-cons-rename-dir-negdentry,
|
| afs-cons-rename-dentry | proved | all subs proved
| afs-cons-rename-file-dentry,
afs-cons-rename-dir-dentry,
|
| afs-cons-rename-dir-negdentry | proved | all subs proved
| lastlink-rename,
Del-at-entries,
afs-cons-reduce,
internal-inode-sync,
renam,
|
| afs-cons-rename-dir-dentry | proved | all subs proved
| lastlink-rename,
lastlink-move,
Del-at-entries,
afs-cons-reduce,
internal-inode-sync,
drop-nlink,
renam,
|
| inv-create | proved | all subs proved
| New-same,
create-ino,
internal-inode-sync,
afs-cons-inode-sync,
afs-cons-create-ino,
create,
|
| inv-unlink | proved | all subs proved
| internal-inode-sync,
afs-cons-reduce,
afs-cons-inode-sync,
drop-nlink,
unlink,
|
| inv-mkdir | proved | all subs proved
| internal-inode-sync,
afs-cons-inode-sync,
mkdir-ino,
afs-cons-mkdir-ino,
mkdir,
|
| inv-rmdir | proved | all subs proved
| internal-inode-sync,
lastlink-rename,
lastlink-move,
afs-cons-reduce,
afs-cons-inode-sync,
drop-nlink,
rmdir,
|
| inv-link | proved | all subs proved
| internal-inode-sync,
afs-cons-reduce,
afs-cons-inode-sync,
inc-nlink,
link,
|
| inv-truncate | proved | all subs proved
| internal-inode-sync,
afs-cons-reduce,
afs-cons-inode-sync,
truncate-internal,
truncate,
|
| afs-cons-rename-file-negdentry | proved | all subs proved
| Del-at-entries,
afs-cons-reduce,
internal-inode-sync,
renam,
|
| afs-cons-rename-file-dentry | proved | all subs proved
| Del-at-entries,
afs-cons-reduce,
internal-inode-sync,
drop-nlink,
renam,
|
| afs-cons-create-ino | proved | all subs proved
| New-same,
afs-cons-reduce,
create-ino,
|
| afs-cons-mkdir-ino | proved | all subs proved
| afs-cons-reduce,
mkdir-ino,
|
| lastlink-rename | proved | all subs proved
| lastlink-move,
|
| afs-cons-inode-sync | proved | all subs proved
| afs-cons-reduce,
internal-inode-sync,
|
| inv-crash | proved | all subs proved
| afs-cons-reduce,
|
| inv-fsyncdir | proved | all subs proved
| fsyncdir,
|
| crash-neutral-fsyncdir | proved | all subs proved
| fsyncdir,
|
| inv-fsync | proved | all subs proved
| fsync,
|
| crash-neutral-fsync | proved | all subs proved
| fsync,
|
| crash-neutral-recovery | proved | all subs proved
| recovery,
|
| inv-sync | proved | all subs proved
| sync,
|
| crash-neutral-sync | proved | all subs proved
| sync,
|
| inv-recovery | proved | all subs proved
| afs-cons-reduce,
recovery,
|
| crash-neutral-check-commit | proved | all subs proved
| check-commit,
|
| crash-neutral-lookup | proved | all subs proved
| lookup,
|
| crash-neutral-create | proved | all subs proved
| create,
|
| crash-neutral-unlink | proved | all subs proved
| internal-inode-sync,
drop-nlink,
unlink,
|
| crash-neutral-mkdir | proved | all subs proved
| mkdir,
|
| crash-neutral-rmdir | proved | all subs proved
| internal-inode-sync,
drop-nlink,
rmdir,
|
| crash-neutral-link | proved | all subs proved
| internal-inode-sync,
inc-nlink,
link,
|
| crash-neutral-renam | proved | all subs proved
| renam,
|
| crash-neutral-readpage | proved | all subs proved
| readpage,
|
| crash-neutral-writepage | proved | all subs proved
| writepage,
|
| crash-neutral-readdir | proved | all subs proved
| readdir,
|
| crash-neutral-evict | proved | all subs proved
| evict,
|
| crash-neutral-truncate | proved | all subs proved
| truncate-internal,
truncate,
|
| crash-neutral-iget | proved | all subs proved
| iget,
|
| crash-neutral-write_inode | proved | all subs proved
| write_inode,
|
| inv-check-commit | proved | all subs proved
| check-commit,
|
| inv-lookup | proved | all subs proved
| lookup,
|
| inv-readpage | proved | all subs proved
| readpage,
|
| inv-writepage | proved | all subs proved
| afs-cons-reduce,
writepage,
|
| inv-readdir | proved | all subs proved
| readdir,
|
| inv-evict | proved | all subs proved
| afs-cons-reduce,
evict,
|
| inv-iget | proved | all subs proved
| iget,
|
| inv-write_inode | proved | all subs proved
| afs-cons-reduce,
write_inode,
|
| inv-format | proved | all subs proved
| format,
|
| Del-at-entries | proved | all subs proved
| |
| fsyncdir | axiom | | |
| fsync | axiom | | |
| sync | axiom | | |
| recovery | axiom | | |
| renam | axiom | | |
| check-commit | axiom | | |
| lookup | axiom | | |
| create | axiom | | |
| create-ino | axiom | | |
| New-same | proved | all subs proved
| |
| unlink | axiom | | |
| mkdir | axiom | | |
| mkdir-ino | axiom | | |
| rmdir | axiom | | |
| drop-nlink | axiom | | |
| lastlink-move | proved | all subs proved
| |
| link | axiom | | |
| inc-nlink | axiom | | |
| readpage | axiom | | |
| writepage | axiom | | |
| readdir | axiom | | |
| evict | axiom | | |
| truncate | axiom | | |
| truncate-internal | axiom | | |
| internal-inode-sync | axiom | | |
| iget | axiom | | |
| write_inode | axiom | | |
| afs-cons-reduce | proved | all subs proved
| |
| format | axiom | | |