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

store/javastore/At-same is used by two-way-sort-corr-term,

Used from specification storefuns

storefuns/init-put-06 is used by two-way-sort-corr-term,
storefuns/initdone-05 is used by two-way-sort-corr-term,
storefuns/newjvmref is used by two-way-sort-corr-term,
storefuns/newref-01 is used by two-way-sort-corr-term,
storefuns/refin is used by two-way-sort-corr-term,

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,

Used from specification valuefuns

valuefuns/coerce-bool is used by two-way-sort-corr-term,
valuefuns/coerce-int is used by two-way-sort-corr-term,
valuefuns/val2int-int is used by two-way-sort-corr-term,

Used from specification arr2bitlist

arr2bitlist/booleanarray-get is used by two-way-sort-corr-term,
arr2bitlist/booleanarray-len is used by two-way-sort-corr-term,
arr2bitlist/booleanarray-put is used by two-way-sort-corr-term,
arr2bitlist/getbooleanarray-length is used by two-way-sort-corr-term,
arr2bitlist/issorted-le-all-def is used by two-way-sort-corr-term,
arr2bitlist/okarray-mod is used by two-way-sort-corr-term,
arr2bitlist/bool-less is used by two-way-sort-corr-term,
arr2bitlist/issorted-empty is used by two-way-sort-corr-term,

Used from specification intnat

intnat/num-i2n-ls is used by two-way-sort-corr-term,
intnat/abs-succ-03 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/minus-one 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/rax-04 is used by two-way-sort-corr-term,
intnat/sub-same 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-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/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/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 okfuns

okfuns/okarray-04 is used by two-way-sort-corr-term,
okfuns/okarray-05 is used by two-way-sort-corr-term,
okfuns/okarray-intval-01 is used by two-way-sort-corr-term,
okfuns/okarray-length-02 is used by two-way-sort-corr-term,

Used from specification storekey

storekey/inj-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/lf-02 is used by two-way-sort-corr-term,
nat-basic1/ls-02 is used by two-way-sort-corr-term,
nat-basic1/one 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,

Used from specification int-basic1

int-basic1/forward-pos is used by two-way-sort-corr-term,
int-basic1/irref is used by two-way-sort-corr-term,
int-basic1/ls-01 is used by two-way-sort-corr-term,
int-basic1/numlsf is used by two-way-sort-corr-term,

Used from specification list-perm

list-perm/bitlista/perm-switch is used by two-way-sort-corr-term,
list-perm/bitlista/sym is used by two-way-sort-corr-term,
list-perm/bitlista/empty is used by two-way-sort-corr-term,
list-perm/bitlista/ref is used by two-way-sort-corr-term,

Used from specification oelem

oelem/intlista/lel is used by two-way-sort-corr-term,
oelem/intlista/transitivity is used by two-way-sort-corr-term,

Used from specification javavalue

javavalue/sel-05 is used by two-way-sort-corr-term,
javavalue/test-13 is used by two-way-sort-corr-term,

Used from specification list-data

list-data/bitlista/l is used by two-way-sort-corr-term,
list-data/bitlista/size-01 is used by two-way-sort-corr-term,

Used from specification specialkeys

specialkeys/length-03 is used by two-way-sort-corr-term,

Used from specification javastore

javastore/at-other-16 is used by two-way-sort-corr-term,
javastore/at-other-17 is used by two-way-sort-corr-term,
javastore/length-at is used by two-way-sort-corr-term,

Used from specification addfuns

addfuns/addobj-mode-01 is used by two-way-sort-corr-term,

Used from specification nat

nat/fle-01 is used by two-way-sort-corr-term,
nat/le is used by two-way-sort-corr-term,
nat/le-add is used by two-way-sort-corr-term,
nat/le-ls-simp is used by two-way-sort-corr-term,
nat/le-num-02 is used by two-way-sort-corr-term,
nat/lels is used by two-way-sort-corr-term,
nat/lels-03 is used by two-way-sort-corr-term,
nat/lep-02 is used by two-way-sort-corr-term,
nat/ler is used by two-way-sort-corr-term,
nat/ls-01 is used by two-way-sort-corr-term,
nat/ls-le-simp 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,