[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 scolsort-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/Min-right is used by scolsort-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, fullcountodd-range,
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 scolsort-dirtyboundhalf, max0column-clean0rowsbounded,
nat-even/min-c is used by scolsort-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, fullcountodd-range, srowsorted-oddrowordered,
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,
nat-even/zero is used by fullcountevn-range,

Used from specification matrix+array

Used from specification nat

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 shearsort-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 divup-half, shearsort-correct, 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/overwrite-row is used by sortrowsnake-correct,
rowcol-upd/perm-toArr-toArc is used by scolsorted-permtoArr,
rowcol-upd/perm-updcol is used by sortcol-correct,
rowcol-upd/perm-updrow is used by sortrowsnake-correct,
rowcol-upd/rev-get is used by rowsorted-biggercol-oddbounded,
rowcol-upd/toArc-def is used by scolsorted-permtoArr,
rowcol-upd/toArr-def is used by srowsorted-permtoArr, sortrows-correct,
rowcol-upd/overwrite-col is used by sortcol-correct,
rowcol-upd/overwrite-row is used by sortrow-correct,
rowcol-upd/perm-updrow is used by sortrow-correct,
rowcol-upd/toArc-base is used by scolsorted-permtoArc-ind,
rowcol-upd/toArc-rec is used by scolsorted-permtoArc-ind,
rowcol-upd/toArr-base is used by sortrow-correct, srowsorted-permtoArr-ind, sortrows-correct,
rowcol-upd/toArr-outside-gen is used by sortrow-correct,
rowcol-upd/toArr-rec is used by sortrow-correct, srowsorted-permtoArr-ind, sortrows-correct,
rowcol-upd/updrow-sel is used by sortrow-correct,

Used from specification list-last

list-last/oarray-sort/lapp is used by sortrow-correct,
list-last/oarray-sort/last-elim is used by sortrow-correct,
list-last/oarray-sort/rev-length is used by rowsorted-biggercol-oddbounded, sort-possible,
list-last/oarray-sort/rev-rev-identity is used by sort-possible,

Used from specification list-data

list-data/oarray-sort/elim-add is used by sortrow-correct,
list-data/oarray-sort/elim-list-c is used by sortrow-correct,
list-data/oarray-sort/l is used by countevn-append-ind, sortrow-correct, count-add-even-odd-ind, countevn-bounded-ind, fullcountevn-range, countodd-bounded-ind, sortedperm-count-splits, fullcountodd-range, countodd-zero-ind, countodd-append-ind, countevn-zero-ind,
list-data/oarray-sort/size-nil is used by sortrow-correct,

Used from specification list

list/oarray-sort/Nil is used by sortrow-correct,
list/oarray-sort/a is used by sortrow-correct, srowsorted-permtoArr-ind, scolsorted-permtoArc-ind,
list/oarray-sort/app is used by sortrow-correct,
list/oarray-sort/c is used by sortrow-correct,
list/oarray-sort/e-01 is used by sortrow-correct,
list/oarray-sort/in-15 is used by sortrow-correct,
list/oarray-sort/in-rec is used by sortrow-correct,
list/oarray-sort/len is used by sortrow-correct,
list/oarray-sort/len-02 is used by sortrow-correct,
list/oarray-sort/len-05 is used by sortrow-correct,

Used from specification filter-count

filter-count/oarray-sort/count-add-dis is used by scolsorted-clean1notls,
filter-count/oarray-sort/count-append-ind is used by count1-leq-clean1, scolsorted-samecount-above-clean0, max0column-clean0rowsbounded, count0-leq-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 scolsorted-count-below-clean0rows, max0column-clean0rowsbounded,
filter-count/oarray-sort/count-def is used by count1-leq-clean1, scolsorted-samecount-above-clean0, max0column-clean0rowsbounded, count0-leq-clean0, scolsorted-clean1notls, count-add-even-odd, max0column-countcol,
filter-count/oarray-sort/count-size-ind is used by scolsorted-count-below-clean0rows, scolsorted-clean0notls,
filter-count/oarray-sort/count-true is used by scolsorted-clean1notls,
filter-count/oarray-sort/count-zero is used by count0-leq-clean0-ind, count1-leq-clean1-ind, countevn-maxcol0-bounded, scolsorted-samecount-above-clean0, max0column-clean0rowsbounded, scolsorted-clean1notls, max0column-determines-clean1rows, dirtyrowsone-rowsincreasing, scolsorted-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 scolsorted-samecount-above-clean0,
filter-count/oarray-sort/perm-count is used by scolsorted-samecount-above-clean0, max0column-clean0rowsbounded, scolsorted-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/oarray-sort/in is used by sortrow-correct, scolsorted-clean0notls,
list-perm/oarray-sort/papp is used by srowsorted-permtoArr-ind, scolsorted-permtoArc-ind,
list-perm/oarray-sort/sym is used by scolsorted-permtoArr, rowperms-clean0unchanged, sort-possible, rowperms-clean1unchanged,
list-perm/oarray-sort/trans is used by sortrowsnake-correct,
list-perm/oarray-sort/app-end-end is used by srowsorted-permtoArr-ind, scolsorted-permtoArc-ind,
list-perm/oarray-sort/in-01 is used by sortrow-correct,
list-perm/oarray-sort/neq is used by sortrowsnake-correct, sortcol-correct,
list-perm/oarray-sort/perm-e is used by srowsorted-permtoArr-ind, scolsorted-permtoArc-ind,
list-perm/oarray-sort/perm-rev-01 is used by sort-possible,
list-perm/oarray-sort/ref is used by scolsorted-count-below-clean0rows, sortrow-correct, rowsorted-biggercol-oddbounded, max0column-determines-clean1rows, sortrows-correct, shearsort-correct, sortrowssnake-correct, rowsorted-smallercol-evnbounded, sortcols-correct,
list-perm/oarray-sort/trans is used by scolsorted-permtoArr, sortrows-correct, shearsort-correct, sortcol-correct,

Used from specification nat-mult

nat-mult/eq is used by scolsort-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 scolsort-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 scolsort-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 scolsort-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 scolsort-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 scolsort-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 scolsort-dirtyboundhalf,
nat-mult/zero-03 is used by log2ub-lem,
nat-mult/zero-06 is used by countevn-bounded-ind,

Used from specification oelem

oelem/irreflexivity is used by shearsort-correct, dirtyrowsone-rowsincreasing,
oelem/lel is used by sortrow-correct,
oelem/nll is used by sortrow-correct, rowsorted-biggercol-oddbounded, dirtyrowsone-rowsincreasing, rowsorted-smallercol-evnbounded,
oelem/nnn is used by rowsorted-smallercol-evnbounded,

Used from specification olist

olist/oarray-sort/ordered-append is used by sortrow-correct,
olist/oarray-sort/orderedle-all is used by rowsorted-biggercol-oddbounded, shearsort-correct, dirtyrowsone-rowsincreasing, rowsorted-smallercol-evnbounded,
olist/oarray-sort/sort-possible is used by sort-possible,
olist/oarray-sort/le-e is used by sortrows-correct,

Used from specification list-del

list-del/oarray-sort/get-numrec is used by sortrow-correct,
list-del/oarray-sort/in-get is used by sortrow-correct, scolsorted-clean0notls,
list-del/oarray-sort/get-in is used by sortrow-correct,
list-del/oarray-sort/get-last is used by sortrow-correct,
list-del/oarray-sort/get-zero is used by sortrow-correct,

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 scolsort-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 scolsort-dirtyboundhalf, countevn-bounded-ind, countevn-maxcol0-bounded, countodd-maxcol0-bounded,
nat-div/ls-02 is used by scolsort-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 scolsort-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 scolsort-dirtyboundhalf, countevn-maxcol0-bounded, countodd-maxcol0-bounded,
nat-div/zero-01 is used by divup-half, log2ub-lem, countodd-maxcol0-bounded,

Used from specification olist-min-max

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

Used from specification array

array/Extension is used by sortrow-correct,