[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 tree-toList-size-equal-less-2, size-toList, toList-ordered-tree-ordered,
nat-basic/add-base is used by tree-toList-size-equal-less-2,
nat-basic/c is used by tree-toList-size-equal-less-2, size-toList, toList-ordered-tree-ordered,
nat-basic/eq-01 is used by tree-toList-size-equal-less-2, size-toList,
nat-basic/f is used by tree-toList-size-equal-less-2, toList-ordered-tree-ordered,
nat-basic/l is used by toList-ordered-tree-ordered,
nat-basic/l-02 is used by toList-ordered-tree-ordered,
nat-basic/one-01 is used by tree-toList-size-equal-less-2,
nat-basic/s-04 is used by toList-ordered-tree-ordered,
nat-basic/succ is used by tree-toList-size-equal-less-2, size-toList, toList-ordered-tree-ordered,

Used from specification nat

nat/l-num-05 is used by tree-toList-size-equal-less-2,
nat/lels-03 is used by toList-ordered-tree-ordered,
nat/lep is used by toList-ordered-tree-ordered,
nat/neq-add1 is used by tree-toList-size-equal-less-2,

Used from specification list-last

list-last/l-02 is used by tree-le-elem-toList-last,
list-last/lapp-01 is used by tree-le-elem-toList-last,
list-last/last-one is used by ordered-toList-ordered, tree-le-elem-toList-last,

Used from specification list-data

list-data/elim-add is used by ordered-toList-ordered,
list-data/l is used by toList-ordered-tree-ordered,
list-data/size-nil is used by size-toList,

Used from specification tree

tree/disj-leaf-branch is used by tree-le-elem-toList-last,
tree/size-branch is used by size-toList,
tree/size-leaf is used by size-toList,

Used from specification list

list/a is used by in-tree-in-toList, size-toList, ordered-toList-ordered, tree-le-elem-toList-last, toList-ordered-tree-ordered,
list/app is used by tree-le-elem-toList-last,
list/c is used by in-tree-in-toList, size-toList, ordered-toList-ordered, tree-le-elem-toList-last, toList-ordered-tree-ordered,
list/c-08 is used by ordered-toList-ordered,
list/e is used by ordered-toList-ordered,
list/e-01 is used by ordered-toList-ordered,
list/in-14 is used by ordered-toList-ordered,
list/in-append is used by in-tree-in-toList,
list/in-empty is used by in-tree-in-toList,
list/in-rec is used by in-tree-in-toList,
list/len is used by size-toList, toList-ordered-tree-ordered,
list/len-05 is used by size-toList, toList-ordered-tree-ordered,

Used from specification oelem

oelem/irreflexivity is used by tree-le-elem-toList-last,
oelem/nll is used by tree-le-elem-in-tree, tree-le-elem-toList-last,

Used from specification olist

olist/ordered-append is used by ordered-toList-ordered,
olist/orderedle-all is used by toList-ordered-tree-ordered,
olist/app is used by toList-ordered-tree-ordered,
olist/app-01 is used by toList-ordered-tree-ordered,
olist/le-e is used by ordered-toList-ordered, toList-ordered-tree-ordered,
olist/le-o is used by ordered-toList-ordered,
olist/orderedle-ls is used by ordered-toList-ordered,

Used from specification list-del

list-del/in-get is used by toList-ordered-tree-ordered,
list-del/get-app is used by toList-ordered-tree-ordered,
list-del/get-append-grt-02 is used by toList-ordered-tree-ordered,
list-del/get-append-less is used by toList-ordered-tree-ordered,
list-del/get-succ is used by toList-ordered-tree-ordered,