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: |
|---|
| abs-nodes-add-crash-aligned-nodes | proved | all subs proved
| abs-nodes-append-h,
abs-nodes-add-crash-aligned,
ls-abs-node-buf-size,
abs-nodes-no-padding-last,
abs-nodes-unique-strong-h,
abs-nodes-elems-adr-length-h,
abs-nodes,
|
| abs-nodes-no-padding-last | proved | all subs proved
| inj-adr,
abs-nodes-one-abs-node,
abs-nodes-append-h,
abs-nodes-rec,
abs-nodes-unique-strong-h,
abs-nodes-elems-adr-length-h,
abs-nodes-no-padding-rec,
size-rec,
abs-nodes-mkbuf0-empty-h,
ls-abs-node-buf-size,
abs-nodes-no-padding-one,
flashsize-one,
|
| abs-nodes-no-padding-one | proved | all subs proved
| abs-nodes-nospace-h,
ls-abs-node-buf-size,
abs-nodes-elems-empty-adr-empty-h,
abs-nodes-mkbuf0-empty-h,
flashsize-one,
abs-nodes-no-padding-rec,
|
| abs-nodes-subarray-failed | proved | all subs proved
| abs-nodes-rec,
abs-nodes-mkbuf0-empty-h,
abs-nodes-one-h,
abs-nodes-base,
ls-abs-node-buf-size,
abs-nodes-no-padding-rec,
size-rec,
flashsize-eq-0,
abs-nodes-elems-adr-length-h,
|
| abs-nodes-no-padding-rec | proved | all subs proved
| ls-abs-node-buf-size,
abs-nodes-unique-strong-h,
abs-nodes-at-least-flashsize,
abs-nodes-rec,
abs-nodes-first-adr-explicit,
size-rec,
|
| abs-nodes-add-crash-aligned | proved | all subs proved
| abs-nodes-mkbuf0-empty-h,
abs-nodes-rec,
abs-nodes-append-h,
abs-nodes-unique-strong-h,
abs-nodes-add-crash-aligned-h,
ls-abs-node-buf-size,
abs-nodes,
|
| add-failed-is-aligned | proved | all subs proved
| abs-nodes-nospace-h,
abs-nodes-aligned-headersize-h,
abs-nodes-aligned-headersize,
abs-nodes,
|
| abs-nodes-strong-imp-weak | proved | all subs proved
| abs-nodes-strong-imp-weak-h,
abs-nodes,
|
| abs-nodes-split | proved | all subs proved
| abs-nodes-unique-strong-h,
abs-nodes-split-h,
abs-nodes,
|
| abs-nodes-nodups | proved | all subs proved
| abs-nodes-nodups-h,
abs-nodes,
|
| abs-nodes-crash | proved | all subs proved
| abs-nodes-unique-weak-h,
abs-nodes-crash-h,
abs-nodes,
|
| abs-nodes-append-empty | proved | all subs proved
| abs-nodes-prefix-elim,
|
| abs-nodes-append | proved | all subs proved
| abs-nodes-prefix-elim,
|
| abs-nodes-aligned-headersize | proved | all subs proved
| abs-nodes-aligned-headersize-h,
abs-nodes,
|
| abs-nodes-strong-imp-weak-h | proved | all subs proved
| abs-nodes-unique-strong-h,
|
| abs-nodes-split-h | proved | all subs proved
| ls-abs-node-buf-size,
abs-nodes-unique-strong-h,
abs-nodes-padding-prefix,
abs-nodes-first-adr-explicit,
abs-nodes-rec,
abs-nodes-mkbuf0-empty-h,
|
| abs-nodes-nodups-h | proved | all subs proved
| abs-nodes-before-no-address-h,
ls-abs-node-buf-size,
abs-nodes-rec,
abs-nodes-elems-empty-adr-empty-h,
|
| abs-nodes-at-least-flashsize | proved | all subs proved
| ls-abs-node-buf-size,
abs-nodes-unique-strong-h,
abs-nodes-first-adr-explicit,
abs-nodes-rec,
size-rec,
flashsize-eq-0,
|
| abs-nodes-crash-h | proved | all subs proved
| ls-abs-node-buf-size,
abs-nodes-headerspace,
abs-nodes-first-adr-explicit,
abs-nodes-rec,
abs-nodes-nospace-h,
abs-nodes-unique-weak-h,
abs-nodes-padding-prefix,
abs-nodes-mkbuf0-empty-h,
abs-nodes-base,
abs-nodes-elems-empty-adr-empty-h,
|
| abs-nodes-prefix-elim | proved | all subs proved
| abs-nodes-nospace-h,
abs-nodes-append-h,
abs-nodes-unique-strong-h,
abs-nodes-prefix-h,
abs-nodes,
|
| abs-nodes-add-crash-aligned-h | proved | all subs proved
| abs-nodes-first-adr-explicit,
abs-nodes-rec,
abs-nodes-unique-strong-h,
abs-nodes-padding-prefix,
abs-nodes-one-h,
abs-nodes-base,
abs-nodes-elems-empty-adr-empty-h,
ls-abs-node-buf-size,
|
| abs-split-by-address | proved | all subs proved
| ls-abs-node-buf-size,
abs-split-by-address-h,
abs-nodes,
|
| abs-nodes-unique-weak | proved | all subs proved
| abs-nodes-unique-weak-h,
abs-nodes,
|
| abs-nodes-unique-strong | proved | all subs proved
| abs-nodes-unique-strong-h,
abs-nodes,
|
| abs-nodes-strengthen | proved | all subs proved
| abs-nodes-unique-strong-h,
abs-nodes,
|
| abs-nodes-prefix | proved | all subs proved
| abs-nodes-prefix-h,
abs-nodes,
|
| abs-nodes-one | proved | all subs proved
| abs-nodes-one-h,
abs-nodes,
|
| abs-nodes-nospace | proved | all subs proved
| abs-nodes-nospace-h,
abs-nodes-mkbuf0-empty,
abs-nodes,
|
| abs-nodes-crash-prefix | proved | all subs proved
| abs-nodes-prefix-h,
abs-nodes,
|
| abs-nodes-case-distinction-h | proved | all subs proved
| ls-abs-node-buf-size,
abs-nodes-unique-weak-h,
abs-nodes-rec,
abs-nodes-first-adr-explicit,
abs-nodes-base,
abs-nodes-elems-empty-adr-empty-h,
|
| abs-nodes-bothcrash-prefix | proved | all subs proved
| abs-nodes-prefix-h,
abs-nodes,
|
| abs-nodes-beyond-no-address | proved | all subs proved
| abs-nodes-beyond-no-address-h,
abs-nodes,
|
| abs-nodes-atend-no-address | proved | all subs proved
| abs-nodes-beyond-no-address-h,
abs-nodes,
|
| abs-nodes-append-empty-h | proved | all subs proved
| abs-nodes-unique-strong-h,
abs-nodes-append-h,
|
| abs-nodes-aligned-2headersize-mod | proved | all subs proved
| abs-nodes-aligned-2headersize-h,
abs-nodes,
|
| abs-nodes-aligned-2headersize | proved | all subs proved
| abs-nodes-aligned-2headersize-h,
abs-nodes,
|
| abs-split-by-address-h | proved | all subs proved
| ls-abs-node-buf-size,
abs-nodes-rec,
abs-nodes-elems-empty-adr-empty-h,
|
| abs-nodes-mkbuf0-empty | proved | all subs proved
| abs-nodes-mkbuf0-empty-h,
abs-nodes,
|
| abs-nodes-before-no-address-h | proved | all subs proved
| inj-adr,
ls-abs-node-buf-size,
abs-nodes-rec,
abs-nodes-elems-empty-adr-empty-h,
|
| abs-nodes-one-abs-node | proved | all subs proved
| abs-nodes-mkbuf0-empty-h,
abs-nodes-elems-empty-adr-empty-h,
inj-adr,
abs-nodes-rec,
ls-abs-node-buf-size,
|
| abs-nodes-unique-weak-h | proved | all subs proved
| abs-failed-abs-nodes-h,
abs-nodes-nospace-h,
ls-abs-node-buf-size,
abs-nodes-first-adr-explicit,
abs-nodes-rec,
abs-nodes-padding-prefix,
abs-nodes-mkbuf0-empty-h,
abs-nodes-base,
abs-nodes-elems-empty-adr-empty-h,
|
| abs-nodes-prefix-h | proved | all subs proved
| abs-nodes-nospace-h,
abs-nodes-base,
ls-abs-node-buf-size,
abs-nodes-padding-prefix,
abs-nodes-first-adr-explicit,
abs-nodes-rec,
abs-nodes-elems-empty-adr-empty-h,
|
| abs-nodes-beyond-no-address-h | proved | all subs proved
| abs-nodes-nospace-h,
ls-abs-node-buf-size,
abs-nodes-rec,
abs-nodes-elems-empty-adr-empty-h,
|
| abs-nodes-aligned-headersize-h | proved | all subs proved
| ls-abs-node-buf-size,
abs-nodes-first-adr-explicit,
abs-nodes-rec,
abs-nodes-base,
abs-nodes-elems-empty-adr-empty-h,
|
| abs-nodes-aligned-2headersize-h | proved | all subs proved
| ls-abs-node-buf-size,
abs-nodes-first-adr-explicit,
abs-nodes-rec,
abs-nodes-base,
abs-nodes-elems-empty-adr-empty-h,
|
| abs-nodes-one-h | proved | all subs proved
| abs-nodes-elems-empty-adr-empty-h,
ls-abs-node-buf-size,
abs-nodes-rec,
|
| abs-nodes-unique-strong-h | proved | all subs proved
| abs-nodes-nospace-h,
ls-abs-node-buf-size,
abs-nodes-first-adr-explicit,
abs-nodes-rec,
abs-nodes-padding-prefix,
abs-nodes-mkbuf0-empty-h,
abs-nodes-base,
abs-nodes-elems-empty-adr-empty-h,
|
| abs-nodes-append-h | proved | all subs proved
| ls-abs-node-buf-size,
abs-nodes-first-adr-explicit,
abs-nodes-rec,
abs-nodes-padding-prefix,
abs-nodes-base,
abs-nodes-elems-empty-adr-empty-h,
|
| abs-padding-abs-nodes-h | proved | all subs proved
| ls-abs-node-buf-size,
abs-nodes-nospace-h,
abs-nodes-first-adr-explicit,
abs-nodes-rec,
abs-nodes-mkbuf0-empty-h,
abs-nodes-elems-empty-adr-empty-h,
abs-nodes-base,
|
| abs-nodes-valid-node | proved | all subs proved
| ls-abs-node-buf-size,
abs-nodes-first-adr-explicit,
abs-nodes-rec,
abs-nodes-headerspace,
abs-nodes-mkbuf0-empty-h,
abs-nodes-base,
abs-nodes-elems-empty-adr-empty-h,
abs-nodes-padding-prefix,
|
| abs-nodes-notrailer-h | proved | all subs proved
| ls-abs-node-buf-size,
abs-nodes-nospace-h,
abs-nodes-headerspace,
abs-nodes-mkbuf0-empty-h,
abs-nodes-first-adr-explicit,
abs-nodes-rec,
abs-nodes-base,
abs-nodes-elems-empty-adr-empty-h,
abs-failed-abs-nodes-h,
|
| abs-nodes-nospace-header-h | proved | all subs proved
| ls-abs-node-buf-size,
abs-nodes-headerspace,
abs-nodes-mkbuf0-empty-h,
abs-nodes-first-adr-explicit,
abs-nodes-rec,
abs-nodes-base,
abs-nodes-elems-empty-adr-empty-h,
abs-failed-abs-nodes-h,
|
| abs-nodes-emptyheader-h | proved | all subs proved
| ls-abs-node-buf-size,
abs-nodes-nospace-h,
abs-nodes-headerspace,
abs-nodes-mkbuf0-empty-h,
abs-nodes-first-adr-explicit,
abs-nodes-rec,
abs-nodes-elems-empty-adr-empty-h,
abs-nodes-base,
|
| abs-nodes-elems-empty-adr-empty | proved | all subs proved
| abs-nodes-elems-empty-adr-empty-h,
abs-nodes,
|
| abs-nodes-headerspace | proved | all subs proved
| abs-nodes-nospace-h,
|
| abs-nodes-elems-empty-adr-empty-h | proved | all subs proved
| abs-nodes-elems-adr-length-h,
|
| abs-nodes-mkbuf0-empty-h | proved | all subs proved
| abs-nodes-nospace-h,
abs-nodes-base,
|
| abs-nodes-elems-adr-length | proved | all subs proved
| abs-nodes-elems-adr-length-h,
abs-nodes,
|
| abs-failed-abs-nodes | proved | all subs proved
| abs-failed-abs-nodes-h,
abs-nodes,
|
| abs-nodes-nospace-h | proved | all subs proved
| abs-nodes-first-adr-explicit,
abs-nodes-rec,
abs-nodes-base,
|
| abs-nodes-elems-adr-length-h | proved | all subs proved
| ls-abs-node-buf-size,
abs-nodes-first-adr-explicit,
abs-nodes-rec,
abs-nodes-base,
|
| abs-failed-abs-nodes-h | proved | all subs proved
| abs-nodes-first-adr-explicit,
abs-nodes-rec,
abs-nodes-base,
|
| flashsize-one | proved | all subs proved
| size-base,
size-rec,
|
| flashsize-eq-0 | proved | all subs proved
| size-rec,
size-base,
|
| abs-nodes-padding-prefix | proved | all subs proved
| abs-nodes-rec,
abs-nodes-base,
|
| abs-nodes-first-adr-explicit | proved | all subs proved
| ls-abs-node-buf-size,
abs-nodes-rec,
|
| size-base | axiom | | |
| inj-adr | proved | all subs proved
| |
| size-rec | axiom | | |
| ls-abs-node-buf-size | proved | all subs proved
| |
| abs-nodes-base | axiom | | |
| abs-nodes-rec | axiom | | |
| abs-nodes | axiom | | |