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: |
|---|
| isempty-append | proved | all subs proved
| isempty-elim-right0,
isempty-ext,
isempty,
|
| isempty-elim-right0 | proved | all subs proved
| isempty,
isempty-elim-right,
|
| isempty-elim-right | proved | all subs proved
| isempty-elim-left0,
isempty-ext,
|
| isempty-elim-left | proved | all subs proved
| isempty-elim-left0,
isempty-ext,
|
| isempty-elim-left0 | proved | all subs proved
| isempty-ext,
|
| subarray-emptypeb-eq-emptypage1 | proved | all subs proved
| lebsize-pebsize,
page-size,
emptypage,
emptypeb,
|
| subarray-emptypeb-eq-emptypage | proved | all subs proved
| pebsize-le-page-size,
page-size,
emptypage,
emptypeb,
|
| subarray-emptypeb-eq-emptyleb | proved | all subs proved
| pebsize-ls-2page-size-n,
emptyleb,
emptypeb,
|
| pebsize-simp-ls | proved | all subs proved
| lebsize-simp-ls,
pebsize-le-2page-size-n,
page-size,
peb-size,
|
| pebsize-le-minus-eb-page-size | proved | all subs proved
| peb-size,
pebsize,
lebsize,
page-size-plus-eq-0,
|
| pebsize-le-2page-size-lebsize | proved | all subs proved
| pebsize-le-2page-size-n,
|
| page-size-simp6 | proved | all subs proved
| lebsize-page-size-is-aligned,
page-size,
|
| page-size-simp4 | proved | all subs proved
| lebsize-page-size-is-aligned,
page-size,
|
| 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,
|
| isempty-empbuf | proved | all subs proved
| isempty-ext,
isempty,
|
| lebsize-pebsize | proved | all subs proved
| peb-size,
pebsize,
lebsize,
|
| pebsize-le-page-size | proved | all subs proved
| peb-size,
pebsize,
page-size,
|
| pebsize-ls-2page-size-n | proved | all subs proved
| lebsize,
peb-size,
pebsize,
|
| lebsize-simp-ls | proved | all subs proved
| lebsize,
page-size,
leb-size,
|
| page-size-plus-eq-0 | proved | all subs proved
| page-size,
|
| lebsize-page-size-is-aligned | proved | all subs proved
| page-size,
lebsize,
|
| 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,
|
| isempty-ext | proved | all subs proved
| is-empty-range-rec,
isempty-range-base,
|
| pebsize-simp-ls-rev | proved | all subs proved
| pebsize,
peb-size,
|
| pebsize-simp | proved | all subs proved
| pebsize,
|
| 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,
lebsize,
peb-size,
pebsize,
|
| 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,
|
| page-size-simp5 | proved | all subs proved
| page-size-rewrite-sum,
|
| page-size-simp3 | proved | all subs proved
| page-size-rewrite-sum,
|
| page-size-simp2 | proved | all subs proved
| page-size-rewrite-sum,
|
| page-size-simp1 | proved | all subs proved
| page-size-rewrite-sum,
|
| lebsize-not-ls-pagesize | proved | all subs proved
| leb-size,
lebsize,
page-size,
|
| lebsize-2page-size-le | proved | all subs proved
| peb-size,
pebsize,
lebsize,
|
| leb-size-rewrite | proved | all subs proved
| lebsize,
|
| emptypeb-size | proved | all subs proved
| emptypeb,
|
| emptypeb-at | proved | all subs proved
| emptypeb,
|
| emptypage-size | proved | all subs proved
| emptypage,
|
| emptypage-at | proved | all subs proved
| emptypage,
|
| emptyleb-size | proved | all subs proved
| emptyleb,
|
| emptyleb-at | proved | all subs proved
| emptyleb,
|
| empbuf-eq-emptypage | proved | all subs proved
| emptypage,
|
| page-size-rewrite-sum | proved | all subs proved
| |
| leb-size | axiom | | |
| page-size | axiom | | |
| pebsize | axiom | | |
| peb-size | axiom | | |
| lebsize | axiom | | |
| isempty-range-base | axiom | | |
| is-empty-range-rec | axiom | | |
| isempty | axiom | | |
| emptypeb | axiom | | |
| emptyleb | axiom | | |
| emptypage | axiom | | |