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: |
|---|
| sort-max-last-01 | proved | all subs proved
| sort-max-append-1,
|
| sort-max-append-1 | proved | all subs proved
| sort-max-last,
|
| sort-max-last | proved | all subs proved
| ordered-max,
ins-max,
max-base,
max-rec,
max-ins-max-last-sort,
|
| max-ins-max-last-sort | proved | all subs proved
| sort-max-max-list,
max-ins-max-last,
|
| sort-max | proved | all subs proved
| sort-max-max-list,
ordered-max,
|
| max-sort-sublist | proved | all subs proved
| max-ge,
max-base,
max-rec,
sort-max-max-list,
|
| sort-max-max-list | proved | all subs proved
| max-ins,
ordered-max,
ins-max,
max-rec,
max-base,
|
| max-ordered | proved | all subs proved
| max-ge,
max-ge-first,
max-base,
max-rec,
|
| max-ins-max | proved | all subs proved
| max-ge-first,
max-rec,
max-base,
|
| max-ge-every | proved | all subs proved
| max-base,
max-rec,
max-ge-first,
|
| max-com-01 | proved | all subs proved
| max-com,
|
| max-append | proved | all subs proved
| max-ge,
max-base,
max-rec,
|
| max-ins | proved | all subs proved
| max-rec,
max-base,
|
| ins-max | proved | all subs proved
| max-base,
max-rec,
|
| ordered-max | proved | all subs proved
| max-rec,
max-base,
|
| max-ins-max-last | proved | all subs proved
| max-base,
max-rec,
|
| max-ge-first | proved | all subs proved
| max-base,
max-rec,
|
| max-com | proved | all subs proved
| max-base,
max-rec,
|
| max-ge | proved | all subs proved
| max-base,
max-rec,
|
| ordered-app-max | proved | all subs proved
| max-rec,
max-base,
|
| min-com | proved | all subs proved
| min-base,
min-rec,
|
| max-ins-last | proved | all subs proved
| max-base,
max-rec,
|
| max-in-01 | proved | all subs proved
| max-rec,
max-base,
|
| max-in | proved | all subs proved
| max-base,
max-rec,
|
| max-ge-01 | proved | all subs proved
| max-rec,
|
| min-rec | axiom | | |
| min-base | axiom | | |
| max-rec | axiom | | |
| max-base | axiom | | |