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: |
|---|
| crash-neutral-recovery | proved | all subs proved
| recovery,
|
| inv-get-page-size | proved | all subs proved
| get-page-size,
|
| inv-get-leb-size | proved | all subs proved
| get-leb-size,
|
| crash-neutral-get-page-size | proved | all subs proved
| get-page-size,
|
| crash-neutral-get-leb-size | proved | all subs proved
| get-leb-size,
|
| inv-recovery | proved | all subs proved
| recovery,
|
| crash-neutral-get-blockcount | proved | all subs proved
| get-blockcount,
|
| crash-neutral-isbad | proved | all subs proved
| isbad,
|
| crash-neutral-markbad | proved | all subs proved
| markbad,
|
| crash-neutral-sync-erase | proved | all subs proved
| sync-erase,
|
| crash-neutral-write-data-wl | proved | all subs proved
| write-data-wl,
|
| crash-neutral-write-data | proved | all subs proved
| write-data,
|
| crash-neutral-read-data | proved | all subs proved
| read-data,
|
| crash-neutral-write-vidhdr | proved | all subs proved
| write-vidhdr,
|
| crash-neutral-read-vidhdr | proved | all subs proved
| read-vidhdr,
|
| crash-neutral-write-echdr | proved | all subs proved
| write-echdr,
|
| crash-neutral-read-echdr | proved | all subs proved
| read-echdr,
|
| inv-get-blockcount | proved | all subs proved
| get-blockcount,
|
| inv-isbad | proved | all subs proved
| isbad,
|
| inv-markbad | proved | all subs proved
| markbad,
|
| inv-sync-erase | proved | all subs proved
| sync-erase,
|
| inv-write-data-wl | proved | all subs proved
| write-data-wl,
|
| inv-write-data | proved | all subs proved
| write-data,
|
| inv-read-data | proved | all subs proved
| read-data,
|
| inv-write-vidhdr | proved | all subs proved
| write-vidhdr,
|
| inv-read-vidhdr | proved | all subs proved
| read-vidhdr,
|
| inv-write-echdr | proved | all subs proved
| write-echdr,
|
| inv-read-echdr | proved | all subs proved
| read-echdr,
|
| inv-format | proved | all subs proved
| format,
|
| get-page-size | axiom | | |
| get-leb-size | axiom | | |
| recovery | axiom | | |
| get-blockcount | axiom | | |
| isbad | axiom | | |
| markbad | axiom | | |
| sync-erase | axiom | | |
| write-data-wl | axiom | | |
| write-data | axiom | | |
| read-data | axiom | | |
| write-vidhdr | axiom | | |
| read-vidhdr | axiom | | |
| write-echdr | axiom | | |
| read-echdr | axiom | | |
| format | axiom | | |