[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 string-data

string-data/elim is used by pos-str-03, pos-str-02, pos-str-01, pos-str, len-str-01, len-str, append-eqlen-01, append-eqlen,

Used from specification nat

nat/anti is used by val-total-01,
nat/eqle-one is used by eqpos,
nat/lels is used by val-total-01, insorted, eqpos,
nat/lels-01 is used by pos-range,
nat/ler is used by val-total-01,
nat/not-zero is used by insorted,
nat/succ-01 is used by eqpos,

Used from specification string-append

string-append/one is used by val-total,
string-append/rec is used by append-eqlen-01,
string-append/append-base is used by less-append, len-app, append-eqlen-01, append-eqlen,
string-append/assoc is used by val-trans, val-total, sortedchars-divided, pos-str-03, pos-str-02, pos-str-01, pos-str, pos-range, pos-one, neq-one, less-empty, less-append, len-zero, len-str-01, len-str, len-app, exlarger, eqpos, eq-one, append-eqlen-01, append-eqlen,
string-append/chartostring-01 is used by val-trans, val-total, val-irref, pos-str-03, pos-str-02, pos-str-01, pos-str, pos-range, less-empty, less-append, len-zero, len-str-01, len-str, len-app, eqpos, append-eqlen-01, append-eqlen,
string-append/empty-01 is used by pos-one, less-append, eq-one,
string-append/one is used by append-eqlen-01, append-eqlen,
string-append/one-01 is used by length-one,
string-append/rest-one is used by length-one,

Used from specification nat-basic2

nat-basic2/a is used by pos-z, pos-str-02, pos-str-01, pos-range, pos-capital-z, pos-capital-c, pos-capital-b, pos-capital-a, pos-c, pos-b, pos-a, pos-2, pos-1, pos-0, neq-one, length-one, len-zero, len-str-01, len-str, len-app, insorted, eqpos, eq-one, append-eqlen-01, append-eqlen,
nat-basic2/add-base is used by len-app,
nat-basic2/c is used by pos-z, pos-str-02, pos-str-01, pos-range, pos-capital-z, pos-capital-c, pos-capital-b, pos-capital-a, pos-c, pos-b, pos-a, pos-2, pos-1, pos-0, neq-one, length-one, len-zero, len-str-01, len-str, len-app, insorted, eqpos, eq-one, append-eqlen-01, append-eqlen,
nat-basic2/eq is used by append-eqlen-01,
nat-basic2/eq-01 is used by pos-str-02, pos-str-01, len-str-01, len-str, len-app, eqpos, append-eqlen,
nat-basic2/l is used by pos-range,
nat-basic2/one-02 is used by neq-one,
nat-basic2/one-03 is used by eq-one,
nat-basic2/oz is used by pos-range,
nat-basic2/s is used by eqpos,
nat-basic2/z-01 is used by len-zero, eqpos, append-eqlen-01, append-eqlen,

Used from specification nat-basic1

nat-basic1/f is used by pos-range, eqpos,
nat-basic1/lf-02 is used by eqpos,
nat-basic1/one is used by neq-one,