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: |
|---|
| replay-log-non-adr | proved | all subs proved
| replaylog-keep-adr,
|
| replay-cons-strong-append | proved | all subs proved
| replay-log-write,
replay-safe-write,
replay-safe-one,
replay-safe-split,
replay-log-one,
replay-split,
replay,
replay-cons-strong,
|
| replaylog-keep-adr | proved | all subs proved
| replayone-keep-adr,
replay-log-rec,
replay-log-empty,
|
| replay-split | proved | all subs proved
| replay-log-split,
replay,
|
| replay-safe-gc-copy | proved | all subs proved
| orphans-cons-gc-one,
replay-one-update,
replay-safe-write,
replay-safe-rec,
replay-safe-empty,
|
| replay-log-gc-copy | proved | all subs proved
| orphans-cons-gc-one,
replay-one-update,
replay-log-write,
replay-log-rec,
replay-log-empty,
|
| replay-cons-strong-variant1 | proved | all subs proved
| replay-cons-strong,
replay-cons-strong-safe,
replay,
|
| replayone-keep-adr | proved | all subs proved
| replay-trunc,
replay-data,
replay-dentry,
replay-ino,
|
| replay-log-split | proved | all subs proved
| replay-log-rec,
replay-log-empty,
|
| replay-one-update | proved | all subs proved
| replay-orphans-dentry,
replay-dentry,
replay-drop-data,
replay-orphans-data,
replay-data,
replay-orphans-inode,
orphans-cons,
replay-ino,
|
| orphans-cons-gc-one | proved | all subs proved
| orphans-cons,
|
| replay-cons-strong-safe | proved | all subs proved
| replay-cons-strong,
|
| replay-log-one | proved | all subs proved
| replay-log-empty,
replay-log-rec,
|
| replay-safe-split | proved | all subs proved
| replay-log-rec,
replay-safe-rec,
replay-log-empty,
replay-safe-empty,
|
| replay-safe-one | proved | all subs proved
| replay-safe-empty,
replay-safe-rec,
|
| replay-safe-write | proved | all subs proved
| replay-safe-rec,
replay-safe-empty,
|
| replay-log-write | proved | all subs proved
| replay-log-rec,
replay-log-empty,
|
| replay-safe-rec-variant1 | proved | all subs proved
| replay-safe-rec,
|
| replay-safe-gc-drop | proved | all subs proved
| replay-safe-rec,
replay-safe-empty,
|
| replay-safe-gc-copy-old | proved | all subs proved
| replay-safe-rec,
replay-safe-empty,
|
| replay-safe-drop | proved | all subs proved
| replay-safe-rec,
replay-safe-empty,
|
| replay-log-gc-drop | proved | all subs proved
| replay-log-rec,
replay-log-empty,
|
| replay-log-gc-copy-old | proved | all subs proved
| replay-log-rec,
replay-log-empty,
|
| replay-log-drop | proved | all subs proved
| replay-log-rec,
replay-log-empty,
|
| replay-cons-strong-empty-log | proved | all subs proved
| replay-log-empty,
replay,
replay-safe-empty,
replay-cons-strong,
|
| replay-cons-add-page | proved | all subs proved
| replay,
replay-cons-strong,
|
| replay-cons-add-orphan | proved | all subs proved
| replay,
replay-cons-strong,
|
| repalyone-monotonic | proved | all subs proved
| replay-trunc,
replay-data,
replay-dentry,
replay-ino,
|
| orphans-cons-reduce | proved | all subs proved
| orphans-cons,
|
| replay-safe-rec | axiom | | |
| replay-orphans-inode | proved | all subs proved
| |
| replay-orphans-data | proved | all subs proved
| |
| replay-drop-data | proved | all subs proved
| |
| replay-orphans-dentry | proved | all subs proved
| |
| replay-log-rec | axiom | | |
| replay-safe-empty | axiom | | |
| replay-log-empty | axiom | | |
| replay-cons-strong | axiom | | |
| replay | axiom | | |
| replay-ino | axiom | | |
| replay-dentry | axiom | | |
| replay-data | axiom | | |
| replay-trunc | axiom | | |
| orphans-cons | axiom | | |