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: |
|---|
| dll-trav-next | proved | all subs proved
| dlls-unfold-tail,
dlls-last-head-null,
ll-trav-nonnull,
dlls-last-rec,
dlls-last-base,
dll-trav-null,
|
| dlls-unfold-tail | proved | all subs proved
| dlls-last-fold-tail,
dlls-last-rec,
dlls-last-base,
dlls-last-one,
|
| dll-trav-end | proved | all subs proved
| dlls-last-one,
dlls-last-head-null,
dlls-last-rec,
ll-trav-nonnull,
dlls-last-base,
dll-trav-null,
|
| dlls-to-dll | proved | all subs proved
| dlls-to-dll-prev,
|
| dlls-to-dll-prev | proved | all subs proved
| dlls-rec,
dlls-base,
|
| dlls-last-head-null | proved | all subs proved
| dlls-last-rec,
dlls-last-base,
|
| dlls-last-one | proved | all subs proved
| dlls-last-base,
dlls-last-rec,
|
| dlls-last-fold-tail | proved | all subs proved
| dlls-last-base,
dlls-last-rec,
|
| dlls-unfold-head-simp | proved | all subs proved
| dlls-rec,
dlls-base,
|
| dlls-null | proved | all subs proved
| dlls-rec,
dlls-base,
|
| dlls-last-consecutive | proved | all subs proved
| dlls-last-rec,
dlls-last-base,
|
| dll-trav-init | proved | all subs proved
| dll-trav-null,
|
| dlls-one | proved | all subs proved
| dlls-base,
dlls-rec,
|
| dlls-last-unfold-head | proved | all subs proved
| dlls-last-rec,
|
| dlls-unfold-head | proved | all subs proved
| dlls-rec,
|
| dlls-last-fold-head | proved | all subs proved
| dlls-last-rec,
|
| dlls-fold-head | proved | all subs proved
| dlls-rec,
|
| dlls-last-unfold-head-simp | proved | all subs proved
| dlls-last-rec,
dlls-last-base,
|
| dll-trav-null | axiom | | |
| ll-trav-nonnull | axiom | | |
| dlls-last-base | axiom | | |
| dlls-last-rec | axiom | | |
| dlls-base | axiom | | |
| dlls-rec | axiom | | |