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: |
|---|
| leb-size-aligned-node-header | proved | all subs proved
| nodeheader-notzero,
leb-size-aligned-2-node-header,
|
| is-aligned-pagesize-imp-headersize | proved | all subs proved
| nodeheader-notzero,
is-aligned-pagesize-imp-2headersize,
|
| is-aligned-nodeheadersize-mod-pagesize | proved | all subs proved
| nodeheader-notzero,
page-size-aligned-node-header,
|
| leb-size-aligned-2-node-header | proved | all subs proved
| nodeheader-notzero,
nodeheader-pagesize,
|
| is-aligned-pagesize-imp-2headersize | proved | all subs proved
| nodeheader-pagesize,
nodeheader-notzero,
|
| page-size-aligned-node-header | proved | all subs proved
| nodeheader-notzero,
nodeheader-pagesize,
|
| validtrailer-neq-empty | proved | all subs proved
| validtrailer-not-empty,
validtrailer-size,
|
| validtrailer-neq-0 | proved | all subs proved
| nodeheader-notzero,
validtrailer-size,
|
| node-header-size-ls-2-node-header-size | proved | all subs proved
| nodeheader-notzero,
|
| node-header-size-add-eq-0 | proved | all subs proved
| nodeheader-notzero,
|
| headersize2-mod-pagesize-is-0 | proved | all subs proved
| nodeheader-notzero,
nodeheader-pagesize,
|
| 2-node-header-size-add-eq-0 | proved | all subs proved
| nodeheader-notzero,
|
| validtrailer-not-empty | axiom | | |
| validtrailer-size | axiom | | |
| nodeheader-pagesize | axiom | | |
| nodeheader-notzero | axiom | | |