[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

nat/sub-add is used by split-first,
nat/elim-pred-c is used by split-first,
nat/elim-sub is used by split-rest,
nat/le-ls-simp is used by split-rest,
nat/le-num-06 is used by len-04,
nat/le-one is used by split-first,
nat/lels is used by len-04,
nat/lels-01 is used by split-rest, split-first,
nat/lep is used by split-rest, split-first,
nat/lep-02 is used by len-04,
nat/leprf is used by split-first,
nat/lez is used by split-first,
nat/lez-01 is used by split-first,
nat/ls-03 is used by split-rest,
nat/not-zero is used by split-first,
nat/pred-03 is used by split-first,
nat/succ-01 is used by len-04,

Used from specification list-data

list-data/disj-1 is used by e-01, e,
list-data/elim-1 is used by first-app,
list-data/elim-list-c is used by rest-01, onein, len-last-rest, inapp, in-rec, in-09, in-08, in-07, firstrest, firsteq-01, firsteq, first-app, first-02, first-01, c-02,
list-data/f is used by len-02, c-03, c, a,
list-data/fr-02 is used by fr,
list-data/inj-1 is used by c-06, c-04, c-03, app-01,
list-data/l is used by unequal, split-first, len-03, len-01, e-04, append-size-less,
list-data/length-neq is used by len-last-rest, len-06,
list-data/less-02 is used by less-append,
list-data/lf-01 is used by onein, len-02,
list-data/sel-1 is used by len-02, first, c-08,
list-data/sel-2 is used by rest, c-07,
list-data/size-01 is used by unequal, split-first, len-04, len-01, len, append-size-less,
list-data/size-02 is used by len-05,

Used from specification nat-basic2

nat-basic2/a is used by unequal, split-rest, split-first, len-last-rest, len-06, len-05, len-04, len-03, len-01, len, e-04, append-size-less,
nat-basic2/add-base is used by len-04, len,
nat-basic2/c is used by unequal, split-rest, split-first, len-last-rest, len-06, len-05, len-04, len-03, len-01, len, e-04, append-size-less,
nat-basic2/eq is used by e-04,
nat-basic2/eq-01 is used by unequal, split-rest, split-first, len-last-rest, len-06, len-05, len-01, len,
nat-basic2/l is used by append-size-less,
nat-basic2/l-02 is used by split-rest, len-04, len-03,
nat-basic2/oz is used by split-first,
nat-basic2/succ is used by unequal, split-first, len-last-rest, len-05, len-04, len-03, len-01, len, append-size-less,
nat-basic2/z-01 is used by unequal, len-01, e-04,

Used from specification nat-basic1

nat-basic1/f is used by split-first, len-03, append-size-less,
nat-basic1/one-01 is used by split-first,
nat-basic1/ref-1 is used by len-03,
nat-basic1/zero is used by append-size-less,