[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 prefixn-shorter, prefixn-add, refine-add, initialization,
nat-basic/c is used by prefixn-shorter, prefixn-add, refine-add, initialization,
nat-basic/f is used by refine-get, refine-add,
nat-basic/l-02 is used by refine-add,
nat-basic/less-1 is used by refine-add,
nat-basic/lf-02 is used by refine-add,
nat-basic/oz is used by prefixn-shorter, prefixn-add, refine-add,
nat-basic/ref is used by refine-add,
nat-basic/s-04 is used by refine-add,
nat-basic/succ is used by refine-add,
nat-basic/succ-03 is used by refine-add,
nat-basic/zero is used by initialization,

Used from specification nat

nat/anti is used by refine-add,
nat/elim-pred-c is used by prefixn-shorter, prefixn-add, refine-add,
nat/eq-01 is used by refine-add,
nat/fle-01 is used by refine-add,
nat/gr-def is used by initialization,
nat/le-def is used by refine-add,
nat/le-ls-simp is used by refine-add,
nat/le-sum is used by refine-add,
nat/lels-02 is used by refine-add,
nat/lep is used by refine-add,
nat/lep-02 is used by refine-add,
nat/lez-01 is used by initialization,

Used from specification list-data

list-data/l is used by refine-get, refine-add,
list-data/length-neq is used by refine-add,
list-data/size-01 is used by refine-add, initialization,

Used from specification list-prefixn

list-prefixn/prefixn-shift-right is used by refine-add,
list-prefixn/prefixn-split-dropn is used by refine-add,
list-prefixn/prefixn-0 is used by prefixn-shorter, refine-add,
list-prefixn/prefixn-empty is used by prefixn-shorter, initialization,
list-prefixn/prefixn-eq-empty is used by prefixn-shorter,
list-prefixn/prefixn-full is used by refine-add,
list-prefixn/prefixn-fulln is used by refine-add,
list-prefixn/prefixn-len-n is used by refine-add,
list-prefixn/prefixn-prepend-one is used by prefixn-shorter, prefixn-add, refine-add,

Used from specification list

list/len-01 is used by refine-add,
list/Nil is used by refine-add, initialization,
list/a is used by prefixn-shorter, prefixn-add, refine-get, refine-add, initialization,
list/app-02 is used by prefixn-shorter,
list/app-08 is used by prefixn-add, refine-add,
list/c is used by prefixn-shorter, refine-add,
list/c-06 is used by prefixn-shorter,
list/e is used by prefixn-shorter,
list/in-14 is used by prefixn-shorter,
list/in-rec is used by prefixn-shorter,
list/len is used by refine-get, refine-add, initialization,
list/len-05 is used by refine-add,