[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 insorted, len-str-01, eq-one, pos-str-01, length-one, pos-str-02, len-app, eqpos, neq-one, len-str,
nat-basic/add-base is used by len-app,
nat-basic/c is used by insorted, len-str-01, eq-one, pos-str-01, length-one, pos-str-02, len-app, eqpos, neq-one, len-str,
nat-basic/eq-01 is used by pos-str-01, pos-str-02, len-app, eqpos,
nat-basic/f 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 eqpos,
nat-basic/s-04 is used by eqpos,
nat-basic/succ is used by len-app,

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 insorted, val-total-01, 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-add is used by pos-str, pos-str-03, pos-str-01, pos-str-02,
list-data/string/l is used by len-str-01, eq-one, eqpos, neq-one, len-str,
list-data/string/length-rest is used by len-str-01, len-str,
list-data/string/size-nil is used by insorted, length-one, len-app,

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 pos-str, pos-str-03, pos-one, less-empty, val-total, exlarger, eq-one, append-eqlen, val-trans, pos-str-01, pos-str-02, less-append, len-app, eqpos, append-eqlen-01, neq-one,
list/string/app is used by pos-one, eq-one, less-append,
list/string/c is used by pos-str, pos-str-03, less-empty, val-total, val-irref, val-trans, pos-str-01, pos-str-02, less-append, len-app, eqpos,
list/string/e is used by val-total, length-one,
list/string/e-01 is used by less-empty, val-total, eqpos,
list/string/first is used by val-total,
list/string/len-01 is used by append-eqlen,
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/len is used by pos-range,
list-del/string/pos-n is used by pos-str-01, pos-str-02, eqpos,
list-del/string/pos-y is used by pos-str, pos-str-03, eqpos,