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: |
|---|
| lls-lasso-inj | proved | all subs proved
| lls-base,
lls-lasso-inj-gen,
lls-rec,
|
| lls-lasso-inj-gen | proved | all subs proved
| lls-unfold-tail,
lls-rec,
lls-base,
|
| 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,
|
| ls-lls-last | proved | all subs proved
| lls-one,
lls-merge,
lls-unfold-tail,
lls-to-ls,
|
| ls-split | proved | all subs proved
| lls-split,
ls-lls,
|
| ls-lls | proved | all subs proved
| lls-rec,
lls-base,
lls-null,
|
| lls-split | proved | all subs proved
| lls-consecutive,
lls-rec,
lls-base,
|
| lls-to-ls | proved | all subs proved
| lls-rec,
lls-null,
lls-base,
|
| lls-merge | proved | all subs proved
| lls-merge-gen,
|
| lls-unfold-tail | proved | all subs proved
| lls-fold-tail,
lls-rec,
lls-base,
lls-one,
|
| ll-trav1-end | proved | all subs proved
| lls-one,
lls-null,
lls-rec,
lls-base,
ll-trav1-def,
|
| ll-trav2-end | proved | all subs proved
| lls-one,
lls-null,
lls-rec,
lls-base,
ll-trav2-null-def,
ll-trav2-nonnull-def,
|
| lls-fold-tail2 | proved | all subs proved
| lls-fold-tail,
|
| lls-prefix | proved | all subs proved
| lls-prefix-gen,
|
| lls-unfold-head-simp | proved | all subs proved
| lls-base,
lls-unfold-head,
|
| lls-unfold-head | proved | all subs proved
| lls-rec,
|
| lls-consecutive | proved | all subs proved
| lls-rec,
lls-base,
|
| lls-prefix-gen | proved | all subs proved
| lls-rec,
lls-base,
|
| lls-merge-gen | proved | all subs proved
| lls-rec,
lls-base,
|
| 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,
|
| ll-trav1-init | proved | all subs proved
| lls-base,
ll-trav1-def,
|
| ll-trav2-init | proved | all subs proved
| ll-trav2-null-def,
|
| lls-fold-head | proved | all subs proved
| lls-rec,
|
| lls-injective | proved | all subs proved
| lls-rec,
lls-base,
|
| ll-trav2-nonnull-def | axiom | | |
| ll-trav2-null-def | axiom | | |
| ll-trav1-def | axiom | | |
| lls-base | axiom | | |
| lls-rec | axiom | | |