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-page-size | proved | all subs proved | page-size, |
| inv-peb-size | proved | all subs proved | peb-size, |
| crash-neutral-page-size | proved | all subs proved | page-size, |
| crash-neutral-peb-size | proved | all subs proved | peb-size, |
| crash-neutral-blockcount | proved | all subs proved | blockcount, |
| crash-neutral-markbad | proved | all subs proved | markbad, |
| crash-neutral-isbad | proved | all subs proved | isbad, |
| crash-neutral-write | proved | all subs proved | write, |
| crash-neutral-read | proved | all subs proved | read, |
| crash-neutral-erase | proved | all subs proved | erase, |
| inv-blockcount | proved | all subs proved | blockcount, |
| inv-markbad | proved | all subs proved | reduce-mtd-cons, markbad, |
| inv-isbad | proved | all subs proved | isbad, |
| inv-write | proved | all subs proved | reduce-mtd-cons, write, |
| inv-read | proved | all subs proved | read, |
| inv-erase | proved | all subs proved | reduce-mtd-cons, erase, |
| inv-crash | proved | all subs proved | reduce-mtd-cons, |
| inv-init | proved | all subs proved | init, |
| page-size | axiom | ||
| peb-size | axiom | ||
| blockcount | axiom | ||
| markbad | axiom | ||
| isbad | axiom | ||
| write | axiom | ||
| read | axiom | ||
| erase | axiom | ||
| reduce-mtd-cons | proved | all subs proved | |
| init | axiom |