[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Theorem base summary for Specification ShearSort

clean0-plus-clean1-bounded(34,13)count-add-even-odd-ind(16,2)countevn-rec(0,0)dirtyrows-trivialbound(4,2)exists-max0column-ind(11,6)max0column-countcol(6,5)rowsorted-biggercol-oddbounded(34,13)scolsorted-permtoArr(10,7)sortrow(0,0)srowsorted-oddrowordered(5,2)
clean0rows-allls(0,0)count0-leq-clean0(7,3)countevn-zero-ind(12,4)dirtyrowsbound-def(0,0)exists-max1column(3,2)max0column-countcol-big-odd(9,3)rowsorted-smallercol-evnbounded(17,9)scolsorted-samecount-above-clean0(25,13)sortrow-correct(70,27)srowsorted-permrow(4,1)
clean0rows-bounded(0,0)count0-leq-clean0-ind(14,5)countodd-append-ind(7,3)dirtyrowsone-rowsincreasing(59,30)exists-max1column-ind(11,6)max0column-countcol-small-even(3,2)scolsort-dirtyboundhalf(64,29)shearsort(0,0)sortrows(0,0)srowsorted-permtoArr(5,3)
clean0rows-notallls(0,0)count1-leq-clean1(9,3)countodd-base(0,0)dirytrows-leone(22,12)fullcountevn-range(41,16)max0column-determines-clean1rows(33,13)scolsorted-clean0notls(28,14)shearsort-correct(43,12)sortrows-correct(10,1)srowsorted-permtoArr-ind(11,6)
clean1rows-allge(0,0)count1-leq-clean1-ind(14,6)countodd-bounded-ind(65,26)dirytrows-zero(7,3)fullcountodd-range(27,12)rowno-updcol(0,0)scolsorted-clean1notls(30,14)sort-possible(13,6)sortrowsnake-correct(27,10)
clean1rows-bounded(0,0)countevn-append-ind(7,3)countodd-def(0,0)divup-def(0,0)log2ub-lem(12,7)rowno-updrow(0,0)scolsorted-colordered(4,1)sortcol(0,0)sortrowssnake(0,0)
clean1rows-notallge(0,0)countevn-base(0,0)countodd-maxcol0-bounded(43,20)divup-half(58,23)log2ub-log2(5,4)rowperms-clean0unchanged(17,8)scolsorted-count-below-clean0rows(10,5)sortcol-correct(30,12)sortrowssnake-correct(11,1)
colno-updcol(0,0)countevn-bounded-ind(39,16)countodd-rec(0,0)divup-one(2,1)log2ub-zero(4,2)rowperms-clean1unchanged(23,11)scolsorted-def(0,0)sortcols(0,0)srowsorted-def(0,0)
colno-updrow(0,0)countevn-def(0,0)countodd-zero-ind(13,4)divup2-def(8,4)log2up-def(0,0)rowperms-dirtyrowsunchanged(12,4)scolsorted-permcol(5,1)sortcols-correct(12,1)srowsorted-dirtyboundunchanged(7,4)
count-add-even-odd(6,4)countevn-maxcol0-bounded(46,20)dirtyrows-def(0,0)exists-max0column(3,2)max0column-clean0rowsbounded(71,37)rowsincreasing-def(0,0)scolsorted-permtoArc-ind(11,6)sortedperm-count-splits(4,2)srowsorted-evenrowordered(5,2)