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: |
|---|
| pebsize-simp-ls | proved | all subs proved
| lebsize-simp-ls,
pebsize-le-2page-size-n,
page-size,
peb-size,
|
| pebsize-le-2page-size-lebsize | proved | all subs proved
| pebsize-le-2page-size-n,
|
| lebsize-ls-2page-size-pebsize | proved | all subs proved
| pebsize-le-2page-size-n,
|
| lebsize-eq-2page-size-pebsize | proved | all subs proved
| pebsize-le-2page-size-n,
|
| lebsize-add-eq-0 | proved | all subs proved
| lebsize-neq-zero,
|
| lebsize-simp-ls | proved | all subs proved
| lebsize,
page-size,
leb-size,
|
| pebsize-le-2page-size-n | proved | all subs proved
| lebsize,
peb-size,
pebsize,
|
| lebsize-neq-zero | proved | all subs proved
| page-size,
leb-size,
lebsize,
|
| subarray-emptypeb-eq-emptypage1 | proved | all subs proved
| emptypeb-at,
peb-size,
emptypeb-size,
page-size,
emptypage-at,
emptypage-size,
|
| subarray-emptypeb-eq-emptypage | proved | all subs proved
| emptypeb-at,
peb-size,
emptypeb-size,
page-size,
emptypage-at,
emptypage-size,
|
| subarray-emptypeb-eq-emptyleb | proved | all subs proved
| emptypeb-at,
peb-size,
emptypeb-size,
page-size,
leb-size,
lebsize,
emptyleb-at,
emptyleb-size,
|
| pebsize-simp-neq | proved | all subs proved
| pebsize,
peb-size,
|
| pebsize-simp-ls-rev | proved | all subs proved
| page-size,
pebsize,
peb-size,
|
| pebsize-page-size-is-aligned | proved | all subs proved
| page-size,
peb-size,
pebsize,
|
| pebsize-minus-eb-page-size | proved | all subs proved
| lebsize,
peb-size,
pebsize,
|
| pebsize-minus-2eb-page-size | proved | all subs proved
| peb-size,
pebsize,
lebsize,
|
| pebsize-ls-lebsize | proved | all subs proved
| page-size,
leb-size,
lebsize,
peb-size,
pebsize,
|
| pebsize-ls-2page-size-n | proved | all subs proved
| lebsize,
peb-size,
pebsize,
|
| pebsize-le-page-size | proved | all subs proved
| peb-size,
pebsize,
page-size,
|
| pebsize-le-minus-eb-page-size | proved | all subs proved
| peb-size,
pebsize,
lebsize,
|
| pebsize-le-2page-size | proved | all subs proved
| peb-size,
pebsize,
page-size,
|
| peb-vs-leb-size-ext | proved | all subs proved
| peb-size,
|
| peb-vs-leb-size | proved | all subs proved
| peb-size,
|
| peb-size-rewrite | proved | all subs proved
| pebsize,
peb-size,
|
| peb-size-not0 | proved | all subs proved
| leb-size,
peb-size,
|
| peb-size-ge2 | proved | all subs proved
| peb-size,
|
| lebsize-pebsize | proved | all subs proved
| peb-size,
pebsize,
lebsize,
|
| lebsize-page-size-is-aligned | proved | all subs proved
| page-size,
lebsize,
|
| lebsize-2page-size-le | proved | all subs proved
| peb-size,
pebsize,
lebsize,
|
| leb-size-rewrite | proved | all subs proved
| lebsize,
|
| emptypage-size | axiom | | |
| emptypage-at | axiom | | |
| emptyleb-size | axiom | | |
| emptyleb-at | axiom | | |
| emptypeb-size | axiom | | |
| emptypeb-at | axiom | | |
| leb-size | axiom | | |
| page-size | axiom | | |
| pebsize | axiom | | |
| peb-size | axiom | | |
| lebsize | axiom | | |