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: |
|---|
| shearsort-correct | proved | all subs proved
| dirtyrowsone-rowsincreasing,
log2ub-lem,
sortrows-correct,
divup-half,
scolsort-dirtyboundhalf,
srowsorted-def,
srowsorted-dirtyboundunchanged,
sortcols-correct,
sortrowssnake-correct,
scolsorted-def,
log2ub-zero,
dirtyrows-trivialbound,
divup-one,
shearsort,
|
| sortcols-correct | proved | all subs proved
| sortcol-correct,
scolsorted-def,
sortcols,
scolsort-dirtyboundhalf,
|
| scolsort-dirtyboundhalf | proved | all subs proved
| countodd-maxcol0-bounded,
countevn-maxcol0-bounded,
clean0rows-bounded,
count-add-even-odd-ind,
max0column-countcol,
divup-def,
scolsorted-def,
max0column-determines-clean1rows,
max0column-clean0rowsbounded,
exists-max0column,
dirtyrows-def,
dirtyrowsbound-def,
|
| max0column-clean0rowsbounded | proved | all subs proved
| count0-leq-clean0-ind,
count-add-even-odd-ind,
max0column-countcol-big-odd,
scolsorted-def,
sortedperm-count-splits,
max0column-countcol-small-even,
clean0rows-notallls,
clean0rows-bounded,
scolsorted-clean0notls,
|
| max0column-countcol-small-even | proved | all subs proved
| clean0rows-bounded,
rowsorted-smallercol-evnbounded,
max0column-countcol,
|
| max0column-countcol-big-odd | proved | all subs proved
| count-add-even-odd-ind,
clean0rows-bounded,
rowsorted-biggercol-oddbounded,
max0column-countcol,
|
| max0column-countcol | proved | all subs proved
| scolsorted-count-below-clean0rows,
clean0rows-bounded,
scolsorted-samecount-above-clean0,
|
| sortrowssnake-correct | proved | all subs proved
| srowsorted-dirtyboundunchanged,
sortrowsnake-correct,
srowsorted-def,
sortrowssnake,
|
| scolsorted-samecount-above-clean0 | proved | all subs proved
| scolsorted-clean0notls,
clean0rows-allls,
clean0rows-bounded,
scolsorted-permcol,
|
| scolsorted-count-below-clean0rows | proved | all subs proved
| count0-leq-clean0,
scolsorted-colordered,
sortedperm-count-splits,
clean0rows-bounded,
scolsorted-clean0notls,
|
| scolsorted-clean0notls | proved | all subs proved
| count0-leq-clean0,
sortedperm-count-splits,
scolsorted-def,
count0-leq-clean0-ind,
clean0rows-notallls,
clean0rows-bounded,
|
| dirtyrowsone-rowsincreasing | proved | all subs proved
| scolsorted-def,
dirytrows-leone,
rowsincreasing-def,
dirtyrowsbound-def,
|
| srowsorted-dirtyboundunchanged | proved | all subs proved
| srowsorted-permrow,
rowperms-dirtyrowsunchanged,
dirtyrowsbound-def,
|
| sortcol-correct | proved | all subs proved
| sort-possible,
scolsorted-def,
scolsorted-permtoArr,
colno-updcol,
rowno-updcol,
sortcol,
|
| scolsorted-clean1notls | proved | all subs proved
| scolsorted-def,
scolsorted-colordered,
scolsorted-permcol,
count1-leq-clean1,
clean1rows-notallge,
clean1rows-bounded,
|
| countevn-maxcol0-bounded | proved | all subs proved
| divup-def,
countevn-bounded-ind,
clean1rows-allge,
countevn-zero-ind,
clean0-plus-clean1-bounded,
clean1rows-bounded,
countevn-append-ind,
dirtyrows-def,
|
| countodd-maxcol0-bounded | proved | all subs proved
| divup-def,
countodd-bounded-ind,
clean1rows-allge,
countodd-zero-ind,
clean0-plus-clean1-bounded,
clean1rows-bounded,
countodd-append-ind,
dirtyrows-def,
|
| count1-leq-clean1 | proved | all subs proved
| clean1rows-bounded,
count1-leq-clean1-ind,
|
| log2ub-zero | proved | all subs proved
| log2ub-log2,
|
| divup-half | proved | all subs proved
| divup-def,
divup2-def,
|
| sortrows-correct | proved | all subs proved
| sortrow-correct,
sortrows,
|
| dirytrows-leone | proved | all subs proved
| clean1rows-notallge,
clean0-plus-clean1-bounded,
clean0rows-notallls,
clean1rows-allge,
clean0rows-allls,
dirtyrows-def,
|
| count0-leq-clean0 | proved | all subs proved
| clean0rows-bounded,
count0-leq-clean0-ind,
|
| rowperms-dirtyrowsunchanged | proved | all subs proved
| rowperms-clean1unchanged,
rowperms-clean0unchanged,
dirtyrows-def,
|
| scolsorted-permtoArr | proved | all subs proved
| scolsorted-permtoArc-ind,
|
| count-add-even-odd | proved | all subs proved
| count-add-even-odd-ind,
countodd-def,
countevn-def,
|
| srowsorted-permtoArr | proved | all subs proved
| srowsorted-permtoArr-ind,
|
| rowsorted-smallercol-evnbounded | proved | all subs proved
| srowsorted-def,
countevn-rec,
countevn-base,
|
| exists-max0column | proved | all subs proved
| exists-max0column-ind,
|
| max0column-determines-clean1rows | proved | all subs proved
| clean1rows-allge,
sortedperm-count-splits,
clean1rows-notallge,
clean1rows-bounded,
|
| srowsorted-permtoArr-ind | proved | all subs proved
| srowsorted-def,
|
| divup2-def | proved | all subs proved
| divup-def,
|
| count1-leq-clean1-ind | proved | all subs proved
| clean1rows-allge,
clean1rows-bounded,
|
| countevn-append-ind | proved | all subs proved
| countevn-rec,
countevn-base,
|
| countevn-zero-ind | proved | all subs proved
| countevn-rec,
countevn-base,
|
| countevn-bounded-ind | proved | all subs proved
| countevn-rec,
countevn-base,
|
| scolsorted-permtoArc-ind | proved | all subs proved
| scolsorted-def,
|
| scolsorted-permcol | proved | all subs proved
| scolsorted-def,
|
| scolsorted-colordered | proved | all subs proved
| scolsorted-def,
|
| rowperms-clean0unchanged | proved | all subs proved
| clean0rows-allls,
clean0rows-notallls,
clean0rows-bounded,
|
| rowperms-clean1unchanged | proved | all subs proved
| clean1rows-allge,
clean1rows-notallge,
clean1rows-bounded,
|
| sortrow-correct | proved | all subs proved
| sort-possible,
rowsincreasing-def,
rowno-updrow,
colno-updrow,
sortrow,
|
| divup-one | proved | all subs proved
| divup-def,
|
| dirtyrows-trivialbound | proved | all subs proved
| dirtyrows-def,
dirtyrowsbound-def,
|
| log2ub-lem | proved | all subs proved
| divup-def,
log2up-def,
|
| count0-leq-clean0-ind | proved | all subs proved
| clean0rows-allls,
clean0rows-bounded,
|
| rowsorted-biggercol-oddbounded | proved | all subs proved
| srowsorted-def,
countodd-rec,
countodd-base,
|
| count-add-even-odd-ind | proved | all subs proved
| countodd-rec,
countevn-rec,
countodd-base,
countevn-base,
|
| log2ub-log2 | proved | all subs proved
| log2up-def,
|
| sortrowsnake-correct | proved | all subs proved
| sort-possible,
srowsorted-def,
colno-updrow,
rowno-updrow,
sortrow,
|
| countodd-append-ind | proved | all subs proved
| countodd-rec,
countodd-base,
|
| countodd-zero-ind | proved | all subs proved
| countodd-rec,
countodd-base,
|
| countodd-bounded-ind | proved | all subs proved
| countodd-rec,
countodd-base,
|
| srowsorted-permrow | proved | all subs proved
| srowsorted-def,
|
| clean0-plus-clean1-bounded | proved | all subs proved
| clean1rows-allge,
clean0rows-allls,
clean0rows-bounded,
clean1rows-bounded,
|
| srowsorted-oddrowordered | proved | all subs proved
| srowsorted-def,
|
| exists-max1column | proved | all subs proved
| exists-max1column-ind,
|
| fullcountodd-range | proved | all subs proved
| countodd-rec,
countodd-base,
|
| dirytrows-zero | proved | all subs proved
| clean1rows-allge,
clean0rows-allls,
dirtyrows-def,
|
| srowsorted-evenrowordered | proved | all subs proved
| srowsorted-def,
|
| fullcountevn-range | proved | all subs proved
| countevn-rec,
countevn-base,
|
| sortrow | axiom | | |
| rowno-updrow | axiom | | |
| colno-updrow | axiom | | |
| sortrows | axiom | | |
| exists-max0column-ind | proved | all subs proved
| |
| shearsort | axiom | | |
| rowsincreasing-def | axiom | | |
| sortedperm-count-splits | proved | all subs proved
| |
| countevn-def | axiom | | |
| countodd-def | axiom | | |
| log2up-def | axiom | | |
| exists-max1column-ind | proved | all subs proved
| |
| sortrowssnake | axiom | | |
| srowsorted-def | axiom | | |
| divup-def | axiom | | |
| dirtyrowsbound-def | axiom | | |
| sortcol | axiom | | |
| rowno-updcol | axiom | | |
| colno-updcol | axiom | | |
| sort-possible | proved | all subs proved
| |
| countodd-base | axiom | | |
| countodd-rec | axiom | | |
| dirtyrows-def | axiom | | |
| clean0rows-notallls | axiom | | |
| clean1rows-notallge | axiom | | |
| clean1rows-bounded | axiom | | |
| clean0rows-bounded | axiom | | |
| clean0rows-allls | axiom | | |
| clean1rows-allge | axiom | | |
| countevn-base | axiom | | |
| countevn-rec | axiom | | |
| sortcols | axiom | | |
| scolsorted-def | axiom | | |