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: |
|---|
| pshearsort-correct | proved | all subs proved
| colsort-dirtyboundhalf,
colsorted-def,
dirtyrowsone-rowsincreasing,
psortrows-correct,
log2ub-lem,
divup-half,
srowsorted-dirtyboundunchanged,
srowsorted-def,
psortcols-correct,
psortrowssnake-correct,
log2ub-zero,
dirtyrows-trivialbound,
divup-one,
pshearsort,
|
| colsort-dirtyboundhalf | proved | all subs proved
| colsorted-def,
countodd-maxcol0-bounded,
countevn-maxcol0-bounded,
clean0rows-bounded,
count-add-even-odd-ind,
max0column-countcol,
divup-def,
max0column-determines-clean1rows,
max0column-clean0rowsbounded,
exists-max0column,
dirtyrows-def,
dirtyrowsbound-def,
|
| max0column-clean0rowsbounded | proved | all subs proved
| colsorted-permcol,
colsorted-colordered,
colsorted-clean0notls,
count0-leq-clean0-ind,
count-add-even-odd-ind,
max0column-countcol-big-odd,
sortedperm-count-splits,
max0column-countcol-small-even,
clean0rows-notallls,
clean0rows-bounded,
|
| 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
| colsorted-samecount-above-clean0,
colsorted-count-below-clean0rows,
clean0rows-bounded,
|
| colsorted-count-below-clean0rows | proved | all subs proved
| colsorted-colordered,
colsorted-clean0notls,
count0-leq-clean0,
sortedperm-count-splits,
clean0rows-bounded,
|
| colsorted-samecount-above-clean0 | proved | all subs proved
| colsorted-permcol,
colsorted-clean0notls,
clean0rows-allls,
clean0rows-bounded,
|
| psortrowssnake-correct | proved | all subs proved
| ordered-rev,
srowsorted-def,
srowsorted-permtoArr,
psortrowsnake-correct,
psortrowssnake,
|
| psortcols-correct | proved | all subs proved
| colsorted-permtoArr,
colsorted-def,
psortcols,
|
| srowsorted-dirtyboundunchanged | proved | all subs proved
| srowsorted-permrow,
rowperms-dirtyrowsunchanged,
dirtyrowsbound-def,
|
| psortrows-correct | proved | all subs proved
| rowsincreasing-def,
rowsincreasing-allrowsorted-sorted,
allperm-permtoArr,
psortrows,
|
| dirtyrowsone-rowsincreasing | proved | all subs proved
| colsorted-def,
dirytrows-leone,
rowsincreasing-def,
dirtyrowsbound-def,
|
| colsorted-clean0notls | proved | all subs proved
| colsorted-def,
count0-leq-clean0,
sortedperm-count-splits,
count0-leq-clean0-ind,
clean0rows-notallls,
clean0rows-bounded,
|
| colsorted-clean1notls | proved | all subs proved
| colsorted-permcol,
colsorted-colordered,
colsorted-def,
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,
|
| log2ub-zero | proved | all subs proved
| log2ub-log2,
|
| divup-half | proved | all subs proved
| divup-def,
divup2-def,
|
| colsorted-permtoArr | proved | all subs proved
| colsorted-permtoArc-ind,
|
| count1-leq-clean1 | proved | all subs proved
| clean1rows-bounded,
count1-leq-clean1-ind,
|
| srowsorted-permtoArr | proved | all subs proved
| srowsorted-permtoArr-ind,
|
| 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,
|
| rowsincreasing-allrowsorted-sorted | proved | all subs proved
| rowsincreasing-allrowsorted-sorted-ind,
|
| count-add-even-odd | proved | all subs proved
| count-add-even-odd-ind,
countodd-def,
countevn-def,
|
| 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,
|
| rowsorted-smallercol-evnbounded | proved | all subs proved
| srowsorted-def,
countevn-rec,
countevn-base,
|
| srowsorted-permtoArr-ind | proved | all subs proved
| srowsorted-def,
|
| 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,
|
| 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,
|
| rowperms-clean0unchanged | proved | all subs proved
| clean0rows-allls,
clean0rows-notallls,
clean0rows-bounded,
|
| rowperms-clean1unchanged | proved | all subs proved
| clean1rows-allge,
clean1rows-notallge,
clean1rows-bounded,
|
| colsorted-colordered | proved | all subs proved
| colsorted-def,
|
| colsorted-permcol | proved | all subs proved
| colsorted-def,
|
| psortrowsnake-correct | proved | all subs proved
| psortrowsnake,
|
| 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,
|
| count0-leq-clean0-ind | proved | all subs proved
| clean0rows-allls,
clean0rows-bounded,
|
| log2ub-log2 | proved | all subs proved
| log2up-def,
|
| 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,
|
| rowsincreasing-allrowsorted-sorted-ind | proved | all subs proved
| rowsincreasing-def,
|
| allperm-permtoArr | proved | all subs proved
| allperm-permtoArr-ind,
|
| clean0-plus-clean1-bounded | proved | all subs proved
| clean1rows-allge,
clean0rows-allls,
clean0rows-bounded,
clean1rows-bounded,
|
| colsorted-permtoArc-ind | proved | all subs proved
| colsorted-def,
|
| 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,
|
| pshearsort | axiom | | |
| psortcols | axiom | | |
| exists-max0column-ind | proved | all subs proved
| |
| psortrowssnake | axiom | | |
| ordered-rev | proved | all subs proved
| |
| countevn-def | axiom | | |
| countodd-def | axiom | | |
| sortedperm-count-splits | proved | all subs proved
| |
| log2up-def | axiom | | |
| exists-max1column-ind | proved | all subs proved
| |
| srowsorted-def | axiom | | |
| divup-def | axiom | | |
| dirtyrowsbound-def | axiom | | |
| countodd-base | axiom | | |
| countodd-rec | axiom | | |
| psortrowsnake | axiom | | |
| psortrows | axiom | | |
| rowsincreasing-def | axiom | | |
| allperm-permtoArr-ind | proved | all subs proved
| |
| 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 | | |
| colsorted-def | axiom | | |