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: |
|---|
| lebs-write-last | proved | all subs proved
| lebs-write-above,
lebs-rec,
|
| lebs-write-above | proved | all subs proved
| lebs-write-below,
lebs-rec,
lebs-base,
|
| lebs-write-below | proved | all subs proved
| lebs-rec,
lebs-base,
|
| mapped-full-zero | proved | all subs proved
| mapped-full,
|
| mapped-full-write-below | proved | all subs proved
| mapped-full,
|
| mapped-full-write-above | proved | all subs proved
| mapped-full,
|
| mapped-full-range-eq | proved | all subs proved
| mapped-full,
|
| mapped-full-last | proved | all subs proved
| mapped-full,
|
| mapped-full-idexpt-below | proved | all subs proved
| mapped-full,
|
| mapped-full-aligndown-vol | proved | all subs proved
| mapped-full,
|
| lebs-size-mappedfull | proved | all subs proved
| lebs-rec,
lebs-base,
mapped-full,
|
| lebs-size | proved | all subs proved
| lebs-rec,
lebs-base,
|
| lebs-range-eq | proved | all subs proved
| lebs-rec,
lebs-base,
|
| lebs-idexpt-below | proved | all subs proved
| lebs-rec,
lebs-base,
|
| lebs-crash | proved | all subs proved
| lebs-rec,
lebs-base,
mapped-full,
|
| disk-layout-size-vol-orphans | proved | all subs proved
| sb-lpt,
sb-orph,
sb-log,
disk-layout,
|
| disk-layout-same-size | proved | all subs proved
| sb-lpt,
sb-orph,
sb-log,
disk-layout,
|
| disk-layout-orphans-below-main | proved | all subs proved
| sb-lpt,
sb-orph,
sb-log,
disk-layout,
|
| disk-layout-not1-unfold | proved | all subs proved
| sb-lpt,
sb-orph,
sb-log,
disk-layout,
|
| disk-layout-main-not-below-lpt | proved | all subs proved
| sb-lpt,
sb-orph,
sb-log,
disk-layout,
|
| disk-layout-lpt-below-main | proved | all subs proved
| sb-lpt,
sb-orph,
sb-log,
disk-layout,
|
| disk-layout-log-not-0 | proved | all subs proved
| sb-log,
disk-layout,
|
| disk-layout-log-neq-orphans | proved | all subs proved
| sb-orph,
sb-log,
disk-layout,
|
| disk-layout-log-above-main | proved | all subs proved
| sb-lpt,
sb-orph,
sb-log,
disk-layout,
|
| disk-layout-avol-neq-1 | proved | all subs proved
| sb-lpt,
sb-orph,
sb-log,
disk-layout,
|
| disk-layout-avol-neq-0 | proved | all subs proved
| sb-lpt,
sb-orph,
sb-log,
disk-layout,
|
| disk-layout-avol-le-5 | proved | all subs proved
| sb-lpt,
sb-orph,
sb-log,
disk-layout,
|
| disk-layout-2-unfold | proved | all subs proved
| sb-lpt,
sb-orph,
sb-log,
disk-layout,
|
| disk-layout-1-unfold | proved | all subs proved
| sb-lpt,
sb-orph,
sb-log,
disk-layout,
|
| mapped-full | axiom | | |
| lebs-base | axiom | | |
| lebs-rec | axiom | | |
| disk-layout | axiom | | |
| sb-log | axiom | | |
| sb-orph | axiom | | |
| sb-lpt | axiom | | |