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: |
|---|
| refine-renam | proved | all subs proved
| rename-precond-abs,
refine-rename-new-keep-parent,
refine-rename-overwrite-keep-parent,
refine-rename-new-reparent,
refine-rename-overwrite-reparent,
|
| refine-rename-overwrite-reparent | proved | all subs proved
| refine-rename-overwrite-reparent-file,
refine-rename-overwrite-reparent-dir,
|
| refine-rename-overwrite-keep-parent | proved | all subs proved
| refine-rename-overwrite-keep-parent-different,
refine-rename-overwrite-keep-parent-identity,
|
| refine-rename-overwrite-reparent-dir | proved | all subs proved
| in-ri-dentry-inode,
in-insert,
mkdir-inj,
at-ri,
rename-precond-abs,
|
| refine-rename-overwrite-reparent-file | proved | all subs proved
| in-ri-dentry-inode,
in-insert,
mkdir-inj,
at-ri,
rename-precond-abs,
|
| refine-rename-overwrite-keep-parent-identity | proved | all subs proved
| in-ri-dentry-inode,
in-insert,
mkdir-inj,
at-ri,
rename-precond-abs,
|
| refine-rename-overwrite-keep-parent-different | proved | all subs proved
| in-insert,
in-ri-dentry-inode,
mkdir-inj,
at-ri,
rename-precond-abs,
|
| refine-rename-new-reparent | proved | all subs proved
| in-ri-dentry-inode,
in-insert,
mkdir-inj,
at-ri,
rename-precond-abs,
|
| refine-rename-new-keep-parent | proved | all subs proved
| in-ri-dentry-inode,
in-insert,
mkdir-inj,
at-ri,
rename-precond-abs,
|
| rename-precond-abs | proved | all subs proved
| afs-cons-abs-dir-subdirs,
afs-cons-abs-dir-size,
|
| recovery | proved | all subs proved
| mkdir-inj,
|
| refine-write-inode | proved | all subs proved
| in-ri-dentry-inode,
mkdir-inj,
at-ri,
|
| refine-truncate | proved | all subs proved
| log-cons-2,
mkdir-inj,
at-ri,
|
| refine-evict | proved | all subs proved
| mkdir-inj,
|
| refine-writepage | proved | all subs proved
| mkdir-inj,
at-ri,
|
| refine-link | proved | all subs proved
| in-ri-dentry-inode,
in-insert,
mkdir-inj,
at-ri,
valid-parent-ino-precond,
|
| refine-rmdir | proved | all subs proved
| in-ri-dentry-inode,
mkdir-inj,
at-ri,
afs-cons-abs-dir-size,
afs-cons-abs-dir-subdirs,
valid-parent-ino-precond,
|
| refine-mkdir | proved | all subs proved
| in-insert,
in-ri-inode-dentry,
in-ri-dentry-inode,
mkdir-inj,
at-ri,
valid-parent-ino-precond,
|
| refine-unlink | proved | all subs proved
| in-ri-dentry-inode,
mkdir-inj,
at-ri,
afs-cons-abs-dir-size,
valid-parent-ino-precond,
|
| refine-create | proved | all subs proved
| in-ri-dentry-inode,
in-insert,
mkdir-inj,
at-ri,
valid-parent-ino-precond,
|
| refine-lookup | proved | all subs proved
| valid-parent-ino-precond,
|
| initialization | proved | all subs proved
| in-ri-dentry-inode,
mkdir-inj,
at-ri,
|
| log-cons-2 | proved | all subs proved
| |
| afs-cons-abs-dir-subdirs | proved | all subs proved
| |
| in-ri-inode-dentry | proved | all subs proved
| |
| afs-cons-abs-dir-size | proved | all subs proved
| |
| in-insert | proved | all subs proved
| |
| valid-parent-ino-precond | proved | all subs proved
| |
| at-ri | proved | all subs proved
| |
| mkdir-inj | proved | all subs proved
| |
| in-ri-dentry-inode | proved | all subs proved
| |