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-unlink | proved | all subs proved
| py-prefix,
ispath-target,
file-fid,
abs-fold-del,
abs-unfold,
fid-file,
of,
fid-ino-entry,
py-strong,
path-in-last,
dir-empty,
abs-acyclic,
dir-entry,
py-px,
py-last,
py-pw,
py,
make-abs-fold-work,
path-in-eq,
path-in,
|
| refine-link | proved | all subs proved
| px-prefix,
py-prefix,
ispath-target,
abs-fold-new,
fid-ino-entry,
abs-unfold,
py-strong,
path-in-last,
py-px,
py-last,
py-pw,
py,
dir-empty,
dir-entry,
px,
make-abs-fold-work,
path-in-eq,
path-in,
|
| refine-create | proved | all subs proved
| py-prefix,
ispath-target,
abs-fold-new,
abs-unfold,
py-strong,
dir-entry,
py-px,
py-last,
py-pw,
py,
make-abs-fold-work,
path-in,
path-in-eq,
|
| refine-rmdir | proved | all subs proved
| py-prefix,
ispath-target,
abs-fold-del,
abs-unfold-entry-p,
abs-unfold,
py-strong,
path-in-last,
dir-empty,
abs-acyclic,
dir-entry,
py-px,
py-last,
py-pw,
py,
make-abs-fold-work,
path-in-eq,
path-in,
|
| refine-mkdir | proved | all subs proved
| py-prefix,
ispath-target,
abs-fold-new-p,
abs-unfold,
py-strong,
path-in-last,
dir-entry,
py-px,
py-last,
py-pw,
py,
make-abs-fold-work,
path-in-eq,
path-in,
|
| py | proved | all subs proved
| pw,
px,
path-in-eq,
path-in,
|
| refine-fsync | proved | all subs proved
| px-prefix,
ispath-target,
pr,
path-in-eq,
path-in,
|
| refine-readdir | proved | all subs proved
| px-prefix,
ispath-target,
pr,
make-abs-fold-work,
path-in-eq,
path-in,
|
| refine-writemeta | proved | all subs proved
| px-prefix,
ispath-target,
fid-ino,
abs-unfold,
pw,
make-abs-fold-work,
path-in-eq,
path-in,
|
| refine-readmeta | proved | all subs proved
| px-prefix,
fid-file,
path-in-last,
ispath-target,
fid-ino,
of,
pr,
make-abs-fold-work,
path-in-eq,
path-in,
|
| refine-truncate | proved | all subs proved
| px-prefix,
ispath-target,
fid-ino,
pw,
path-in-eq,
path-in,
|
| refine-open | proved | all subs proved
| px-prefix,
ispath-target,
fid-ino,
pw,
pr,
path-in-eq,
path-in,
|
| pr | proved | all subs proved
| px-parent,
fid-file,
path-in-eq,
path-in,
|
| pw | proved | all subs proved
| px-parent,
fid-file,
path-in-eq,
path-in,
|
| px-parent | proved | all subs proved
| px,
ispath-target,
path-in-eq,
path-in,
|
| fid-ino-entry | proved | all subs proved
| path-in-eq,
dir-entry,
path-in,
make-abs-fold-work,
|
| px-prefix | proved | all subs proved
| px,
path-in-eq,
path-in,
|
| dir-empty | proved | all subs proved
| path-in-eq,
dir-entry,
path-in,
make-abs-fold-work,
|
| px | proved | all subs proved
| fid-file,
path-in-eq,
path-in,
|
| fid-ino | proved | all subs proved
| path-in-eq,
path-in,
|
| abs-acyclic | proved | all subs proved
| fid-file,
path-in-eq,
path-in,
make-abs-fold-work,
|
| dir-entry | proved | all subs proved
| path-in-eq,
path-in,
make-abs-fold-work,
|
| path-in-last | proved | all subs proved
| path-in,
path-in-eq,
|
| py-strong | proved | all subs proved
| py-px,
py-last,
py-pw,
path-in-eq,
path-in,
|
| abs-unfold | proved | all subs proved
| path-in,
path-in-eq,
make-abs-fold-work,
|
| py-prefix | proved | all subs proved
| fid-file,
path-in-eq,
path-in,
|
| path-in | proved | all subs proved
| fid-file,
path-in-eq,
|
| py-pw | proved | all subs proved
| py-px,
py-last,
|
| recovery | proved | all subs proved
| file-fid,
fid-file,
|
| refine-close | proved | all subs proved
| file-fid,
of,
|
| file-fid | proved | all subs proved
| fid-file,
|
| abs-fold-new | proved | all subs proved
| abs-fold-new-p,
|
| abs-fold-del | proved | all subs proved
| abs-fold-del-p,
|
| path-in-eq | proved | all subs proved
| fid-file,
|
| py-last | proved | all subs proved
| py-px,
|
| refine-write | proved | all subs proved
| files-del-eq,
|
| abs-fold-del-p | proved | all subs proved
| |
| fid-file | proved | all subs proved
| |
| files-del-eq | proved | all subs proved
| |
| of | proved | all subs proved
| |
| abs-unfold-entry-p | proved | all subs proved
| |
| make-abs-fold-work | proved | all subs proved
| |
| py-px | proved | all subs proved
| |
| abs-fold-new-p | proved | all subs proved
| |
| ispath-target | proved | all subs proved
| |