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