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: |
|---|
| meta-exsplit | proved | all subs proved
| meta-path,
meta-split,
expath,
|
| meta-split | proved | all subs proved
| path-trans,
meta-path,
|
| orphans-del-file | proved | all subs proved
| valid-ino,
orphans,
afs-cons-notfile,
afs-cons-links-empty,
afs-cons-file-nlink,
|
| orphans-del-dir | proved | all subs proved
| links-deldir,
valid-ino,
orphans,
afs-cons-notfile,
afs-cons-links-empty,
afs-cons-dir-nlink,
|
| expath-prefix | proved | all subs proved
| path-prefix,
expath,
|
| expath-append | proved | all subs proved
| isexpath,
expath-split,
|
| afs-cons-nlink0-empty | proved | all subs proved
| valid-pagesize,
valid-ino,
dir-empty,
afs-cons,
afs-cons-dir-nlink,
afs-cons-notfile,
afs-cons-links-empty,
|
| afs-cons-links-rmorphans | proved | all subs proved
| valid-pagesize,
dir-empty,
afs-cons,
valid-ino,
afs-cons-notfile,
afs-cons-links-empty,
orphans,
afs-cons-dir-nlink,
links,
|
| meta-path | proved | all subs proved
| lookup-dir,
path-in-dirs,
lookup-file,
path-in-end,
expath-eps,
path-lookup,
isexpath,
meta,
|
| path-prefix | proved | all subs proved
| path-expath-prefix,
|
| expath-split | proved | all subs proved
| path-trans,
isexpath,
path-split,
expath,
|
| afs-cons-links-empty | proved | all subs proved
| afs-cons-notfile,
afs-cons-file-nlink,
afs-cons-dir-nlink,
afs-cons-nlink0-notin,
|
| expath-split-given | proved | all subs proved
| path-trans,
isexpath,
path-in-dirs,
path-in-end,
expath-eps,
path-inj,
path-split,
expath,
|
| path-expath-prefix | proved | all subs proved
| isexpath,
path-split,
|
| path-lookup | proved | all subs proved
| lookup-rec,
valid-dir-ino,
path-rec,
lookup-file,
lookup-dir,
valid-ino,
path-here,
|
| path-trans | proved | all subs proved
| path-split,
|
| afs-cons-nlink0-notin | proved | all subs proved
| afs-cons-in-next,
links-nonempty,
links,
|
| subdirs-del | proved | all subs proved
| subdirs-del-mod-size,
|
| path-split-one | proved | all subs proved
| path-inj,
path-one,
path-split,
|
| path-links-empty | proved | all subs proved
| links-nonempty,
path-one,
path-split,
path-in-dirs,
valid-ino,
path-here,
|
| meta-file | proved | all subs proved
| lookup-file,
expath-eps,
meta,
|
| links-modmeta-write3 | proved | all subs proved
| links-modmeta-write2,
|
| links-delsame | proved | all subs proved
| links-delsame-mod-subdirs,
|
| links-delother | proved | all subs proved
| links-delother-subdirs,
|
| afs-cons-size-at-upto | proved | all subs proved
| afs-cons-pagesize,
at-upto,
|
| subdirs-del-mod-size | proved | all subs proved
| subdirs,
subdirs-del-entry,
|
| lookup-file | proved | all subs proved
| lookup-dir,
valid-ino,
lookup-here,
|
| links-modmeta-write2 | proved | all subs proved
| links-modmeta,
|
| links-delsame-mod-subdirs | proved | all subs proved
| links,
links-modmeta,
links-del-entry,
|
| links-delother-subdirs | proved | all subs proved
| links-modmeta,
links-del-entry,
|
| path-split | proved | all subs proved
| valid-dir-ino,
path-rec,
path-in-start,
valid-ino,
path-here,
|
| afs-cons-pagesize | proved | all subs proved
| valid-pagesize,
valid-ino,
dir-empty,
afs-cons,
afs-cons-file-nlink,
|
| afs-cons-in-next | proved | all subs proved
| valid-pagesize,
valid-ino,
dir-empty,
afs-cons,
afs-cons-dir-nlink,
afs-cons-notfile,
|
| subdirs-put | proved | all subs proved
| subdirs,
subdirs-add-entry,
|
| subdirs-delete-orphans | proved | all subs proved
| links-nonempty,
orphans,
subdirs,
|
| path-uni-com | proved | all subs proved
| path-uni,
|
| path-file | proved | all subs proved
| afs-cons-notfile,
path-in-dirs,
valid-ino,
path-here,
|
| meta-dir | proved | all subs proved
| lookup-dir,
expath-eps,
meta,
|
| links-putsame | proved | all subs proved
| links-modmeta,
links-add-entry,
|
| links-putother | proved | all subs proved
| links-modmeta,
links-add-entry,
|
| links-put-same-entries | proved | all subs proved
| links-modmeta,
|
| expath-rec | proved | all subs proved
| isexpath,
path-rec,
expath,
valid-dir-ino,
|
| expath-one | proved | all subs proved
| path-one,
expath,
|
| afs-cons-non0 | proved | all subs proved
| valid-pagesize,
valid-ino,
dir-empty,
afs-cons,
afs-cons-dir-nlink,
|
| subdirs-add-entry | proved | all subs proved
| subdirs,
|
| subdirs-del-entry | proved | all subs proved
| subdirs,
|
| path-uni | proved | all subs proved
| valid-dir-ino,
path-rec,
valid-ino,
path-here,
|
| path-in-start | proved | all subs proved
| valid-dir-ino,
path-rec,
valid-ino,
path-here,
|
| links-deldir | proved | all subs proved
| links,
|
| lookup-dir | proved | all subs proved
| valid-ino,
lookup-here,
|
| links-add-entry | proved | all subs proved
| links,
|
| links-del-entry | proved | all subs proved
| links,
|
| links-modmeta | proved | all subs proved
| links,
|
| path-inj | proved | all subs proved
| valid-dir-ino,
path-rec,
valid-ino,
path-here,
|
| expath-eps | proved | all subs proved
| valid-ino,
path-here,
expath,
|
| path-in-end | proved | all subs proved
| valid-dir-ino,
path-rec,
valid-ino,
path-here,
|
| path-in-dirs | proved | all subs proved
| valid-dir-ino,
path-rec,
|
| path-one | proved | all subs proved
| valid-ino,
path-here,
valid-dir-ino,
path-rec,
|
| isexpath | proved | all subs proved
| expath,
|
| links-nonempty | proved | all subs proved
| links,
|
| afs-cons-file-nlink | proved | all subs proved
| valid-pagesize,
valid-ino,
dir-empty,
afs-cons,
|
| afs-cons-notfile | proved | all subs proved
| valid-pagesize,
valid-ino,
dir-empty,
afs-cons,
|
| afs-cons-dir-nlink | proved | all subs proved
| valid-pagesize,
valid-ino,
dir-empty,
afs-cons,
|
| upto-same | proved | all subs proved
| at-upto,
in-upto,
valid-content,
|
| upto-less | proved | all subs proved
| at-upto,
in-upto,
|
| upto-idem | proved | all subs proved
| at-upto,
in-upto,
|
| subdirs-write | proved | all subs proved
| subdirs,
|
| subdirs-putother | proved | all subs proved
| subdirs,
|
| subdirs-modmeta | proved | all subs proved
| subdirs,
|
| subdirs-inc-size | proved | all subs proved
| subdirs,
|
| subdirs-dec-size | proved | all subs proved
| subdirs,
|
| subdirs-alloc | proved | all subs proved
| subdirs,
|
| root-not-orphan | proved | all subs proved
| orphans,
|
| new-exists | proved | all subs proved
| max-exists,
|
| links-putnew | proved | all subs proved
| links,
|
| links-inc-nsubdirs | proved | all subs proved
| links,
|
| links-dirs-union | proved | all subs proved
| links,
|
| links-dec-nsubdirs | proved | all subs proved
| links,
|
| link-mod-dir-meta | proved | all subs proved
| links,
|
| empty-upto | proved | all subs proved
| in-upto,
|
| afs-cons-root-notfile | proved | all subs proved
| valid-pagesize,
valid-ino,
dir-empty,
afs-cons,
|
| afs-cons-root-dir | proved | all subs proved
| afs-cons,
|
| afs-cons-init | proved | all subs proved
| subdirs,
links,
afs-cons,
|
| valid-content | axiom | | |
| lookup-rec | axiom | | |
| max-exists | proved | all subs proved
| |
| meta | axiom | | |
| lookup-here | axiom | | |
| valid-dir-ino | axiom | | |
| path-rec | axiom | | |
| expath | axiom | | |
| path-here | axiom | | |
| in-upto | axiom | | |
| at-upto | axiom | | |
| orphans | axiom | | |
| links | axiom | | |
| subdirs | axiom | | |
| afs-cons | axiom | | |
| dir-empty | axiom | | |
| valid-ino | axiom | | |
| valid-pagesize | axiom | | |