[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 nat-basic

nat-basic/a is used by pos-str-02, pos-str-01, neq-one, length-one, len-zero, len-str-01, len-str, len-app, insorted, eqpos, eq-one,
nat-basic/add-base is used by len-app,
nat-basic/c is used by pos-str-02, pos-str-01, neq-one, length-one, len-zero, len-str-01, len-str, len-app, insorted, eqpos, eq-one,
nat-basic/eq-01 is used by pos-str-02, pos-str-01, len-app, eqpos,
nat-basic/f is used by val-trans-01, eqpos,
nat-basic/lf-02 is used by eqpos,
nat-basic/one is used by neq-one,
nat-basic/one-01 is used by len-str-01, len-str,
nat-basic/one-05 is used by neq-one,
nat-basic/one-06 is used by eq-one,
nat-basic/oz is used by len-zero, eqpos,
nat-basic/ref is used by val-irref-01,
nat-basic/s-04 is used by eqpos,
nat-basic/succ is used by val-trans-01, len-app,
nat-basic/trans is used by val-trans-01,
nat-basic/trans-01 is used by val-trans-01,

Used from specification string-less

string-less/len-app is used by neq-one, len-zero, eqpos, eq-one,
string-less/len-zero is used by neq-one, len-str-01, len-str, eqpos, eq-one,
string-less/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/le-def is used by len-str-01, len-str,
nat/lels is used by val-total-01, insorted, eqpos,
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/elim-list is used by pos-str-03, pos-str-02, pos-str-01, pos-str,
list-data/string/length-rest is used by len-str-01, len-str,
list-data/string/size-01 is used by length-one, len-zero, len-app, insorted,

Used from specification list

list/string/firsteq is used by val-total,
list/string/Nil is used by val-total, less-append, len-app,
list/string/a is used by val-trans, val-total, 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/app is used by pos-one, less-append, eq-one,
list/string/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/e is used by val-total, length-one,
list/string/e-01 is used by val-total, pos-str-02, pos-str-01, less-empty, eqpos,
list/string/first is used by val-total,
list/string/len-01 is used by append-eqlen,
list/string/len-02 is used by len-zero,
list/string/len-05 is used by len-app,
list/string/len-06 is used by append-eqlen-01,
list/string/rest is used by val-total, length-one,

Used from specification list-del

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