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: |
|---|
| datasize-split-empty | proved | all subs proved
| datasize-split-empty-h,
datasize,
|
| datasize-split-empty-h | proved | all subs proved
| datasize-zero-h,
datasize-append-lower-h,
datasize-append-h-new,
|
| datsize-write-higher | proved | all subs proved
| datsize-write-higher-h,
datasize,
|
| datasize-ls-samedata | proved | all subs proved
| datasize-ls-samedata-h,
datasize,
|
| datasize-append | proved | all subs proved
| datasize-base,
datasize-append-lower-h,
datasize-append-h-new,
datasize,
|
| datsize-write-higher-h | proved | all subs proved
| datasize-ls-add,
datasize-at,
datasize-is-smaller-help,
datasize-rec,
datasize-base,
datasize,
|
| datasize-ls-samedata-h | proved | all subs proved
| datasize-ls-add,
datasize-at,
datasize-is-smaller-help,
datasize-rec,
datasize-base,
datasize,
|
| datasize-append-h-new | proved | all subs proved
| datasize-base,
datasize-rec,
datasize-append-empty-h,
datasize-append-lower-h,
|
| datasize-subarray | proved | all subs proved
| datasize-subarray-h,
datasize,
|
| datasize-samebuf-h | proved | all subs proved
| datasize-ls-add,
datasize-rec,
|
| datasize-ls | proved | all subs proved
| datasize-ls-h,
datasize,
|
| datasize-empbuf | proved | all subs proved
| datasize-append-lower-h,
datasize-empbuf-h,
datasize,
|
| datasize-subarray-h | proved | all subs proved
| datasize-rec,
datasize-is-smaller-help,
datasize-base,
|
| datasize-at | proved | all subs proved
| datasize-at-h,
datasize,
|
| datasize-ls-add | proved | all subs proved
| datasize-is-smaller-help,
|
| datasize-ls-h | proved | all subs proved
| datasize-at-h,
datasize-le-h,
|
| datasize-empbuf-h | proved | all subs proved
| datasize-rec,
datasize-base,
datasize-append-lower-h,
|
| datasize-append-empty-h | proved | all subs proved
| datasize-rec,
datasize-base,
datasize-append-lower-h,
|
| datasize-zero | proved | all subs proved
| datasize-zero-h,
datasize,
|
| datasize-subarray0 | proved | all subs proved
| datasize-subarray0-h,
datasize,
|
| datasize-mkempbuffer | proved | all subs proved
| datasize-mkempbuffer-h,
datasize,
|
| datasize-le-fwd | proved | all subs proved
| datasize-is-smaller-help,
datasize,
|
| datasize-le | proved | all subs proved
| datasize-le-h,
datasize,
|
| datasize-is-smaller | proved | all subs proved
| datasize-is-smaller-help,
datasize,
|
| datasize-subarray0-h | proved | all subs proved
| datasize-rec,
datasize-base,
|
| datasize-zero-h | proved | all subs proved
| datasize-rec,
datasize-base,
|
| datasize-mkempbuffer-h | proved | all subs proved
| datasize-rec,
datasize-base,
|
| datasize-le-h | proved | all subs proved
| datasize-rec,
datasize-base,
|
| datasize-is-smaller-help | proved | all subs proved
| datasize-rec,
datasize-base,
|
| datasize-at-h | proved | all subs proved
| datasize-rec,
datasize-base,
|
| datasize-append-lower-h | proved | all subs proved
| datasize-rec,
datasize-base,
|
| datasize-ls-datasize-h | proved | all subs proved
| datasize,
|
| datasize-further | proved | all subs proved
| datasize-rec,
datasize-base,
|
| datasize-datasize-elim-h | proved | all subs proved
| datasize-rec,
datasize-base,
|
| datasize-add-empty-h | proved | all subs proved
| datasize-rec,
|
| datasize | axiom | | |
| datasize-base | axiom | | |
| datasize-rec | axiom | | |