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

int-mult/associativity is used by hexbyte-byte,
int-mult/commutativity is used by numhex-rec, hexbyte-byte, hex-rec,
int-mult/numsucc is used by hexbyte-byte,
int-mult/one is used by hexbyte-byte,

Used from specification string-data

string-data/elim is used by numhex-rec, hexbyte-byte, hex-rec,

Used from specification string-less

string-less/Length-empty is used by test-01, hexstring-length, hexbyte-byte,
string-less/Length-rec is used by numhex-rec, hexstring-length, hexbyte-byte, hex-rec,
string-less/len-str-01 is used by test-01,
string-less/len-zero is used by hexbyte-byte,

Used from specification nat

nat/add-num-04 is used by hexbyte-byte,

Used from specification int-abs

int-abs/numadd-01 is used by test-01,
int-abs/numsub is used by numhex-rec, hex-rec,

Used from specification string-append

string-append/assoc is used by numhex-rec, hexstring-length, hexbyte-byte, hex-rec,
string-append/chartostring-01 is used by numhex-rec, hexstring-rec-01, hexstring-length, hexbyte-byte, hex-rec,
string-append/empty is used by hexbyte-byte,
string-append/injectivity is used by numhex-rec,
string-append/one-01 is used by hexbyte-byte,

Used from specification list-data

list-data/intlista/size-01 is used by hexstring-length,

Used from specification list

list/intlista/a is used by hexstring-length, hex-rec,
list/intlista/c is used by hexstring-rec-01, hexstring-length, hex-rec,
list/intlista/len is used by hexstring-length,
list/intlista/len-02 is used by hexstring-length,

Used from specification nat-basic2

nat-basic2/a is used by numhex-rec, hexstring-length, hexbyte-byte, hex-rec,
nat-basic2/c is used by numhex-rec, hexstring-length, hexbyte-byte, hex-rec,
nat-basic2/eq-01 is used by hexstring-length,
nat-basic2/one-03 is used by hexbyte-byte,

Used from specification intnat

intnat/n2i-add is used by numhex-rec, hex-rec,

Used from specification int-basic2

int-basic2/add-a is used by test-01, numhex-rec, hexbyte-byte, hex-rec,
int-basic2/add-c is used by test-01, numhex-rec, hexbyte-byte, hex-rec,
int-basic2/add-in is used by hex-rec,
int-basic2/add-zero is used by numhex-rec, hexbyte-byte, hex-rec,