[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 fids-sub, fids-strpath, fids-put1, fids-in,
nat-basic/c is used by fids-sub, fids-strpath, fids-put1, fids-in,
nat-basic/f is used by fids-sub, fids-put1,
nat-basic/l-02 is used by fids-sub, fids-put1,
nat-basic/ref is used by fids-strpath, fids-in,
nat-basic/s-04 is used by fids-strpath, fids-in,

Used from specification directory-tree-base

directory-tree-base/At-other is used by fids-strpath,
directory-tree-base/At-same is used by fids-sub, fids-strpath, fids-put3, fids-put2, fids-put1, fids-in, fids-del,
directory-tree-base/In-empty is used by fids-strpath,
directory-tree-base/In-insert is used by fids-strpath, fids-put3, fids-put1, fids-in, fids-del,
directory-tree-base/Size-insert is used by fids-strpath, fids-in,
directory-tree-base/disj is used by fids-in,
directory-tree-base/fnode-inj is used by fids-in,

Used from specification bag-union

bag-union/fidbag/count-subset is used by fids-sub, fids-put1,
bag-union/fidbag/difference is used by fidb-diff-one,
bag-union/fidbag/in is used by fidb-diff-one,
bag-union/fidbag/in-union is used by fids-strpath, fids-in,
bag-union/fidbag/union is used by fids-sub, fids-put1,
bag-union/fidbag/union-diff-distr is used by fids-put1,
bag-union/fidbag/count-one is used by fidb-diff-one,
bag-union/fidbag/in-emp is used by fids-strpath, fids-in,
bag-union/fidbag/in-one is used by fids-in,
bag-union/fidbag/in-union is used by fids-in,
bag-union/fidbag/subset-refl is used by fids-sub,
bag-union/fidbag/union-ass is used by fids-put3, fids-put2, fids-put1, fids-in, fids-del,
bag-union/fidbag/union-com is used by fids-put3, fids-put2, fids-put1, fids-in, fids-del,
bag-union/fidbag/union-diff-cancel is used by fids-put1, fids-del,
bag-union/fidbag/union-diff-distr is used by fids-put1, fids-del,
bag-union/fidbag/union-inj is used by fids-put3, fids-put2, fids-put1,

Used from specification store

store/directory-tree-inst/exin is used by fids-sub, fids-put3, fids-put2, fids-put1, fids-in, fids-del,
store/directory-tree-inst/exnotempty is used by fids-strpath, fids-in,
store/directory-tree-inst/At-in-out is used by fids-strpath, fids-in,
store/directory-tree-inst/Del-rec-same is used by fids-del,
store/directory-tree-inst/insin is used by fids-strpath, fids-put3, fids-put1, fids-in, fids-del,
store/directory-tree-inst/insins is used by fids-put3, fids-put2, fids-put1, fids-del,
store/directory-tree-inst/notin-del-notin is used by fids-del,

Used from specification directory-tree

directory-tree/del-recin is used by fids-del,
directory-tree/put-rec is used by fids-put3, fids-put1,
directory-tree/tree-induction is used by fids-in,
directory-tree/at-dnode is used by fids-sub, fids-put3, fids-put2, fids-put1, fids-in, fids-del,
directory-tree/at-dnode-same is used by fids-put1, fids-in,
directory-tree/del-here is used by fids-del,
directory-tree/fnode-notin is used by fids-put2, fids-in,
directory-tree/in-dnode is used by fids-put2, fids-in,
directory-tree/isdnode is used by fids-put2,
directory-tree/isfnode is used by fids-put2,
directory-tree/nil-at is used by fids-sub, fids-put3, fids-put2, fids-put1, fids-in, fids-del,
directory-tree/nil-in is used by fids-sub, fids-put3, fids-put2, fids-in,
directory-tree/nil-put is used by fids-put3, fids-put2,
directory-tree/one-at is used by fids-sub, fids-put3, fids-put2, fids-put1, fids-in, fids-del,
directory-tree/one-ind is used by fids-sub, fids-put3, fids-put2, fids-put1, fids-in, fids-del,
directory-tree/one-inf is used by fids-sub, fids-put3, fids-put2, fids-put1, fids-in, fids-del,
directory-tree/put-here is used by fids-put3, fids-put2, fids-put1,
directory-tree/put-rec is used by fids-put2,
directory-tree/split-in is used by fids-sub, fids-put3, fids-put2, fids-put1, fids-in, fids-del,

Used from specification nat

nat/fle is used by fids-sub, fids-put1,
nat/le-def is used by fids-sub, fids-put1,
nat/lez is used by fidb-diff-one,
nat/sub-base is used by fidb-diff-one,

Used from specification list-last

list-last/path/bapp is used by fids-put2, fids-put1,
list-last/path/b-02 is used by fids-put2,
list-last/path/bc is used by fids-put2,
list-last/path/butlast-one is used by fids-put2,

Used from specification list

list/path/a is used by fids-sub, fids-put3, fids-put2, fids-put1, fids-in, fids-del,
list/path/app is used by fids-put3, fids-put2, fids-put1, fids-del,
list/path/c is used by fids-sub, fids-put3, fids-put2, fids-put1, fids-in, fids-del,
list/path/e-01 is used by fids-put2, fids-put1, fids-del,