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
| renam,
rename-root,
rename-fids,
|
| rename-fids | proved | all subs proved
| fids-cons-reduce,
renam,
|
| rename-root | proved | all subs proved
| renam,
|
| inv-sync | proved | all subs proved
| sync,
|
| inv-fsync | proved | all subs proved
| fsync,
|
| inv-fsyncdir | proved | all subs proved
| fsyncdir,
|
| crash-neutral-sync | proved | all subs proved
| sync,
|
| crash-neutral-fsync | proved | all subs proved
| fsync,
|
| crash-neutral-fsyncdir | proved | all subs proved
| fsyncdir,
|
| crash-neutral-recover | proved | all subs proved
| recover,
|
| crash-neutral-mkdir | proved | all subs proved
| mkdir,
|
| crash-neutral-rmdir | proved | all subs proved
| rmdir,
|
| crash-neutral-create | proved | all subs proved
| create,
|
| crash-neutral-open | proved | all subs proved
| open,
|
| crash-neutral-close | proved | all subs proved
| close,
|
| crash-neutral-read | proved | all subs proved
| read,
|
| crash-neutral-write | proved | all subs proved
| write,
|
| crash-neutral-seek | proved | all subs proved
| seek,
|
| crash-neutral-renam | proved | all subs proved
| renam,
|
| crash-neutral-link | proved | all subs proved
| link,
|
| crash-neutral-unlink | proved | all subs proved
| unlink,
|
| crash-neutral-truncate | proved | all subs proved
| truncate,
|
| crash-neutral-readmeta | proved | all subs proved
| readmeta,
|
| crash-neutral-writemeta | proved | all subs proved
| writemeta,
|
| crash-neutral-readdir | proved | all subs proved
| readdir,
|
| inv-recover | proved | all subs proved
| fids-cons-reduce,
recover,
|
| inv-mkdir | proved | all subs proved
| fids-cons-reduce,
mkdir,
|
| inv-rmdir | proved | all subs proved
| fids-cons-reduce,
rmdir,
|
| inv-create | proved | all subs proved
| fids-cons-reduce,
create,
|
| inv-open | proved | all subs proved
| fids-cons-reduce,
open,
|
| inv-close | proved | all subs proved
| fid-in-fs,
fids-cons-reduce,
close,
|
| inv-read | proved | all subs proved
| fid-in-fs,
fids-cons-reduce,
read,
|
| inv-write | proved | all subs proved
| fid-in-fs,
fids-cons-reduce,
write,
|
| inv-seek | proved | all subs proved
| fid-in-fs,
fids-cons-reduce,
seek,
|
| inv-link | proved | all subs proved
| fids-cons-reduce,
link,
|
| inv-unlink | proved | all subs proved
| fids-cons-reduce,
unlink,
|
| inv-truncate | proved | all subs proved
| fids-cons-reduce,
truncate,
|
| inv-readmeta | proved | all subs proved
| readmeta,
|
| inv-writemeta | proved | all subs proved
| fids-cons-reduce,
writemeta,
|
| inv-readdir | proved | all subs proved
| readdir,
|
| inv-format | proved | all subs proved
| format,
|
| sync | axiom | | |
| fsync | axiom | | |
| fsyncdir | axiom | | |
| recover | axiom | | |
| mkdir | axiom | | |
| rmdir | axiom | | |
| create | axiom | | |
| open | axiom | | |
| close | axiom | | |
| read | axiom | | |
| write | axiom | | |
| seek | axiom | | |
| fid-in-fs | proved | all subs proved
| |
| renam | axiom | | |
| link | axiom | | |
| unlink | axiom | | |
| truncate | axiom | | |
| readmeta | axiom | | |
| writemeta | axiom | | |
| fids-cons-reduce | proved | all subs proved
| |
| readdir | axiom | | |
| format | axiom | | |