[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-induction, split-restn, one-restn, in-put, at-put, at-mod, at-del,
nat-basic/c is used by tree-induction, split-restn, one-restn, in-put, at-put, at-mod, at-del,
nat-basic/f is used by tree-induction,
nat-basic/l-02 is used by tree-induction,
nat-basic/s-04 is used by tree-induction,
nat-basic/succ is used by split-restn, in-put, at-put, at-mod, at-del,

Used from specification directory-tree-base

directory-tree-base/At-other is used by in-mod, at-put, at-mod,
directory-tree-base/At-other is used by in-put, in-del, at-put, at-mod, at-del,
directory-tree-base/At-same is used by tree-induction, same-put-one, same-put, in-put, in-mod, in-del, at-put, at-mod, at-dnode-same, at-del,
directory-tree-base/Del-at is used by in-del, at-del,
directory-tree-base/Del-in is used by in-del, at-del,
directory-tree-base/In-empty is used by in-dnode-empty,
directory-tree-base/In-insert is used by same-put-one, in-put, in-mod, in-del, at-put, at-mod, at-dnode-same, at-del,
directory-tree-base/disj is used by tree-ext, put-fnode, dnode-del, dir-put3, dir-put2, dir-put,
directory-tree-base/dnode-inj is used by tree-ext, in-put, at-put, at-mod,
directory-tree-base/fnode-inj is used by tree-ext, setfid-elim, put-fnode, fnode-elim-strong, fnode-elim,

Used from specification store

store/directory-tree-inst/exin is used by tree-induction, in-put, in-mod, at-put, at-mod,
store/directory-tree-inst/k-Extension is used by tree-ext,
store/directory-tree-inst/At-in-out is used by in-put,
store/directory-tree-inst/Del-at-strong is used by at-del,
store/directory-tree-inst/in-neq is used by in-put, at-put, at-mod, at-del,
store/directory-tree-inst/ins is used by again-put,
store/directory-tree-inst/ins-same-01 is used by again-put,
store/directory-tree-inst/insin is used by same-put, same-in, in-put, in-mod, in-del, at-put, at-mod, at-del,
store/directory-tree-inst/insins is used by same-put, in-put,
store/directory-tree-inst/k-At-same is used by in-put, at-put,

Used from specification directory-tree-inst

directory-tree-inst/read-notin is used by tree-ext, in-mod,

Used from specification list-last

list-last/path/bc is used by dir-put3,
list-last/path/prefix-empty is used by split-restn, in-put, in-del, at-put, at-mod,
list-last/path/prefix-nil is used by at-put, at-mod, at-del,
list-last/path/prefix-one is used by in-put, in-del, at-put,
list-last/path/prefix-one-01 is used by in-put, at-put, at-mod, at-del,
list-last/path/prefix-rec-02 is used by in-put, in-del, at-put, at-mod, at-del,
list-last/path/prefix-rec-03 is used by split-restn, in-put, in-del, at-put, at-mod, at-del,
list-last/path/prefix-self is used by notin-del,

Used from specification list-data

list-data/path/elim-list-c is used by split-restn, one-restn, in-put, at-put,
list-data/path/size-01 is used by split-restn, in-put, at-put, at-mod, at-del,

Used from specification list

list/path/Nil is used by split-restn, split-put, split-in, split-del, split-at, in-put, at-put,
list/path/a is used by tree-ext, split-restn, split-put, split-in, split-del, split-at, same-put, same-in, same-at, put-fnode, one-restn, one-ind, one-at, next-at, in-put, in-mod, in-dnode-empty, in-del, fnode-notin, dnode-del, dir-put3, at-put, at-mod, at-del, again-put,
list/path/app is used by split-put, same-put, put-fnode, one-ind, one-at, in-put, in-mod, in-del, dnode-del, dir-put3, at-put, at-mod, at-del,
list/path/app-01 is used by split-restn,
list/path/app-02 is used by split-restn, split-put, split-del, in-put, at-put,
list/path/app-04 is used by at-put, at-mod,
list/path/c is used by tree-ext, split-restn, split-put, split-in, split-del, split-at, same-put, same-in, same-at, put-fnode, one-restn, in-put, in-mod, in-dnode-empty, in-del, fnode-notin, dnode-del, dir-put3, at-put, at-mod, at-del, again-put,
list/path/c-03 is used by in-put, at-put, at-mod, at-del,
list/path/c-07 is used by in-put, at-put,
list/path/e is used by split-restn, one-inf, in-put, at-put,
list/path/e-01 is used by split-restn, put-fnode, in-put, in-mod, in-dnode-empty, in-del, fnode-notin, dnode-del, dir-put3, at-put, at-mod, at-del, again-put,
list/path/e-02 is used by in-put, at-put,
list/path/len-05 is used by split-restn, in-put, at-put, at-mod, at-del,

Used from specification list-del

list-del/path/rest-empty is used by restn-len,
list-del/path/restN-zero is used by split-restn, in-put, at-put, at-mod, at-del,
list-del/path/restn-empty is used by restn-len,
list-del/path/weak-restN-rec is used by split-restn, one-restn, at-put, at-mod, at-del,