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-get-leb-size | proved | all subs proved
| get-leb-size,
|
| crash-neutral-get-leb-size | proved | all subs proved
| get-leb-size,
|
| crash-neutral-recovery | proved | all subs proved
| recovery,
|
| inv-is-log-empty | proved | all subs proved
| is-log-empty,
|
| crash-neutral-is-log-empty | proved | all subs proved
| is-log-empty,
|
| inv-format | proved | all subs proved
| format,
|
| inv-get-block-free-size | proved | all subs proved
| get-block-free-size,
|
| crash-neutral-get-block-free-size | proved | all subs proved
| get-block-free-size,
|
| inv-sync | proved | all subs proved
| sync,
|
| crash-neutral-sync | proved | all subs proved
| sync,
|
| inv-add-gnds | proved | all subs proved
| add-gnds,
|
| crash-neutral-add-gnds | proved | all subs proved
| add-gnds,
|
| crash-neutral-contains | proved | all subs proved
| contains,
|
| crash-neutral-lookup | proved | all subs proved
| lookup,
|
| crash-neutral-store | proved | all subs proved
| store,
|
| crash-neutral-remove | proved | all subs proved
| remove,
|
| crash-neutral-truncate | proved | all subs proved
| truncate,
|
| crash-neutral-entries | proved | all subs proved
| entries,
|
| crash-neutral-read-gnd | proved | all subs proved
| read-gnd,
|
| crash-neutral-read-gblock | proved | all subs proved
| read-gblock,
|
| crash-neutral-get-gc-block | proved | all subs proved
| get-gc-block,
|
| crash-neutral-set-gblock-refsize | proved | all subs proved
| set-gblock-refsize,
|
| crash-neutral-get-gblock-refsize | proved | all subs proved
| get-gblock-refsize,
|
| crash-neutral-allocate-gnd | proved | all subs proved
| allocate-gnd,
|
| crash-neutral-deallocate-gnd | proved | all subs proved
| deallocate-gnd,
|
| crash-neutral-commit | proved | all subs proved
| commit,
|
| crash-neutral-requires-commit | proved | all subs proved
| requires-commit,
|
| inv-recovery | proved | all subs proved
| recovery,
|
| inv-requires-commit | proved | all subs proved
| requires-commit,
|
| inv-commit | proved | all subs proved
| commit,
|
| inv-deallocate-gnd | proved | all subs proved
| deallocate-gnd,
|
| inv-allocate-gnd | proved | all subs proved
| allocate-gnd,
|
| inv-get-gblock-refsize | proved | all subs proved
| get-gblock-refsize,
|
| inv-set-gblock-refsize | proved | all subs proved
| set-gblock-refsize,
|
| inv-get-gc-block | proved | all subs proved
| get-gc-block,
|
| inv-read-gblock | proved | all subs proved
| read-gblock,
|
| inv-read-gnd | proved | all subs proved
| read-gnd,
|
| inv-entries | proved | all subs proved
| entries,
|
| inv-truncate | proved | all subs proved
| truncate,
|
| inv-remove | proved | all subs proved
| remove,
|
| inv-store | proved | all subs proved
| store,
|
| inv-lookup | proved | all subs proved
| lookup,
|
| inv-contains | proved | all subs proved
| contains,
|
| get-leb-size | axiom | | |
| is-log-empty | axiom | | |
| format | axiom | | |
| get-block-free-size | axiom | | |
| sync | axiom | | |
| add-gnds | axiom | | |
| recovery | axiom | | |
| requires-commit | axiom | | |
| commit | axiom | | |
| deallocate-gnd | axiom | | |
| allocate-gnd | axiom | | |
| get-gblock-refsize | axiom | | |
| set-gblock-refsize | axiom | | |
| get-gc-block | axiom | | |
| read-gblock | axiom | | |
| read-gnd | axiom | | |
| entries | axiom | | |
| truncate | axiom | | |
| remove | axiom | | |
| store | axiom | | |
| lookup | axiom | | |
| contains | axiom | | |