[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

allperm-permtoArr(6,3)colno-updrow(0,0)colsorted-samecount-above-clean0(25,13)countevn-def(0,0)countodd-zero-ind(13,4)divup2-def(8,4)log2up-def(0,0)psortcols-correct(18,9)rowperms-clean1unchanged(23,11)srowsorted-dirtyboundunchanged(7,4)
allperm-permtoArr-ind(11,4)colsort-dirtyboundhalf(64,29)count-add-even-odd(6,4)countevn-maxcol0-bounded(46,20)dirtyrows-def(0,0)exists-max0column(3,2)max0column-clean0rowsbounded(49,26)psortrows(0,0)rowperms-dirtyrowsunchanged(12,4)srowsorted-evenrowordered(5,2)
clean0-plus-clean1-bounded(34,13)colsorted-clean0notls(28,14)count-add-even-odd-ind(16,2)countevn-rec(0,0)dirtyrows-trivialbound(4,2)exists-max0column-ind(11,6)max0column-countcol(6,5)psortrows-correct(46,26)rowsincreasing-allrowsorted-sorted(5,2)srowsorted-oddrowordered(5,2)
clean0rows-allls(0,0)colsorted-clean1notls(30,14)count0-leq-clean0(7,3)countevn-zero-ind(12,4)dirtyrowsbound-def(0,0)exists-max1column(3,2)max0column-countcol-big-odd(9,3)psortrowsnake(0,0)rowsincreasing-allrowsorted-sorted-ind(32,14)srowsorted-permrow(4,1)
clean0rows-bounded(0,0)colsorted-colordered(4,1)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)psortrowsnake-correct(13,5)rowsincreasing-def(0,0)srowsorted-permtoArr(5,3)
clean0rows-notallls(0,0)colsorted-count-below-clean0rows(10,5)count1-leq-clean1(9,3)countodd-base(0,0)dirytrows-leone(22,12)fullcountevn-range(41,16)max0column-determines-clean1rows(33,13)psortrowssnake(0,0)rowsorted-biggercol-oddbounded(34,13)srowsorted-permtoArr-ind(11,6)
clean1rows-allge(0,0)colsorted-def(0,0)count1-leq-clean1-ind(14,6)countodd-bounded-ind(65,26)dirytrows-zero(7,3)fullcountodd-range(27,12)ordered-rev(35,11)psortrowssnake-correct(23,12)rowsorted-smallercol-evnbounded(17,9)
clean1rows-bounded(0,0)colsorted-permcol(5,1)countevn-append-ind(7,3)countodd-def(0,0)divup-def(0,0)log2ub-lem(12,7)pshearsort(0,0)rowno-updcol(0,0)sort-possible(9,4)
clean1rows-notallge(0,0)colsorted-permtoArc-ind(11,6)countevn-base(0,0)countodd-maxcol0-bounded(43,20)divup-half(58,23)log2ub-log2(5,4)pshearsort-correct(51,13)rowno-updrow(0,0)sortedperm-count-splits(4,2)
colno-updcol(0,0)colsorted-permtoArr(10,7)countevn-bounded-ind(39,16)countodd-rec(0,0)divup-one(2,1)log2ub-zero(4,2)psortcols(0,0)rowperms-clean0unchanged(17,8)srowsorted-def(0,0)