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: |
|---|
| encode-node | proved | all subs proved
| buf-size-zero,
abs-node,
|
| decode-node | proved | all subs proved
| buf-size-zero,
abs-node,
|
| buf-elim-2 | proved | all subs proved
| buf-size-zero,
|
| buf-elim | proved | all subs proved
| buf-size-zero,
|
| abs-padding-subarray-failed | proved | all subs proved
| buf-size-zero,
abs-failed,
abs-padding,
|
| abs-padding-size | proved | all subs proved
| abs-padding,
|
| abs-padding-nospace | proved | all subs proved
| abs-padding,
|
| abs-padding-mkbuf0 | proved | all subs proved
| abs-padding,
|
| abs-padding-isempty | proved | all subs proved
| abs-padding,
|
| abs-padding-full | proved | all subs proved
| abs-padding,
|
| abs-padding-eq | proved | all subs proved
| abs-padding,
|
| abs-padding-alignup | proved | all subs proved
| abs-padding,
|
| abs-padding-aligned-2headersize | proved | all subs proved
| abs-padding,
|
| abs-padding-abs-failed-append | proved | all subs proved
| abs-failed,
abs-padding,
|
| abs-node-unique | proved | all subs proved
| abs-node,
|
| abs-node-subarray-failed | proved | all subs proved
| abs-failed,
abs-node,
|
| abs-node-no-abs-padding | proved | all subs proved
| abs-node,
abs-padding,
|
| abs-node-isempty | proved | all subs proved
| abs-node,
|
| abs-node-full | proved | all subs proved
| abs-node,
|
| abs-node-emptybuf | proved | all subs proved
| abs-node,
|
| abs-node-aligned-headersize | proved | all subs proved
| abs-node,
|
| abs-node-aligned-2headersize | proved | all subs proved
| abs-node,
|
| abs-node-abs-node-append-subarray | proved | all subs proved
| abs-node,
|
| abs-node-abs-node | proved | all subs proved
| abs-node,
|
| abs-node-abs-failed | proved | all subs proved
| abs-failed,
abs-node,
|
| abs-failed-size0 | proved | all subs proved
| buf-size-zero,
abs-failed,
|
| abs-failed-nospace | proved | all subs proved
| abs-failed,
|
| abs-failed-aligned-headersize | proved | all subs proved
| buf-size-zero,
abs-failed,
|
| abs-padding | axiom | | |
| abs-node | axiom | | |
| abs-failed | axiom | | |
| buf-size-zero | proved | all subs proved
| |