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-replay | proved | all subs proved
| elim-data,
at-diff-ri,
replay-prog,
|
| replay-prog | proved | all subs proved
| replaylog-prog,
replayorphans-prepost,
replay,
|
| inv-renam | proved | all subs proved
| inv-rename-new-keep-parent,
inv-rename-overwrite-keep-parent,
inv-rename-new-reparent,
inv-rename-overwrite-reparent,
renam,
|
| replaylog-prog | proved | all subs proved
| replayone-prog,
replaylog,
|
| inv-rename-overwrite-reparent | proved | all subs proved
| data-ubifs-cons,
elim-data,
ubifs-cons-dentry-target-not-in-orphans,
dentry-ubifs-cons,
elim-dentry,
inode-ubifs-cons,
elim-inode,
at-del-ri,
at-ri,
in-ri,
ubifs-cons-reduce,
at-fs,
rename-overwrite-reparent,
|
| inv-rename-new-reparent | proved | all subs proved
| inode-ubifs-cons,
data-ubifs-cons,
elim-data,
dentry-ubifs-cons,
elim-dentry,
ubifs-cons-dentry-target-not-in-orphans,
at-del-ri,
at-ri,
in-ri,
ubifs-cons-reduce,
at-fs,
rename-new-reparent,
|
| inv-rename-overwrite-keep-parent | proved | all subs proved
| data-notin-other2,
data-notin-other1,
data-ubifs-cons,
elim-data,
ubifs-cons-dentry-target-not-in-orphans,
dentry-ubifs-cons,
elim-dentry,
inode-ubifs-cons,
elim-inode,
at-del-ri,
at-ri,
in-ri,
ubifs-cons-reduce,
at-fs,
rename-overwrite-keep-parent,
|
| inv-rename-new-keep-parent | proved | all subs proved
| inode-ubifs-cons,
data-ubifs-cons,
elim-data,
dentry-ubifs-cons,
elim-dentry,
ubifs-cons-dentry-target-not-in-orphans,
at-del-ri,
at-ri,
in-ri,
ubifs-cons-reduce,
at-fs,
rename-new-keep-parent,
|
| inv-check-commit | proved | all subs proved
| ubifs-cons-reduce,
check-commit,
|
| inv-create | proved | all subs proved
| inode-ubifs-cons,
data-ubifs-cons,
elim-data,
dentry-ubifs-cons,
elim-dentry,
at-ri,
in-ri,
ubifs-cons-reduce,
data-notin-other2,
data-notin-other1,
at-fs,
create,
|
| inv-mkdir | proved | all subs proved
| inode-ubifs-cons,
data-ubifs-cons,
elim-data,
dentry-ubifs-cons,
elim-dentry,
at-ri,
in-ri,
ubifs-cons-reduce,
data-notin-other2,
data-notin-other1,
at-fs,
mkdir,
|
| inv-unlink | proved | all subs proved
| inode-ubifs-cons,
ubifs-cons-dentry-target-not-in-orphans,
data-ubifs-cons,
elim-data,
dentry-ubifs-cons,
elim-dentry,
at-del-ri,
at-ri,
in-ri,
ubifs-cons-reduce,
data-notin-del2,
at-fs,
unlink,
|
| inv-rmdir | proved | all subs proved
| inode-ubifs-cons,
ubifs-cons-dentry-target-not-in-orphans,
data-ubifs-cons,
elim-data,
dentry-ubifs-cons,
elim-dentry,
at-del-ri,
at-ri,
in-ri,
ubifs-cons-reduce,
data-notin-del2,
at-fs,
rmdir,
|
| inv-link | proved | all subs proved
| inode-ubifs-cons,
data-ubifs-cons,
elim-data,
dentry-ubifs-cons,
elim-dentry,
at-ri,
in-ri,
ubifs-cons-reduce,
data-notin-other2,
data-notin-other1,
at-fs,
link,
|
| inv-writepage | proved | all subs proved
| data-ubifs-cons,
elim-data,
dentry-ubifs-cons,
elim-dentry,
inode-ubifs-cons,
elim-inode,
at-ri,
in-ri,
ubifs-cons-reduce,
at-fs,
writepage,
|
| inv-truncate | proved | all subs proved
| dentry-ubifs-cons,
elim-dentry,
elim-inode,
inode-ubifs-cons,
data-ubifs-cons,
elim-data,
at-ri,
at-diff-ri,
in-ri,
ubifs-cons-reduce,
data-notin-other1,
at-fs,
truncate,
|
| inv-write-inode | proved | all subs proved
| inode-ubifs-cons,
data-ubifs-cons,
elim-data,
dentry-ubifs-cons,
elim-dentry,
at-ri,
in-ri,
ubifs-cons-reduce,
at-fs,
write-inode,
|
| inv-evict | proved | all subs proved
| data-ubifs-cons,
ubifs-cons-reduce,
elim-data,
at-diff-ri,
at-del-ri,
evict,
|
| replayone-prog | proved | all subs proved
| elim-data,
elim-dentry,
elim-inode,
replayone,
|
| replayorphans-prepost | proved | all subs proved
| elim-inode,
elim-data,
at-del-ri,
at-diff-ri,
replayorphans,
|
| ubifs-cons-reduce | proved | all subs proved
| elim-data,
elim-dentry,
|
| inv-fsyncdir | proved | all subs proved
| fsyncdir,
|
| inv-fsync | proved | all subs proved
| fsync,
|
| inv-sync | proved | all subs proved
| sync,
|
| inv-iget | proved | all subs proved
| inode-ubifs-cons,
iget-check,
iget,
|
| inv-lookup | proved | all subs proved
| dentry-ubifs-cons,
lookup,
|
| inv-readpage | proved | all subs proved
| data-ubifs-cons,
readpage,
|
| inv-readdir | proved | all subs proved
| readdir,
|
| inv-format | proved | all subs proved
| at-ri,
in-ri,
at-fs,
format,
|
| inv-gc | proved | all subs proved
| gc,
|
| replayorphans | axiom | | |
| replayone | axiom | | |
| replaylog | axiom | | |
| replay | axiom | | |
| rename-overwrite-keep-parent | axiom | | |
| rename-new-reparent | axiom | | |
| rename-new-keep-parent | axiom | | |
| rename-overwrite-reparent | axiom | | |
| fsyncdir | axiom | | |
| fsync | axiom | | |
| sync | axiom | | |
| check-commit | axiom | | |
| iget | axiom | | |
| iget-check | axiom | | |
| lookup | axiom | | |
| create | axiom | | |
| mkdir | axiom | | |
| unlink | axiom | | |
| rmdir | axiom | | |
| data-notin-del2 | proved | all subs proved
| |
| ubifs-cons-dentry-target-not-in-orphans | proved | all subs proved
| |
| link | axiom | | |
| data-notin-other2 | proved | all subs proved
| |
| renam | axiom | | |
| readpage | axiom | | |
| writepage | axiom | | |
| readdir | axiom | | |
| truncate | axiom | | |
| data-notin-other1 | proved | all subs proved
| |
| elim-inode | proved | all subs proved
| |
| write-inode | axiom | | |
| elim-dentry | proved | all subs proved
| |
| dentry-ubifs-cons | proved | all subs proved
| |
| inode-ubifs-cons | proved | all subs proved
| |
| evict | axiom | | |
| at-del-ri | proved | all subs proved
| |
| at-diff-ri | proved | all subs proved
| |
| elim-data | proved | all subs proved
| |
| data-ubifs-cons | proved | all subs proved
| |
| format | axiom | | |
| at-fs | proved | all subs proved
| |
| in-ri | proved | all subs proved
| |
| at-ri | proved | all subs proved
| |
| gc | axiom | | |