[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 dll-size-correct, dll-size-iter-correct, dll_to_bst_rec_correct,
nat-basic/add-base is used by dll_to_bst_rec_correct,
nat-basic/c is used by dll-size-correct, dll-size-iter-correct, dll_to_bst_rec_correct,
nat-basic/eq-01 is used by dll-size-correct, dll-size-iter-correct, dll_to_bst_rec_correct,
nat-basic/eq-02 is used by dll-size-iter-correct,
nat-basic/f is used by dll_to_bst_rec_correct,
nat-basic/l is used by dll_to_bst_rec_correct,
nat-basic/l-02 is used by dll_to_bst_rec_correct,
nat-basic/lf is used by dll_to_bst_rec_correct,
nat-basic/lf-01 is used by dll_to_bst_rec_correct,
nat-basic/lf-02 is used by dll_to_bst_rec_correct,
nat-basic/neq-04 is used by dll_to_bst_rec_correct,
nat-basic/one-01 is used by dll_to_bst_rec_correct,
nat-basic/oz is used by dll-size-iter-correct, dll_to_bst_rec_correct,
nat-basic/refl-nat is used by dll-size-correct, dll-size-iter-correct, dll_to_bst_rec_correct,
nat-basic/s-04 is used by dll-size-correct, dll-size-iter-correct, dll_to_bst_rec_correct,
nat-basic/succ is used by dll-size-correct, dll-size-iter-correct, dll_to_bst_rec_correct,
nat-basic/trans-nat is used by dll_to_bst_rec_correct,
nat-basic/z-01 is used by dll_to_bst_rec_correct,
nat-basic/zero is used by dll_to_bst_rec_correct,

Used from specification linked-tree

linked-tree/tr-rec is used by dll_to_bst_rec_correct,
linked-tree/tr-null is used by dll_to_bst_rec_correct,

Used from specification node

node/elim-mknode is used by dll_to_bst_rec_correct,
node/inj-mknode is used by dll_to_bst_rec_correct,
node/sel-mknode-dotright is used by dll-size-correct, dll-size-iter-correct,
node/upd-mknode-dotleft is used by dll_to_bst_rec_correct,
node/upd-mknode-dotright is used by dll_to_bst_rec_correct,

Used from specification heap-sep

heap-sep/sep-com is used by dll_to_bst_rec_correct,
heap-sep/and is used by dll_to_bst_iter_correct, dll-size-correct, dll-size-iter-correct, dll_to_bst_rec_correct, dll_to_bst_correct,
heap-sep/and-ass is used by dll_to_bst_iter_correct, dll-size-correct, dll-size-iter-correct, dll_to_bst_rec_correct, dll_to_bst_correct,
heap-sep/and-com is used by dll_to_bst_iter_correct, dll-size-correct, dll-size-iter-correct, dll_to_bst_rec_correct, dll_to_bst_correct,
heap-sep/emp-sep is used by dll_to_bst_iter_correct, dll-size-correct, dll-size-iter-correct, dll_to_bst_rec_correct, dll_to_bst_correct,
heap-sep/false-rev is used by dll-size-correct, dll-size-iter-correct,
heap-sep/false-sep is used by dll-size-correct, dll-size-iter-correct,
heap-sep/falseH is used by dll-size-correct, dll-size-iter-correct,
heap-sep/prop is used by dll_to_bst_iter_correct, dll-size-correct, dll-size-iter-correct, dll_to_bst_rec_correct, dll_to_bst_correct,
heap-sep/prop-shift is used by dll_to_bst_iter_correct, dll-size-correct, dll-size-iter-correct, dll_to_bst_rec_correct, dll_to_bst_correct,
heap-sep/sep-ass is used by dll_to_bst_iter_correct, dll-size-correct, dll-size-iter-correct, dll_to_bst_rec_correct, dll_to_bst_correct,
heap-sep/sep-com is used by dll_to_bst_iter_correct, dll-size-correct, dll-size-iter-correct, dll_to_bst_rec_correct, dll_to_bst_correct,

Used from specification nat

nat/add-num-03 is used by dll_to_bst_rec_correct,
nat/elim-pred-c is used by dll_to_bst_rec_correct,
nat/elim-sub is used by dll_to_bst_rec_correct,
nat/eq is used by dll_to_bst_rec_correct,
nat/eq-01 is used by dll_to_bst_rec_correct,
nat/eqle-one is used by dll_to_bst_rec_correct,
nat/fle is used by dll_to_bst_rec_correct,
nat/fle-01 is used by dll_to_bst_rec_correct,
nat/ge is used by dll_to_bst_rec_correct,
nat/gr-def is used by dll_to_bst_rec_correct,
nat/le-def is used by dll_to_bst_rec_correct,
nat/lels is used by dll_to_bst_rec_correct,
nat/lep is used by dll_to_bst_rec_correct,
nat/lep-02 is used by dll_to_bst_rec_correct,
nat/ler is used by dll_to_bst_iter_correct, dll_to_bst_correct,
nat/let is used by dll_to_bst_rec_correct,
nat/lez is used by dll_to_bst_rec_correct,
nat/ls-01 is used by dll_to_bst_rec_correct,
nat/ls-02 is used by dll_to_bst_rec_correct,
nat/not-zero is used by dll_to_bst_rec_correct,
nat/succ-01 is used by dll_to_bst_rec_correct,

Used from specification maplet

maplet/node-heap/map-putex is used by dll_to_bst_rec_correct,
maplet/node-heap/at-rw is used by dll-size-correct, dll-size-iter-correct, dll_to_bst_rec_correct,
maplet/node-heap/ex1-shift is used by dll-size-correct, dll-size-iter-correct, dll_to_bst_rec_correct,
maplet/node-heap/ex2-shift is used by dll_to_bst_rec_correct,
maplet/node-heap/map-null is used by dll-size-correct, dll-size-iter-correct,
maplet/node-heap/map-write is used by dll_to_bst_rec_correct,
maplet/node-heap/mapex-in is used by dll_to_bst_rec_correct,
maplet/node-heap/mapex-put-rw is used by dll_to_bst_rec_correct,

Used from specification list-data

list-data/l is used by dll-size-iter-correct, dll_to_bst_rec_correct,
list-data/size-nil is used by dll-size-correct, dll_to_bst_rec_correct,

Used from specification linked-tree-list

linked-tree-list/balanced-base is used by dll_to_bst_rec_correct,
linked-tree-list/balanced-rec is used by dll_to_bst_rec_correct,
linked-tree-list/toList-base is used by dll_to_bst_rec_correct,
linked-tree-list/toList-ordered-tree-ordered is used by dll_to_bst_iter_correct, dll_to_bst_correct,
linked-tree-list/toList-rec is used by dll_to_bst_rec_correct,
linked-tree-list/tree-toList-size-equal-less-2 is used by dll_to_bst_rec_correct,

Used from specification list

list/elim-first is used by dll_to_bst_rec_correct,
list/Nil is used by dll-size-iter-correct, dll_to_bst_rec_correct,
list/a is used by dll-size-correct, dll-size-iter-correct, dll_to_bst_rec_correct,
list/app is used by dll-size-iter-correct,
list/app-02 is used by dll_to_bst_rec_correct,
list/c is used by dll-size-correct, dll-size-iter-correct, dll_to_bst_rec_correct,
list/c-06 is used by dll_to_bst_rec_correct,
list/e is used by dll_to_bst_rec_correct,
list/e-03 is used by dll_to_bst_rec_correct,
list/in-14 is used by dll-size-correct, dll_to_bst_rec_correct,
list/in-append is used by dll_to_bst_rec_correct,
list/in-rec is used by dll-size-correct, dll_to_bst_rec_correct,
list/len is used by dll-size-iter-correct, dll_to_bst_rec_correct,
list/len-01 is used by dll_to_bst_rec_correct,
list/len-02 is used by dll-size-iter-correct,
list/len-05 is used by dll-size-correct, dll-size-iter-correct, dll_to_bst_rec_correct,

Used from specification dlinked-list

dlinked-list/dlls-rec is used by dll_to_bst_rec_correct,
dlinked-list/dll is used by dll_to_bst_iter_correct, dll_to_bst_correct,
dlinked-list/dlls-base is used by dll_to_bst_iter_correct, dll-size-correct, dll-size-iter-correct, dll_to_bst_rec_correct, dll_to_bst_correct,
dlinked-list/dlls-rec is used by dll-size-correct, dll-size-iter-correct,

Used from specification heap

heap/node-heap/sanity is used by dll_to_bst_iter_correct, dll_to_bst_rec_correct, dll_to_bst_correct,

Used from specification nat-mult

nat-mult/ls-08 is used by dll_to_bst_rec_correct,
nat-mult/mult-a is used by dll_to_bst_rec_correct,
nat-mult/mult-c is used by dll_to_bst_rec_correct,
nat-mult/numeral-19 is used by dll_to_bst_rec_correct,
nat-mult/numeral-20 is used by dll_to_bst_rec_correct,
nat-mult/numeral-23 is used by dll_to_bst_rec_correct,
nat-mult/numeral-29 is used by dll_to_bst_rec_correct,
nat-mult/numeral-32 is used by dll_to_bst_rec_correct,
nat-mult/numeral-33 is used by dll_to_bst_rec_correct,
nat-mult/one is used by dll_to_bst_rec_correct,
nat-mult/rsucc-02 is used by dll_to_bst_rec_correct,
nat-mult/two-zero-01 is used by dll_to_bst_rec_correct,

Used from specification separation

separation/node-heap/eq is used by dll_to_bst_rec_correct,
separation/node-heap/assign-known is used by dll_to_bst_rec_correct,

Used from specification list-del

list-del/restN-append is used by dll_to_bst_rec_correct,
list-del/restn-nonempty-2 is used by dll_to_bst_rec_correct,
list-del/elim-firstn-restn is used by dll_to_bst_rec_correct,
list-del/first-all is used by dll_to_bst_iter_correct, dll_to_bst_correct,
list-del/first-append is used by dll_to_bst_rec_correct,
list-del/firstN-empty is used by dll_to_bst_rec_correct,
list-del/firstN-len is used by dll_to_bst_rec_correct,
list-del/firstN-zero is used by dll_to_bst_rec_correct,
list-del/rest-empty is used by dll_to_bst_rec_correct,
list-del/rest-len is used by dll_to_bst_rec_correct,
list-del/restN-all is used by dll_to_bst_iter_correct, dll_to_bst_correct,
list-del/restN-len is used by dll_to_bst_rec_correct,
list-del/restN-zero is used by dll_to_bst_rec_correct,

Used from specification nat-div

nat-div/div-elim is used by dll_to_bst_rec_correct,