[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-less-new

string-less-new/len-app is used by neq-one, eq-one,
string-less-new/len-zero is used by neq-one, len-str-01, len-str, eqpos, eq-one,
string-less-new/pos-range is used by pos-range,

Used from specification nat

nat/anti is used by val-total-01,
nat/eq-02 is used by len-str-01, len-str,
nat/eqle-one is used by eqpos,
nat/lels is used by val-total-01, insorted, eqpos,
nat/lels-01 is used by len-str-01, len-str,
nat/ler is used by val-total-01,
nat/not-zero is used by insorted,
nat/pred-03 is used by len-str-01, len-str,
nat/succ-01 is used by eqpos,

Used from specification list-data

list-data/string-new/elim-list is used by pos-str-03, pos-str-02, pos-str-01, pos-str,
list-data/string-new/length-rest is used by len-str-01, len-str,
list-data/string-new/size-01 is used by length-one, len-zero, len-app, insorted,

Used from specification list

list/string-new/firsteq is used by val-total,
list/string-new/Nil is used by val-total, less-append, len-app,
list/string-new/a is used by val-trans, val-total, sortedchars-divided, pos-str-03, pos-str-02, pos-str-01, pos-str, pos-one, neq-one, less-empty, less-append, len-zero, len-app, exlarger, eqpos, eq-one, append-eqlen-01, append-eqlen,
list/string-new/app is used by pos-one, less-append, eq-one,
list/string-new/c is used by val-trans, val-total, val-irref, pos-str-03, pos-str-02, pos-str-01, pos-str, less-empty, less-append, len-zero, len-app, eqpos,
list/string-new/e is used by val-total, length-one,
list/string-new/e-01 is used by val-total, less-empty, eqpos,
list/string-new/first is used by val-total,
list/string-new/len-01 is used by append-eqlen,
list/string-new/len-05 is used by len-zero, len-app, eqpos,
list/string-new/len-06 is used by append-eqlen-01,
list/string-new/rest is used by val-total, length-one,

Used from specification nat-basic2

nat-basic2/a is used by pos-z, pos-str-02, pos-str-01, 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,
nat-basic2/add-base is used by len-app,
nat-basic2/c is used by pos-z, pos-str-02, pos-str-01, 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,
nat-basic2/eq-01 is used by pos-str-02, pos-str-01, len-app, eqpos,
nat-basic2/one-02 is used by neq-one,
nat-basic2/one-03 is used by eq-one,
nat-basic2/s is used by eqpos,
nat-basic2/succ is used by len-zero, len-app, eqpos,
nat-basic2/z-01 is used by len-zero, eqpos,

Used from specification nat-basic1

nat-basic1/f is used by eqpos,
nat-basic1/lf-02 is used by eqpos,
nat-basic1/one is used by neq-one,
nat-basic1/one-01 is used by len-str-01, len-str,

Used from specification list-del

list-del/string-new/pos-n is used by eqpos,
list-del/string-new/pos-y is used by pos-one,
list-del/string-new/pos-n is used by pos-str-02, pos-str-01, eqpos,
list-del/string-new/pos-y is used by pos-str-03, pos-str, eqpos,