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: |
|---|
| ll-trav1-next | proved | all subs proved
| lls-unfold-tail,
lls-rec,
lls-base,
ll-trav1-def,
|
| ll-trav2-next | proved | all subs proved
| lls-unfold-tail,
lls-rec,
lls-base,
ll-trav2-null-def,
ll-trav2-nonnull-def,
|
| lls-unfold-tail | proved | all subs proved
| lls-fold-tail,
lls-rec,
lls-base,
lls-one,
|
| ll-trav2-end | proved | all subs proved
| lls-one,
lls-null,
lls-rec,
lls-base,
ll-trav2-null-def,
ll-trav2-nonnull-def,
|
| lls-to-ls | proved | all subs proved
| lls-rec,
lls-null,
lls-base,
|
| ll-trav1-end | proved | all subs proved
| lls-one,
lls-null,
lls-rec,
lls-base,
ll-trav1-def,
|
| lls-unfold-head-simp | proved | all subs proved
| lls-base,
lls-unfold-head,
|
| lls-fold-tail | proved | all subs proved
| lls-base,
lls-rec,
|
| lls-null | proved | all subs proved
| lls-rec,
lls-base,
|
| lls-one | proved | all subs proved
| lls-base,
lls-rec,
|
| lls-unfold-head | proved | all subs proved
| lls-rec,
|
| lls-fold-head | proved | all subs proved
| lls-rec,
|
| ll-trav2-init | proved | all subs proved
| ll-trav2-null-def,
|
| lls-consecutive | proved | all subs proved
| lls-rec,
lls-base,
|
| ll-trav1-init | proved | all subs proved
| lls-base,
ll-trav1-def,
|
| ll-trav2-nonnull-def | axiom | | |
| ll-trav2-null-def | axiom | | |
| lls-rec | axiom | | |
| ll-trav1-def | axiom | | |
| lls-base | axiom | | |