[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 int-basic2

int-basic2/add-a is used by two_way_sort-corr-term,
int-basic2/add-c is used by two_way_sort-corr-term,
int-basic2/add-in is used by two_way_sort-corr-term,
int-basic2/ls is used by two_way_sort-corr-term,

Used from specification intnat

intnat/num-i2n-le-02 is used by two_way_sort-corr-term,
intnat/num-i2n-ls-02 is used by two_way_sort-corr-term,
intnat/num-n2i-ls-06 is used by two_way_sort-corr-term,
intnat/abs is used by two_way_sort-corr-term,
intnat/abs-eq is used by two_way_sort-corr-term,
intnat/abs-zero is used by two_way_sort-corr-term,
intnat/labs is used by two_way_sort-corr-term,
intnat/labs-01 is used by two_way_sort-corr-term,
intnat/le is used by two_way_sort-corr-term,
intnat/ls-int-ls-nat is used by two_way_sort-corr-term,
intnat/n2i-add is used by two_way_sort-corr-term,
intnat/n2n is used by two_way_sort-corr-term,
intnat/nat2int is used by two_way_sort-corr-term,
intnat/nat2int-04 is used by two_way_sort-corr-term,
intnat/num-n2i-ls-02 is used by two_way_sort-corr-term,
intnat/num-n2i-ls-07 is used by two_way_sort-corr-term,
intnat/pos-int is used by two_way_sort-corr-term,
intnat/rax-04 is used by two_way_sort-corr-term,

Used from specification int-abs

int-abs/Sub-def is used by two_way_sort-corr-term,
int-abs/abs-03 is used by two_way_sort-corr-term,
int-abs/abs-04 is used by two_way_sort-corr-term,
int-abs/abs-19 is used by two_way_sort-corr-term,
int-abs/absle is used by two_way_sort-corr-term,
int-abs/anti is used by two_way_sort-corr-term,
int-abs/elim-sub is used by two_way_sort-corr-term,
int-abs/forward-le is used by two_way_sort-corr-term,
int-abs/forward-le-01 is used by two_way_sort-corr-term,
int-abs/forward-le-05 is used by two_way_sort-corr-term,
int-abs/forward-lele is used by two_way_sort-corr-term,
int-abs/forward-lels is used by two_way_sort-corr-term,
int-abs/forward-lsle is used by two_way_sort-corr-term,
int-abs/le-add is used by two_way_sort-corr-term,
int-abs/le-add-03 is used by two_way_sort-corr-term,
int-abs/lels is used by two_way_sort-corr-term,
int-abs/lels-01 is used by two_way_sort-corr-term,
int-abs/lels-02 is used by two_way_sort-corr-term,
int-abs/lels-03 is used by two_way_sort-corr-term,
int-abs/lenls is used by two_way_sort-corr-term,
int-abs/lep-01 is used by two_way_sort-corr-term,
int-abs/ler is used by two_way_sort-corr-term,
int-abs/les is used by two_way_sort-corr-term,
int-abs/mone-06 is used by two_way_sort-corr-term,
int-abs/numadd-01 is used by two_way_sort-corr-term,
int-abs/numle-02 is used by two_way_sort-corr-term,
int-abs/numleledel-01 is used by two_way_sort-corr-term,
int-abs/numls-02 is used by two_way_sort-corr-term,
int-abs/sub-eq is used by two_way_sort-corr-term,
int-abs/sub-ls is used by two_way_sort-corr-term,
int-abs/succ-01 is used by two_way_sort-corr-term,
int-abs/succ-02 is used by two_way_sort-corr-term,
int-abs/zero-gels-04 is used by two_way_sort-corr-term,

Used from specification nat-basic1

nat-basic1/f is used by two_way_sort-corr-term,
nat-basic1/lf-01 is used by two_way_sort-corr-term,
nat-basic1/ref-1 is used by two_way_sort-corr-term,
nat-basic1/zero is used by two_way_sort-corr-term,
nat-basic1/zero-01 is used by two_way_sort-corr-term,

Used from specification int-basic1

int-basic1/irref is used by two_way_sort-corr-term,
int-basic1/ls-01 is used by two_way_sort-corr-term,

Used from specification list-perm

list-perm/boollist/perm-switch is used by two_way_sort-corr-term,
list-perm/boollist/sym is used by two_way_sort-corr-term,
list-perm/boollist/ref is used by two_way_sort-corr-term,

Used from specification array

array/boolarr/Put-other is used by two_way_sort-corr-term,
array/boolarr/Put-same is used by two_way_sort-corr-term,
array/boolarr/Size-put is used by two_way_sort-corr-term,
array/boolarr/cgetput is used by two_way_sort-corr-term,
array/boolarr/cngetput is used by two_way_sort-corr-term,

Used from specification nat

nat/add-01 is used by two_way_sort-corr-term,
nat/elim-pred-c is used by two_way_sort-corr-term,
nat/eq is used by two_way_sort-corr-term,
nat/eqle-one is used by two_way_sort-corr-term,
nat/fle is used by two_way_sort-corr-term,
nat/fle-01 is used by two_way_sort-corr-term,
nat/le is used by two_way_sort-corr-term,
nat/le-ls-simp is used by two_way_sort-corr-term,
nat/le-sum is used by two_way_sort-corr-term,
nat/lels is used by two_way_sort-corr-term,
nat/lels-01 is used by two_way_sort-corr-term,
nat/les is used by two_way_sort-corr-term,
nat/let is used by two_way_sort-corr-term,
nat/ls-01 is used by two_way_sort-corr-term,
nat/succ-01 is used by two_way_sort-corr-term,

Used from specification nat-basic2

nat-basic2/a is used by two_way_sort-corr-term,
nat-basic2/c is used by two_way_sort-corr-term,
nat-basic2/eq-01 is used by two_way_sort-corr-term,
nat-basic2/l is used by two_way_sort-corr-term,
nat-basic2/l-02 is used by two_way_sort-corr-term,
nat-basic2/oz is used by two_way_sort-corr-term,
nat-basic2/s is used by two_way_sort-corr-term,
nat-basic2/z is used by two_way_sort-corr-term,

Used from specification arr2list

arr2list/arr2list-get is used by two_way_sort-corr-term,
arr2list/arr2list-put is used by two_way_sort-corr-term,
arr2list/arr2list-len is used by two_way_sort-corr-term,
arr2list/bool-less is used by two_way_sort-corr-term,
arr2list/isperm-def is used by two_way_sort-corr-term,
arr2list/issorted-le-all-def is used by two_way_sort-corr-term,