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: |
|---|
| slice-range0 | proved | all subs proved
| prefixn-0,
dropn,
slice,
|
| prefixn-neq-empty-plusone | proved | all subs proved
| prefixn-empty,
prefixn,
|
| prefixn-eq-append | proved | all subs proved
| prefixn-append-left,
prefixn,
|
| prefixn-append-prefix | proved | all subs proved
| prefixn-shift-right,
prefixn,
prefixn-append-left,
|
| prefixn-0 | proved | all subs proved
| prefixn,
|
| prefixn-empty | proved | all subs proved
| prefixn,
|
| prefixn-append-left | proved | all subs proved
| prefixn,
|
| prefixn-shift-right | proved | all subs proved
| prefixn,
|
| prefixn-split-sublist | proved | all subs proved
| prefixn,
|
| prefixn-split-dropn | proved | all subs proved
| dropn,
prefixn,
|
| prefixn-size-prefixn | proved | all subs proved
| prefixn,
|
| prefixn-size-eq | proved | all subs proved
| prefixn,
|
| prefixn-single-1 | proved | all subs proved
| prefixn,
|
| prefixn-prepend-one | proved | all subs proved
| prefixn,
|
| prefixn-prefixn | proved | all subs proved
| prefixn,
|
| prefixn-notin | proved | all subs proved
| prefixn,
|
| prefixn-nodups | proved | all subs proved
| prefixn,
|
| prefixn-len-n | proved | all subs proved
| prefixn,
|
| prefixn-len-le-n | proved | all subs proved
| prefixn,
|
| prefixn-le-size | proved | all subs proved
| prefixn,
|
| prefixn-le-eq | proved | all subs proved
| prefixn,
|
| prefixn-in | proved | all subs proved
| prefixn,
|
| prefixn-fulln | proved | all subs proved
| prefixn,
|
| prefixn-full-eq | proved | all subs proved
| prefixn,
|
| prefixn-full | proved | all subs proved
| prefixn,
|
| prefixn-eq-prefixn-app | proved | all subs proved
| prefixn,
|
| prefixn-eq-empty | proved | all subs proved
| prefixn,
|
| prefixn-butlast | proved | all subs proved
| prefixn,
|
| prefixn-append-slice | proved | all subs proved
| dropn,
slice,
prefixn,
|
| prefix-prefixn-same | proved | all subs proved
| prefixn,
|
| prefix-prefixn-not-shorter | proved | all subs proved
| prefixn,
|
| prefix-prefixn-exact | proved | all subs proved
| prefixn,
|
| isprefix-prefixn | proved | all subs proved
| prefixn,
|
| isprefix-app-prefixn-isprefix | proved | all subs proved
| prefixn,
|
| isprefix-add-prefixn-size | proved | all subs proved
| prefixn,
|
| in-prefixn-samepos | proved | all subs proved
| prefixn,
|
| in-prefixn-pos-smaller0 | proved | all subs proved
| prefixn,
|
| in-prefixn-pos-smaller | proved | all subs proved
| prefixn,
|
| in-prefixn-in-shorter-prefix | proved | all subs proved
| prefixn,
|
| in-prefixn-at-smaller | proved | all subs proved
| prefixn,
|
| dropn-first | proved | all subs proved
| dropn,
|
| dropn-empty | proved | all subs proved
| dropn,
|
| dropn-0 | proved | all subs proved
| dropn,
|
| slice | axiom | | |
| prefixn | axiom | | |
| dropn | axiom | | |