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,
ins-max,
|
| max-sort-sublist | proved | all subs proved
| max-ge,
max-base,
max-rec,
sort-max-max-list,
|
| sort-max | proved | all subs proved
| sort-max-max-list,
ordered-max,
|
| sort-max-max-list | proved | all subs proved
| max-ins,
ordered-max,
ins-max,
max-rec,
max-base,
|
| max-ge-every | proved | all subs proved
| max-rec,
max-ge-first,
|
| allls-allle | proved | all subs proved
| notallle-notallls,
|
| max-com-01 | proved | all subs proved
| max-com,
|
| allgr-allge | proved | all subs proved
| notallge-notallge,
|
| max-ins-max | proved | all subs proved
| max-ge-first,
max-rec,
max-base,
|
| max-ordered | proved | all subs proved
| max-ge,
max-base,
max-rec,
|
| max-append | proved | all subs proved
| max-ge,
max-base,
max-rec,
|
| max-ins | proved | all subs proved
| max-rec,
max-base,
|
| ordered-max | proved | all subs proved
| max-rec,
max-base,
|
| notallge-notallge | proved | all subs proved
| allge-def,
allgr-def,
|
| max-ge | proved | all subs proved
| max-base,
max-rec,
|
| max-com | proved | all subs proved
| max-base,
max-rec,
|
| notallle-notallls | proved | all subs proved
| allle-def,
allls-def,
|
| ins-max | proved | all subs proved
| max-base,
max-rec,
|
| max-ge-first | proved | all subs proved
| max-base,
max-rec,
|
| allge-in | proved | all subs proved
| allge-def,
|
| allgrrange-recup | proved | all subs proved
| allgr-range-def,
|
| allgr-empty | proved | all subs proved
| allgr-range-def,
|
| allle-inclower | proved | all subs proved
| allle-range-def,
|
| alllsrange-lslow | proved | all subs proved
| allls-range-def,
|
| allls-allsrange | proved | all subs proved
| allls-range-def,
allls-def,
|
| allle-rec | proved | all subs proved
| allle-def,
|
| allgr-alt-def | proved | all subs proved
| allgr-def,
|
| allgr-notls | proved | all subs proved
| allgr-def,
|
| allge-rec | proved | all subs proved
| allge-def,
|
| allgerange-notlowls | proved | all subs proved
| allge-range-def,
|
| max-in | proved | all subs proved
| max-base,
max-rec,
|
| alllsrange-upls | proved | all subs proved
| allls-range-def,
|
| allgr-inclower | proved | all subs proved
| allgr-range-def,
|
| allle-base | proved | all subs proved
| allle-def,
|
| allle-decupper | proved | all subs proved
| allle-range-def,
|
| allls-incupper | proved | all subs proved
| allls-range-def,
|
| allgrrange-upgr | proved | all subs proved
| allgr-range-def,
|
| allls-in | proved | all subs proved
| allls-def,
|
| allgr-numone | proved | all subs proved
| allgr-range-def,
|
| allle-incupper | proved | all subs proved
| allle-range-def,
|
| allge-inclower | proved | all subs proved
| allge-range-def,
|
| alllsrange-notlowgr | proved | all subs proved
| allls-range-def,
|
| alllerange-recup | proved | all subs proved
| allle-range-def,
|
| allls-numone | proved | all subs proved
| allls-range-def,
|
| allgr-decupper | proved | all subs proved
| allgr-range-def,
|
| min-com | proved | all subs proved
| min-base,
min-rec,
|
| allgrrange-grlow | proved | all subs proved
| allgr-range-def,
|
| alllerange-reclow | proved | all subs proved
| allle-range-def,
|
| allle-one | proved | all subs proved
| allle-range-def,
|
| allge-one | proved | all subs proved
| allge-range-def,
|
| allgr-in | proved | all subs proved
| allgr-def,
|
| allgr-incupper | proved | all subs proved
| allgr-range-def,
|
| allge-decupper | proved | all subs proved
| allge-range-def,
|
| allle-in | proved | all subs proved
| allle-def,
|
| allge-incupper | proved | all subs proved
| allge-range-def,
|
| allgerange-reclow | proved | all subs proved
| allge-range-def,
|
| allls-ls | proved | all subs proved
| allls-def,
|
| allge-numone | proved | all subs proved
| allge-range-def,
|
| allle-numone | proved | all subs proved
| allle-range-def,
|
| alllerange-notupgr | proved | all subs proved
| allle-range-def,
|
| alllsrange-reclow | proved | all subs proved
| allls-range-def,
|
| allgrrange-notupgr | proved | all subs proved
| allgr-range-def,
|
| allls-empty | proved | all subs proved
| allls-range-def,
|
| allgr-decupper-inclower | proved | all subs proved
| allgr-range-def,
|
| max-ins-last | proved | all subs proved
| max-base,
max-rec,
|
| allls-base | proved | all subs proved
| allls-def,
|
| allgr-rec | proved | all subs proved
| allgr-def,
|
| alllsrange-notupgr | proved | all subs proved
| allls-range-def,
|
| allgr-one | proved | all subs proved
| allgr-range-def,
|
| allge-base | proved | all subs proved
| allge-def,
|
| allgrrange-reclow | proved | all subs proved
| allgr-range-def,
|
| allge-alt-def | proved | all subs proved
| allge-def,
|
| allls-declower | proved | all subs proved
| allls-range-def,
|
| allls-notgr | proved | all subs proved
| allls-def,
|
| allle-decupper-inclower | proved | all subs proved
| allle-range-def,
|
| ordered-app-max | proved | all subs proved
| max-rec,
max-base,
|
| allle-alllerange | proved | all subs proved
| allle-range-def,
allle-def,
|
| allgr-allsrange | proved | all subs proved
| allgr-range-def,
allgr-def,
|
| max-ge-01 | proved | all subs proved
| max-rec,
|
| allle-empty | proved | all subs proved
| allle-range-def,
|
| allge-notls | proved | all subs proved
| allge-def,
|
| allls-alt-def | proved | all subs proved
| allls-def,
|
| allgerange-notupls | proved | all subs proved
| allge-range-def,
|
| min-in-01 | proved | all subs proved
| min-rec,
min-base,
|
| allgr-gr | proved | all subs proved
| allgr-def,
|
| allle-notgr | proved | all subs proved
| allle-def,
|
| allls-one | proved | all subs proved
| allls-range-def,
|
| max-in-01 | proved | all subs proved
| max-rec,
max-base,
|
| allls-rec | proved | all subs proved
| allls-def,
|
| allgr-base | proved | all subs proved
| allgr-def,
|
| allgr-declower | proved | all subs proved
| allgr-range-def,
|
| allls-decupper | proved | all subs proved
| allls-range-def,
|
| alllsrange-recup | proved | all subs proved
| allls-range-def,
|
| alllerange-notlowgr | proved | all subs proved
| allle-range-def,
|
| allge-allgerange | proved | all subs proved
| allge-range-def,
allge-def,
|
| allge-declower | proved | all subs proved
| allge-range-def,
|
| allls-decupper-inclower | proved | all subs proved
| allls-range-def,
|
| allgerange-recup | proved | all subs proved
| allge-range-def,
|
| allge-empty | proved | all subs proved
| allge-range-def,
|
| allge-decupper-inclower | proved | all subs proved
| allge-range-def,
|
| allle-alt-def | proved | all subs proved
| allle-def,
|
| allls-inclower | proved | all subs proved
| allls-range-def,
|
| allgrrange-notlowgr | proved | all subs proved
| allgr-range-def,
|
| allle-declower | proved | all subs proved
| allle-range-def,
|
| min-rec | axiom | | |
| min-base | axiom | | |
| max-base | axiom | | |
| allge-range-def | axiom | | |
| allgr-def | axiom | | |
| allle-def | axiom | | |
| allls-def | axiom | | |
| allls-range-def | axiom | | |
| max-rec | axiom | | |
| allle-range-def | axiom | | |
| allgr-range-def | axiom | | |
| allge-def | axiom | | |