[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 list

list/Last is used by path-equiv-reach,
list/Nil is used by path-two, path-equiv-reach,
list/a is used by path-two, path-equiv-reach,
list/app is used by path-equiv-reach,
list/c is used by path-equiv-reach,
list/c-08 is used by path-equiv-reach,
list/e-01 is used by path-equiv-reach,
list/e-02 is used by path-equiv-reach,
list/first is used by path-equiv-reach,
list/len is used by path-equiv-reach,
list/len-02 is used by path-equiv-reach,

Used from specification nat-basic1

nat-basic1/f is used by reachless-edge,
nat-basic1/one-01 is used by reachless-one,
nat-basic1/ref-1 is used by reachless-succ,
nat-basic1/zero-01 is used by reachless-zero,

Used from specification set-basic

set-basic/In-empty is used by reachset-emptyset,
set-basic/in-04 is used by reachset-one,
set-basic/ne-01 is used by reachset-mem-reach, reachset-del, reachless-succ-edge, reachless-edge, reach-trans, reach-rec-rev, path-equiv-reach,
set-basic/size-zero-01 is used by reachset-mem-reach, reachset-del, reachless-succ-edge, reachless-edge, reach-trans, reach-rec-rev, path-equiv-reach,

Used from specification list-data

list-data/elim-list-c is used by path-equiv-reach,
list-data/l is used by path-equiv-reach,
list-data/size-01 is used by path-equiv-reach,

Used from specification nat

nat/add-num-01 is used by path-equiv-reach,
nat/le-add is used by reachless-next,
nat/lels is used by reachless-next,
nat/let is used by reachless-next,

Used from specification list-last

list-last/butlast-last is used by path-equiv-reach,
list-last/l is used by path-equiv-reach,
list-last/l-02 is used by path-equiv-reach,
list-last/last-01 is used by path-equiv-reach,
list-last/last-def is used by path-equiv-reach,
list-last/last-elim is used by path-equiv-reach,

Used from specification nat-basic2

nat-basic2/a is used by reachless-succ-edge, reachless-succ, reachless-next, reachless-edge, reach-trans, reach-rec-rev, path-equiv-reach,
nat-basic2/c is used by reachless-succ-edge, reachless-succ, reachless-next, reachless-edge, reach-trans, reach-rec-rev, path-equiv-reach,
nat-basic2/eq-01 is used by path-equiv-reach,
nat-basic2/l is used by reachless-succ-edge,
nat-basic2/one-03 is used by path-equiv-reach,
nat-basic2/oz is used by path-equiv-reach,
nat-basic2/s is used by reachless-succ, reachless-next, reachless-edge,
nat-basic2/succ is used by reach-trans, reach-rec-rev, path-equiv-reach,
nat-basic2/z is used by reach-trans,
nat-basic2/z-01 is used by path-equiv-reach,

Used from specification set-union

set-union/Delete is used by reachset-del,