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-create | proved | all subs proved
| of-cons-reduce,
may-create,
walk-prepost-parent,
create,
|
| inv-mkdir | proved | all subs proved
| of-cons-reduce,
may-create,
walk-prepost-parent,
mkdir,
|
| inv-rmdir | proved | all subs proved
| put-inode,
of-cons-reduce,
inv-put-inode,
may-delete,
may-delete-check,
walk-prepost-parent,
rmdir,
|
| inv-unlink | proved | all subs proved
| put-inode,
of-cons-reduce,
inv-put-inode,
may-delete,
may-delete-check,
walk-prepost-parent,
unlink,
|
| inv-renam | proved | all subs proved
| may-create,
put-inode,
of-cons-reduce,
inv-put-inode,
may-delete-check,
may-lookup,
may-delete,
walk-prepost-parent,
renam,
|
| inv-link | proved | all subs proved
| of-cons-reduce,
may-create,
walk-prepost,
may-link,
walk-prepost-parent,
link,
|
| walk-prepost-parent | proved | all subs proved
| walk-prepost,
|
| inv-fsync | proved | all subs proved
| may-open,
walk-prepost,
fsync,
|
| inv-writemeta | proved | all subs proved
| of-cons-reduce,
walk-prepost,
writemeta,
|
| inv-open | proved | all subs proved
| of-cons-reduce,
may-open,
walk-prepost,
open,
|
| inv-truncate | proved | all subs proved
| of-cons-reduce,
may-open,
walk-prepost,
truncate,
|
| inv-readmeta | proved | all subs proved
| walk-prepost,
readmeta,
|
| inv-readdir | proved | all subs proved
| may-open,
walk-prepost,
readdir,
|
| inv-write | proved | all subs proved
| write-page,
write-block,
of-cons-reduce,
write-loop,
write,
write-term,
|
| walk-prepost | proved | all subs proved
| walk-prepost-h,
walk-term,
|
| write-term | proved | all subs proved
| write-loop-term,
write,
|
| inv-close | proved | all subs proved
| of-cons-reduce,
inv-put-inode,
close,
|
| inv-read | proved | all subs proved
| of-cons-reduce,
read-loop-term,
read,
|
| write-loop-term | proved | all subs proved
| write-page,
write-block,
write-loop,
|
| walk-term | proved | all subs proved
| may-lookup,
walk,
|
| walk-prepost-h | proved | all subs proved
| px-last,
may-lookup,
walk,
|
| inv-put-inode | proved | all subs proved
| of-cons-reduce,
put-inode,
|
| read-loop-term | proved | all subs proved
| read-block,
read-loop,
|
| write-loop-err | proved | all subs proved
| write-page,
write-block,
write-loop,
|
| write-loop-0 | proved | all subs proved
| write-page,
write-block,
write-loop,
|
| inv-sync | proved | all subs proved
| sync,
|
| inv-recover | proved | all subs proved
| of-cons-reduce,
recover,
|
| inv-seek | proved | all subs proved
| of-cons-reduce,
seek,
|
| inv-format | proved | all subs proved
| format,
|
| walk | axiom | | |
| px-last | proved | all subs proved
| |
| read-loop | axiom | | |
| read-block | axiom | | |
| fsync | axiom | | |
| sync | axiom | | |
| writemeta | axiom | | |
| recover | axiom | | |
| create | axiom | | |
| mkdir | axiom | | |
| rmdir | axiom | | |
| unlink | axiom | | |
| renam | axiom | | |
| may-delete | axiom | | |
| may-lookup | axiom | | |
| may-delete-check | axiom | | |
| put-inode | axiom | | |
| link | axiom | | |
| may-link | axiom | | |
| may-create | axiom | | |
| open | axiom | | |
| close | axiom | | |
| truncate | axiom | | |
| seek | axiom | | |
| readmeta | axiom | | |
| readdir | axiom | | |
| may-open | axiom | | |
| read | axiom | | |
| write | axiom | | |
| write-loop | axiom | | |
| of-cons-reduce | proved | all subs proved
| |
| write-block | axiom | | |
| write-page | axiom | | |
| format | axiom | | |