[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,

Used simplifier rules/spec theorems by specification

Used from specification nat-basic

Used from specification nat-even

nat-even/Even is used by countevn-bounded-ind, countodd-bounded-ind, divup2-def,
nat-even/Min-left is used by colsort-dirtyboundhalf, max0column-clean0rowsbounded,
nat-even/even-add is used by countevn-bounded-ind, fullcountevn-range,
nat-even/even-div2 is used by fullcountevn-range,
nat-even/odd-add is used by countodd-bounded-ind, fullcountodd-range,
nat-even/odd-div2 is used by fullcountevn-range,
nat-even/oex is used by countevn-bounded-ind,
nat-even/plus is used by countevn-bounded-ind,
nat-even/Even-new is used by fullcountevn-range,
nat-even/Min-right is used by colsort-dirtyboundhalf, max0column-clean0rowsbounded,
nat-even/Odd is used by count-add-even-odd-ind, countevn-bounded-ind, fullcountevn-range, countodd-bounded-ind, fullcountodd-range, countodd-maxcol0-bounded,
nat-even/eo is used by count-add-even-odd-ind, countevn-bounded-ind, countodd-bounded-ind, fullcountodd-range,
nat-even/eo-01 is used by countevn-bounded-ind, divup-half, countevn-maxcol0-bounded, fullcountevn-range, divup2-def, psortrowssnake-correct, fullcountodd-range, psortrowsnake-correct,
nat-even/eo-02 is used by countevn-bounded-ind, divup-half, fullcountevn-range,
nat-even/even-div2 is used by fullcountevn-range, fullcountodd-range,
nat-even/meven-02 is used by countevn-bounded-ind, divup-half, countodd-bounded-ind, divup2-def,
nat-even/min-a is used by colsort-dirtyboundhalf, max0column-clean0rowsbounded,
nat-even/min-c is used by colsort-dirtyboundhalf, max0column-clean0rowsbounded,
nat-even/min-ls-self1 is used by max0column-clean0rowsbounded,
nat-even/modd-03 is used by countevn-bounded-ind, divup-half, countodd-bounded-ind, divup2-def,
nat-even/odd-div2 is used by divup-half, fullcountevn-range, fullcountodd-range,
nat-even/oe-01 is used by count-add-even-odd-ind, rowsorted-biggercol-oddbounded, countevn-bounded-ind, fullcountevn-range, countodd-bounded-ind, psortrowssnake-correct, fullcountodd-range, srowsorted-oddrowordered, psortrowsnake-correct,
nat-even/oe-02 is used by divup-half, countodd-bounded-ind, fullcountodd-range,
nat-even/ozero is used by fullcountodd-range,
nat-even/plus is used by countevn-bounded-ind, fullcountevn-range, countodd-bounded-ind, fullcountodd-range,

Used from specification tord

tord/irreflexivity is used by pshearsort-correct, dirtyrowsone-rowsincreasing,
tord/Bubblesort-row-rev/lel is used by psortrows-correct,
tord/lel is used by rowsincreasing-allrowsorted-sorted-ind, psortrows-correct,
tord/nen is used by psortrows-correct,
tord/Bubblesort-row-rev/nen is used by colsorted-clean0notls, psortrows-correct,
tord/nll is used by rowsorted-biggercol-oddbounded, dirtyrowsone-rowsincreasing, ordered-rev, psortrows-correct,
tord/Bubblesort-row-rev/nll is used by rowsorted-biggercol-oddbounded, dirtyrowsone-rowsincreasing, ordered-rev, rowsorted-smallercol-evnbounded, psortrows-correct,

Used from specification matrix+array

Used from specification nat

Used from specification matrix-revops

matrix-revops/Bubblesort-row/revselect-def is used by psortrows-correct,
matrix-revops/revselect-def is used by psortrows-correct,

Used from specification nat-pot

nat-pot/Log2def is used by log2ub-lem,
nat-pot/potex is used by log2ub-lem,
nat-pot/Pot2-zero is used by pshearsort-correct,
nat-pot/div-eq-zero is used by divup-half,
nat-pot/inj is used by log2ub-log2,
nat-pot/lemma-ax2 is used by pshearsort-correct, divup-half, log2ub-lem,
nat-pot/lone is used by log2ub-log2, log2ub-zero,
nat-pot/lpot is used by log2ub-log2, log2ub-lem, log2ub-zero,
nat-pot/lsucc-01 is used by log2ub-log2, log2ub-lem,
nat-pot/one is used by log2ub-zero,
nat-pot/zero is used by divup-half, log2ub-log2, log2ub-lem, log2ub-zero,

Used from specification rowcol-upd

rowcol-upd/perm-toArr-toArc is used by colsorted-permtoArr,
rowcol-upd/putcol-getcol is used by psortcols-correct,
rowcol-upd/Bubblesort-row/putcol-getcol is used by psortrowssnake-correct, psortrows-correct,
rowcol-upd/toArc-def is used by colsorted-permtoArr,
rowcol-upd/toArr-def is used by srowsorted-permtoArr, rowsincreasing-allrowsorted-sorted, allperm-permtoArr,
rowcol-upd/colno-updcol is used by psortcols-correct,
rowcol-upd/colno-updrow is used by psortrowssnake-correct, psortrowsnake-correct, psortrows-correct,
rowcol-upd/putcol-id is used by psortcols-correct,
rowcol-upd/putrow-id is used by psortrowssnake-correct, psortrowsnake-correct, psortrows-correct,
rowcol-upd/rowno-updcol is used by psortcols-correct,
rowcol-upd/rowno-updrow is used by psortrowssnake-correct, psortrowsnake-correct, psortrows-correct,
rowcol-upd/toArc-base is used by colsorted-permtoArc-ind,
rowcol-upd/toArc-rec is used by colsorted-permtoArc-ind,
rowcol-upd/toArr-base is used by rowsincreasing-allrowsorted-sorted-ind, srowsorted-permtoArr-ind, allperm-permtoArr-ind,
rowcol-upd/toArr-rec is used by rowsincreasing-allrowsorted-sorted-ind, srowsorted-permtoArr-ind, allperm-permtoArr-ind,

Used from specification list-last

list-last/list-as-arrayinstance/lapp is used by rowsincreasing-allrowsorted-sorted-ind,
list-last/list-as-arrayinstance/last-elim is used by rowsincreasing-allrowsorted-sorted-ind,
list-last/list-as-arrayinstance/rev-length is used by rowsorted-biggercol-oddbounded, ordered-rev, sort-possible,
list-last/list-as-arrayinstance/rev-rev-identity is used by sort-possible,

Used from specification list-data

list-data/oarray-sort/elim-add is used by rowsincreasing-allrowsorted-sorted-ind,
list-data/oarray-sort/l is used by countevn-append-ind, count-add-even-odd-ind, rowsincreasing-allrowsorted-sorted-ind, countevn-bounded-ind, fullcountevn-range, countodd-bounded-ind, ordered-rev, sortedperm-count-splits, fullcountodd-range, countodd-zero-ind, countodd-append-ind, countevn-zero-ind,
list-data/oarray-sort/size-nil is used by rowsincreasing-allrowsorted-sorted-ind,

Used from specification list

list/list-as-arrayinstance/Nil is used by rowsincreasing-allrowsorted-sorted-ind,
list/list-as-arrayinstance/a is used by rowsincreasing-allrowsorted-sorted-ind, srowsorted-permtoArr-ind, colsorted-permtoArc-ind,
list/list-as-arrayinstance/app is used by rowsincreasing-allrowsorted-sorted-ind,
list/list-as-arrayinstance/app-02 is used by rowsincreasing-allrowsorted-sorted-ind,
list/list-as-arrayinstance/c is used by rowsincreasing-allrowsorted-sorted-ind,
list/list-as-arrayinstance/e is used by rowsincreasing-allrowsorted-sorted-ind,
list/list-as-arrayinstance/in-14 is used by rowsincreasing-allrowsorted-sorted-ind,
list/list-as-arrayinstance/in-15 is used by rowsincreasing-allrowsorted-sorted-ind,
list/list-as-arrayinstance/in-rec is used by rowsincreasing-allrowsorted-sorted-ind,
list/list-as-arrayinstance/len-05 is used by rowsincreasing-allrowsorted-sorted-ind,

Used from specification filter-count

filter-count/oarray-sort/count-add-dis is used by colsorted-clean1notls,
filter-count/oarray-sort/count-append-ind is used by count1-leq-clean1, max0column-clean0rowsbounded, count0-leq-clean0, colsorted-samecount-above-clean0, max0column-countcol,
filter-count/oarray-sort/count-bounded is used by max0column-determines-clean1rows,
filter-count/oarray-sort/count-bounded-ind is used by max0column-clean0rowsbounded, colsorted-count-below-clean0rows,
filter-count/oarray-sort/count-def is used by count1-leq-clean1, max0column-clean0rowsbounded, count0-leq-clean0, colsorted-samecount-above-clean0, colsorted-clean1notls, count-add-even-odd, max0column-countcol,
filter-count/oarray-sort/count-size-ind is used by colsorted-count-below-clean0rows, colsorted-clean0notls,
filter-count/oarray-sort/count-true is used by colsorted-clean1notls,
filter-count/oarray-sort/count-zero is used by count0-leq-clean0-ind, count1-leq-clean1-ind, countevn-maxcol0-bounded, max0column-clean0rowsbounded, max0column-determines-clean1rows, colsorted-samecount-above-clean0, colsorted-clean1notls, dirtyrowsone-rowsincreasing, colsorted-clean0notls, countodd-maxcol0-bounded, clean0-plus-clean1-bounded,
filter-count/oarray-sort/countrange-rec is used by rowsorted-biggercol-oddbounded, rowsorted-smallercol-evnbounded,
filter-count/oarray-sort/fullcount-range is used by colsorted-samecount-above-clean0,
filter-count/oarray-sort/perm-count is used by max0column-clean0rowsbounded, colsorted-samecount-above-clean0, colsorted-clean1notls, rowperms-clean0unchanged, sortedperm-count-splits, rowperms-clean1unchanged,
filter-count/oarray-sort/countrange-base is used by count0-leq-clean0-ind, count1-leq-clean1-ind, count-add-even-odd-ind, rowsorted-biggercol-oddbounded, rowsorted-smallercol-evnbounded,
filter-count/oarray-sort/countrange-rec is used by count0-leq-clean0-ind, count1-leq-clean1-ind, count-add-even-odd-ind,

Used from specification list-perm

list-perm/list-as-arrayinstance/in is used by colsorted-clean0notls, psortrows-correct,
list-perm/list-as-arrayinstance/papp is used by srowsorted-permtoArr-ind, colsorted-permtoArc-ind, allperm-permtoArr-ind,
list-perm/list-as-arrayinstance/sym is used by rowperms-clean0unchanged, rowperms-clean1unchanged, colsorted-permtoArr,
list-perm/list-as-arrayinstance/app-end-end is used by srowsorted-permtoArr-ind, colsorted-permtoArc-ind,
list-perm/list-as-arrayinstance/l is used by sort-possible,
list-perm/list-as-arrayinstance/perm-e is used by srowsorted-permtoArr-ind, colsorted-permtoArc-ind, allperm-permtoArr-ind,
list-perm/list-as-arrayinstance/perm-rev-01 is used by sort-possible,
list-perm/list-as-arrayinstance/perm-rev-02 is used by sort-possible,
list-perm/list-as-arrayinstance/ref is used by rowsorted-biggercol-oddbounded, pshearsort-correct, colsorted-count-below-clean0rows, max0column-determines-clean1rows, rowsorted-smallercol-evnbounded,
list-perm/list-as-arrayinstance/trans is used by pshearsort-correct, colsorted-permtoArr,

Used from specification nat-mult

nat-mult/eq is used by colsort-dirtyboundhalf, countevn-maxcol0-bounded, countodd-bounded-ind, countodd-maxcol0-bounded,
nat-mult/mult-c is used by countevn-maxcol0-bounded, countodd-maxcol0-bounded,
nat-mult/zero-02 is used by countevn-maxcol0-bounded,
nat-mult/coef-17 is used by countevn-bounded-ind, divup-half, countodd-bounded-ind,
nat-mult/coef-20 is used by countevn-bounded-ind,
nat-mult/le-05 is used by divup-half,
nat-mult/le-num is used by colsort-dirtyboundhalf, countevn-bounded-ind, countevn-maxcol0-bounded, countodd-maxcol0-bounded,
nat-mult/le2-04 is used by countevn-bounded-ind, countevn-maxcol0-bounded, countodd-maxcol0-bounded,
nat-mult/ls-01 is used by log2ub-lem,
nat-mult/ls2-03 is used by countevn-bounded-ind,
nat-mult/modeq is used by divup-half, countevn-maxcol0-bounded, countodd-bounded-ind, countodd-maxcol0-bounded,
nat-mult/modeq-01 is used by countevn-bounded-ind, divup-half, countevn-maxcol0-bounded, countodd-bounded-ind, divup2-def, countodd-maxcol0-bounded,
nat-mult/modls is used by countevn-bounded-ind,
nat-mult/mult-a is used by colsort-dirtyboundhalf, countevn-bounded-ind, divup-half, countevn-maxcol0-bounded, countodd-bounded-ind, divup2-def, divup-one, log2ub-log2, log2ub-lem, countodd-maxcol0-bounded,
nat-mult/mult-c is used by colsort-dirtyboundhalf, countevn-bounded-ind, divup-half, countevn-maxcol0-bounded, countodd-bounded-ind, divup2-def, divup-one, log2ub-log2, log2ub-lem, countodd-maxcol0-bounded,
nat-mult/numeral-36 is used by divup-half,
nat-mult/one is used by divup-half, divup-one,
nat-mult/one-01 is used by divup-half,
nat-mult/rsucc-02 is used by countevn-bounded-ind, divup-half, countevn-maxcol0-bounded, countodd-bounded-ind, countodd-maxcol0-bounded,
nat-mult/two-02 is used by countevn-bounded-ind, countodd-bounded-ind, divup2-def,
nat-mult/two-ls-01 is used by colsort-dirtyboundhalf, countevn-bounded-ind, log2ub-lem,
nat-mult/two-one-01 is used by countevn-maxcol0-bounded, countodd-maxcol0-bounded,
nat-mult/two-succ-05 is used by colsort-dirtyboundhalf, divup-half,
nat-mult/two-zero-01 is used by divup-half, countevn-maxcol0-bounded, countodd-bounded-ind, log2ub-lem, countodd-maxcol0-bounded,
nat-mult/twole is used by divup-half,
nat-mult/zero is used by divup-half,
nat-mult/zero-01 is used by log2ub-lem,
nat-mult/zero-02 is used by colsort-dirtyboundhalf,
nat-mult/zero-03 is used by log2ub-lem,
nat-mult/zero-06 is used by countevn-bounded-ind,

Used from specification olist

olist/Bubblesort-row-rev-Bubblesort-row-oarray-sort/orderedle-all is used by ordered-rev,
olist/oarray-sort/orderedle-all is used by rowsorted-biggercol-oddbounded, pshearsort-correct, dirtyrowsone-rowsincreasing, ordered-rev, rowsorted-smallercol-evnbounded,
olist/oarray-sort/orderedle-append is used by rowsincreasing-allrowsorted-sorted-ind,
olist/oarray-sort/sort-possible is used by sort-possible,
olist/oarray-sort/le-e is used by rowsincreasing-allrowsorted-sorted-ind,

Used from specification list-del

list-del/list-as-arrayinstance/in-get is used by rowsincreasing-allrowsorted-sorted-ind, colsorted-clean0notls, psortrows-correct,
list-del/list-as-arrayinstance/rev-get is used by rowsorted-biggercol-oddbounded, ordered-rev,
list-del/list-as-arrayinstance/get-zero is used by rowsincreasing-allrowsorted-sorted-ind,

Used from specification nat-div

nat-div/mult is used by divup-half,
nat-div/zero-01 is used by divup-half,
nat-div/div-elim is used by colsort-dirtyboundhalf, countevn-bounded-ind, divup-half, countevn-maxcol0-bounded, countodd-bounded-ind, divup2-def, countodd-maxcol0-bounded,
nat-div/le-div-to-mult is used by colsort-dirtyboundhalf, countevn-bounded-ind, countevn-maxcol0-bounded, countodd-maxcol0-bounded,
nat-div/ls-02 is used by colsort-dirtyboundhalf,
nat-div/mult-01 is used by divup-half,
nat-div/one is used by log2ub-lem,
nat-div/one-01 is used by divup-one,
nat-div/two-loup-09 is used by divup2-def,
nat-div/two-mdiv2-02 is used by colsort-dirtyboundhalf, countevn-maxcol0-bounded, divup2-def, countodd-maxcol0-bounded,
nat-div/two-rec is used by countevn-bounded-ind, divup-half, fullcountevn-range, fullcountodd-range,
nat-div/two-two-01 is used by countodd-maxcol0-bounded,
nat-div/two-twosucc-02 is used by divup2-def,
nat-div/two-zero-01-01 is used by colsort-dirtyboundhalf, countevn-maxcol0-bounded, countodd-maxcol0-bounded,
nat-div/zero-01 is used by divup-half, log2ub-lem, countodd-maxcol0-bounded,

Used from specification matrix

matrix/extension is used by psortrowsnake-correct,

Used from specification olist-min-max

olist-min-max/oarray-sort/ordered-count-splits is used by colsorted-clean1notls, sortedperm-count-splits,

Used from specification Bubblesort-col

Bubblesort-col/psortcol-correct is used by psortcols-correct,
Bubblesort-col/Bubblesort-row-rev-Bubblesort-row/psortcol-correct is used by psortrowsnake-correct,
Bubblesort-col/Bubblesort-row/psortcol-correct is used by psortrowsnake-correct, psortrows-correct,

Used from specification array

array/Extension is used by rowsincreasing-allrowsorted-sorted-ind,