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-size-apebs1 | proved | all subs proved
| abs,
|
| abs-size-apebs0 | proved | all subs proved
| abs-echdr,
abs-vidhdr,
abs-peb,
abs,
|
| abs-reduce0 | proved | all subs proved
| abs-vidhdr,
abs-echdr,
abs-peb,
abs,
|
| abs-reduce | proved | all subs proved
| abs-vidhdr,
abs-echdr,
abs-peb,
abs,
|
| abs-peb-empty | proved | all subs proved
| is-encoded-vidheader-emptypage,
abs-vidhdr,
is-encoded-echeader-emptypage,
abs-echdr,
abs-peb,
|
| abs-fwd | proved | all subs proved
| abs-vidhdr,
abs-echdr,
abs-peb,
abs,
|
| abs-fillcount-valid-headers | proved | all subs proved
| abs-vidhdr,
abs-echdr,
abs-peb,
abs,
|
| abs-fillcount-empty-vidhdr | proved | all subs proved
| abs-vidhdr,
abs-echdr,
abs-peb,
abs,
|
| abs-fillcount-empty-echdr | proved | all subs proved
| abs-vidhdr,
abs-echdr,
abs-peb,
abs,
|
| abs-data-at | proved | all subs proved
| abs-vidhdr,
abs-echdr,
abs-peb,
abs,
|
| abs-bad | proved | all subs proved
| abs-vidhdr,
abs-echdr,
abs-peb,
abs,
|
| is-encoded-echeader-emptypage | proved | all subs proved
| |
| is-encoded-vidheader-emptypage | proved | all subs proved
| |
| abs | axiom | | |
| abs-peb | axiom | | |
| abs-echdr | axiom | | |
| abs-vidhdr | axiom | | |