[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 alink

Used from specification nat-basic

nat-basic/a is used by path-split-wand, entries-dom, counttheshit, count-entries, abs-has-rootpath-h,
nat-basic/c is used by path-split-wand, entries-dom, counttheshit, count-entries, abs-has-rootpath-h,
nat-basic/eq-01 is used by path-split-wand, counttheshit, count-entries,
nat-basic/oz is used by counttheshit,
nat-basic/s-04 is used by entries-dom, counttheshit, count-entries, abs-has-rootpath-h,

Used from specification abstract-file

abstract-file/elim is used by abs-files-put-nlink, abs-files-put, abs-files-new, abs-files-del, abs-files-cong,
abstract-file/inj is used by abs-files-put-nlink, abs-files-put, abs-files-new,
abstract-file/sel-01 is used by abs-files-put, abs-files-new, abs-files-del, abs-files-cong,
abstract-file/sel-02 is used by abs-files-cong,
abstract-file/sel-06 is used by abs-files-put, abs-files-new, abs-files-del, abs-files-cong,
abstract-file/sel-07 is used by abs-files-put, abs-files-new, abs-files-del, abs-files-cong,

Used from specification afs-base

afs-base/expath is used by abs-nlinks-h, abs-meta-h,
afs-base/orphans is used by abs-delorphans,
afs-base/path-split is used by abs-paths-eq, abs-nlinks-h, abs-delorphans,
afs-base/expath-eps is used by abs-path-h, abs-nlinks-h,
afs-base/expath-rec is used by abs-path-h,
afs-base/isexpath is used by abs-unshared-h, abs-paths-eq, abs-nlinks-h, abs-meta-h, abs-delorphans,
afs-base/links is used by abs-nlinks-h,
afs-base/links-nonempty is used by abs-nlinks-h, abs-delorphans,
afs-base/meta-dir is used by abs-meta-h,
afs-base/meta-file is used by abs-meta-h,
afs-base/meta-path is used by abs-meta-h,
afs-base/path-here is used by path-fid, absc-path, abs-has-rootpath-h, abs-dir-h, abs-delorphans,
afs-base/path-in-dirs is used by path-fid, absc-path, abs-paths-eq, abs-nlinks-h, abs-delorphans,
afs-base/path-inj is used by abs-paths-eq,
afs-base/path-one is used by abs-nlinks-h, abs-delorphans,
afs-base/path-rec is used by path-fid, absc-path, abs-paths-eq, abs-has-rootpath-h, abs-dir-h,
afs-base/path-uni is used by abs-has-rootpath-h,
afs-base/path-uni-com is used by abs-has-rootpath-h,
afs-base/valid-dir-ino is used by path-fid, absc-path, abs-paths-eq, abs-path-h, abs-has-rootpath-h, abs-dir-h,
afs-base/valid-ino is used by path-fid, absc-path, abs-has-rootpath-h, abs-dir-h, abs-delorphans,

Used from specification afs-stream

afs-stream/files-iso is used by abs-files-cong,
afs-stream/stream-empty is used by abs-files-new,

Used from specification heap-sep

heap-sep/dir-heap/Eq-P is used by path-unfold, entries-empty, absc-drop,
heap-sep/dir-heap/Imp is used by path-unfold-wand,
heap-sep/dir-heap/sep is used by path-split-wand, abs-has-rootpath-h,
heap-sep/dir-heap/sep-ass is used by path-split-wand,
heap-sep/dir-heap/sep-mp is used by path-split-wand,
heap-sep/dir-heap/sep-split-interactive is used by path-split-wand, abs-has-rootpath-h,
heap-sep/dir-heap/split-union is used by path-split-wand,
heap-sep/dir-heap/wand is used by path-unfold-wand, path-split-wand,
heap-sep/dir-heap/And-prop-inj is used by entries-recdel,
heap-sep/dir-heap/and is used by tree-fold-dnode, path-unfold, path-split-wand, path-fid, entries-empty, entries-dom, entries-any, absc-path, absc-drop, abs-unshared-h, abs-tree, abs-paths-eq, abs-path-h, abs-nlinks-h, abs-meta-h, abs-is-file, abs-has-rootpath-h, abs-dnode-emp, abs-dir-h,
heap-sep/dir-heap/and-ass is used by tree-fold-dnode, path-unfold, path-split-wand, path-fid, entries-unfold, entries-recdel, entries-fold-p, entries-fold-fnode, entries-fold, entries-empty, entries-dom, entries-any, absc-path, absc-drop, absc-dnode-rec, absc-dnode-one, abs-unshared-h, abs-tree, abs-paths-eq, abs-path-h, abs-nlinks-h, abs-meta-h, abs-is-file, abs-is-dnode, abs-has-rootpath-h, abs-dnode-emp, abs-dir-h,
heap-sep/dir-heap/and-com is used by tree-fold-dnode, path-unfold, path-split-wand, path-fid, entries-unfold, entries-recdel, entries-fold-p, entries-fold-fnode, entries-fold, entries-empty, entries-dom, entries-any, absc-path, absc-drop, absc-dnode-rec, absc-dnode-one, abs-unshared-h, abs-tree, abs-paths-eq, abs-path-h, abs-nlinks-h, abs-meta-h, abs-is-file, abs-is-dnode, abs-has-rootpath-h, abs-dnode-emp, abs-dir-h,
heap-sep/dir-heap/emp is used by abs-nlinks-h,
heap-sep/dir-heap/emp-sep is used by path-unfold, entries-fold-fnode, entries-empty, entries-dom, absc-path, absc-drop, abs-unshared-h, abs-tree, abs-paths-eq, abs-path-h, abs-nlinks-h, abs-is-file, abs-has-rootpath-h, abs-has-rootpath, abs-dnode-emp, abs-dir-h, abs-delorphans,
heap-sep/dir-heap/false-and is used by abs-unshared-h, abs-paths-eq,
heap-sep/dir-heap/false-rev is used by path-unfold, absc-path, abs-nlinks-h,
heap-sep/dir-heap/false-sep is used by abs-unshared-h, abs-paths-eq,
heap-sep/dir-heap/falseH is used by path-unfold, absc-path, abs-unshared-h, abs-paths-eq, abs-nlinks-h,
heap-sep/dir-heap/precise-split-l is used by abs-has-rootpath-h,
heap-sep/dir-heap/prop is used by tree-fold-dnode, path-unfold, path-split-wand, path-fid, entries-empty, entries-dom, entries-any, absc-path, absc-drop, abs-unshared-h, abs-tree, abs-paths-eq, abs-path-h, abs-nlinks-h, abs-meta-h, abs-is-file, abs-has-rootpath-h, abs-dnode-emp, abs-dir-h,
heap-sep/dir-heap/prop-shift is used by tree-fold-dnode, path-unfold, path-split-wand, path-fid, entries-fold-fnode, entries-empty, entries-dom, entries-any, absc-path, absc-drop, absc-dnode-rec, abs-unshared-h, abs-tree, abs-paths-eq, abs-path-h, abs-nlinks-h, abs-meta-h, abs-is-file, abs-has-rootpath-h, abs-dnode-emp, abs-dir-h,
heap-sep/dir-heap/sep-ass is used by tree-fold-dnode, path-unfold-wand, path-unfold, path-split-wand, path-fid, entries-unfold, entries-fold-p, entries-fold-fnode, entries-empty, entries-dom, entries-del, entries-any, absc-path, absc-drop, absc-dnode-rec, abs-unshared-h, abs-tree, abs-paths-eq, abs-path-h, abs-nlinks-h, abs-meta-h, abs-is-file, abs-has-rootpath-h, abs-has-rootpath, abs-dnode-emp, abs-dir-h, abs-delorphans,
heap-sep/dir-heap/sep-com is used by tree-fold-dnode, path-unfold-wand, path-unfold, path-split-wand, path-fid, entries-unfold, entries-recdel, entries-fold-p, entries-fold-fnode, entries-empty, entries-dom, entries-del, entries-any, absc-path, absc-drop, absc-dnode-rec, abs-unshared-h, abs-tree, abs-paths-eq, abs-path-h, abs-nlinks-h, abs-meta-h, abs-is-file, abs-has-rootpath-h, abs-has-rootpath, abs-dnode-emp, abs-dir-h, abs-delorphans,
heap-sep/dir-heap/split-union is used by path-unfold-wand,
heap-sep/dir-heap/this is used by abs-has-rootpath-h,
heap-sep/dir-heap/this-emp is used by abs-has-rootpath-h, abs-has-rootpath,
heap-sep/dir-heap/true-and is used by path-unfold, entries-unfold, entries-fold-p, entries-fold-fnode, entries-fold, entries-empty, entries-any, absc-drop, abs-tree, abs-paths-eq, abs-nlinks-h, abs-dir-h,
heap-sep/dir-heap/true-rev is used by path-unfold, path-split-wand, entries-unfold, entries-fold-p, entries-fold-fnode, entries-fold, entries-empty, entries-any, absc-drop, abs-tree, abs-paths-eq, abs-nlinks-h, abs-is-file, abs-dir-h,
heap-sep/dir-heap/trueH is used by path-split-wand, abs-is-file,
heap-sep/dir-heap/wand-same-emp-p is used by path-split-wand,

Used from specification bag-union

bag-union/fidbag/in-one is used by abs-tree, abs-path-h, abs-nlinks-h, abs-dir-h,

Used from specification directory-tree-base

directory-tree-base/Extension is used by count-entries,
directory-tree-base/In-insert is used by entries-dom, count-entries,
directory-tree-base/At-same is used by path-split-wand, path-fid, entries-recdel, absc-drop, abs-has-rootpath-h,
directory-tree-base/Del-at is used by abs-paths-eq,
directory-tree-base/Del-in is used by entries-unfold, abs-paths-eq,
directory-tree-base/In-empty is used by entries-dom, count-entries, abs-has-rootpath-h,
directory-tree-base/In-insert is used by path-fid, abs-has-rootpath-h,
directory-tree-base/Size-insert is used by entries-dom, count-entries, abs-has-rootpath-h,
directory-tree-base/fnode-inj is used by abs-is-file,

Used from specification directory-tree

directory-tree/dnode-elim-strong is used by abs-nlinks-h,
directory-tree/dnode-onein is used by abs-nlinks-h,
directory-tree/fnode-elim-strong is used by abs-unshared-h,
directory-tree/split-at is used by abs-paths-eq, abs-nlinks-h,
directory-tree/tree-ext is used by abs-tree,
directory-tree/tree-induction is used by abs-has-rootpath-h,
directory-tree/at-dnode is used by path-unfold, path-split-wand, path-fid, absc-drop, abs-tree, abs-paths-eq, abs-dir-h,
directory-tree/dnode-elim is used by abs-paths-eq, abs-meta-h, abs-is-dnode,
directory-tree/fid is used by abs-tree, abs-meta-h,
directory-tree/fnode-notin is used by absc-drop,
directory-tree/in-dnode is used by absc-drop,
directory-tree/isdnode is used by absc-drop, abs-tree, abs-paths-eq, abs-meta-h, abs-dir-h,
directory-tree/isfnode is used by absc-drop, abs-tree, abs-meta-h, abs-dir-h,
directory-tree/meta is used by abs-tree,
directory-tree/nil-at is used by path-unfold, path-split-wand, path-fid, absc-drop, abs-tree, abs-paths-eq, abs-nlinks-h, abs-dir-h,
directory-tree/nil-in is used by path-unfold, path-split-wand, path-fid, absc-path, absc-drop, abs-tree, abs-paths-eq, abs-path-h, abs-nlinks-h, abs-delorphans,
directory-tree/notdir-notin is used by abs-paths-eq,
directory-tree/one-at is used by path-unfold, path-split-wand, path-fid, absc-path, abs-tree, abs-paths-eq, abs-path-h, abs-nlinks-h,
directory-tree/one-ind is used by path-unfold, path-split-wand, path-fid, absc-path, abs-tree, abs-paths-eq, abs-path-h, abs-nlinks-h,
directory-tree/one-inf is used by path-unfold, path-split-wand, path-fid, absc-path, abs-tree, abs-path-h,
directory-tree/put-here is used by absc-drop,
directory-tree/put-rec is used by absc-drop,
directory-tree/split-in is used by path-unfold, path-split-wand, path-fid, absc-path, abs-tree, abs-paths-eq, abs-path-h, abs-nlinks-h, abs-delorphans,

Used from specification file

file/sel is used by abs-of-put,
file/sel-02 is used by abs-of-put,
file/sel-03 is used by abs-of-put,

Used from specification store

store/file-data-store/At-other is used by abs-files-put,
store/file-data-store/Extension is used by abs-files-put, abs-files-emp,
store/open-file-handles/Extension is used by abs-of-emp,
store/dir-entries/In-insert is used by entries-dom, count-entries,
store/file-data-store/In-insert is used by abs-files-put,
store/dir-entries/Subset is used by abs-has-rootpath-h,
store/dir-entries/exin is used by path-split-wand, entries-unfold,
store/directory-tree-inst/exin is used by path-split-wand, entries-recdel, count-entries,
store/directory-tree-inst/exnotempty is used by entries-any,
store/dir-entries/exnotempty is used by count-entries,
store/file-data-store/k-Extension is used by abs-files-put-nlink, abs-files-put, abs-files-new, abs-files-del, abs-files-cong,
store/open-file-handles/k-Extension is used by abs-of-put, abs-of-del,
store/dir-entries/notin-del-notin is used by entries-del,
store/open-file-handles/notmemlookup is used by abs-of-emp,
store/directory-tree-inst/At-in-out is used by abs-has-rootpath-h,
store/dir-entries/At-in-out is used by abs-has-rootpath-h,
store/file-data-store/At-other is used by abs-files-new,
store/open-files/At-other is used by abs-of-put,
store/open-file-handles/At-other is used by abs-of-put,
store/open-files/At-same is used by abs-of-put,
store/file-data-store/At-same is used by abs-files-put, abs-files-new,
store/open-file-handles/At-same is used by abs-of-put,
store/dir-entries/At-same is used by path-split-wand, path-fid, entries-unfold, entries-fold-p, entries-fold-fnode, entries-fold, entries-any, abs-has-rootpath-h,
store/file-data-store/Del-at is used by abs-files-del,
store/open-file-handles/Del-at is used by abs-of-del,
store/dir-entries/Del-at is used by abs-paths-eq,
store/open-files/Del-at is used by abs-of-del,
store/dir-entries/Del-in is used by entries-any, absc-path, abs-paths-eq,
store/file-data-store/Del-in is used by abs-files-del,
store/open-files/Del-in is used by abs-of-del,
store/open-file-handles/Del-in is used by abs-of-del,
store/dir-entries/Del-rec-same is used by path-split-wand, entries-unfold, entries-fold-p, entries-fold-fnode, entries-fold, entries-any,
store/directory-tree-inst/Del-rec-same is used by entries-recdel, absc-drop,
store/file-data-store/In-empty is used by abs-files-emp,
store/dir-entries/In-empty is used by entries-dom, count-entries,
store/open-files/In-empty is used by abs-of-emp,
store/open-file-handles/In-empty is used by abs-of-emp,
store/open-files/In-insert is used by abs-of-put,
store/dir-entries/In-insert is used by path-fid, entries-unfold, count-entries, abs-has-rootpath-h,
store/dir-entries/Size-empty is used by count-entries, abs-dnode-emp,
store/dir-entries/Size-insert is used by path-split-wand, path-fid, count-entries,
store/directory-tree-inst/del-put is used by entries-unfold,
store/dir-entries/del-put is used by entries-any,
store/directory-tree-inst/empty is used by count-entries,
store/file-data-store/in-neq is used by abs-files-new,
store/open-files/in-neq is used by abs-of-put,
store/open-file-handles/in-neq is used by abs-of-put,
store/directory-tree-inst/ins-same-01 is used by entries-unfold,
store/dir-entries/ins-same-01 is used by entries-any,
store/file-data-store/insin is used by abs-files-put, abs-files-new,
store/open-files/insin is used by abs-of-put,
store/directory-tree-inst/insin is used by abs-has-rootpath-h,
store/open-file-handles/insin is used by abs-of-put,
store/dir-entries/insin is used by path-split-wand, entries-unfold, entries-fold-p, entries-fold-fnode, entries-fold, entries-any, count-entries, abs-has-rootpath-h,
store/dir-entries/neq is used by entries-empty,
store/directory-tree-inst/neq is used by entries-dom, abs-has-rootpath-h,
store/dir-entries/notin-del-notin is used by path-split-wand, entries-unfold, entries-fold-fnode, entries-fold, entries-any,
store/directory-tree-inst/notin-del-notin is used by entries-recdel, absc-path,
store/file-data-store/notmemlookup is used by abs-files-emp,
store/dir-entries/sub-ref is used by abs-has-rootpath-h,
store/dir-entries/subset-empty is used by abs-has-rootpath-h,

Used from specification maplet

maplet/dir-heap/map-del is used by abs-has-rootpath-h,
maplet/dir-heap/maplet is used by abs-has-rootpath-h,
maplet/dir-heap/at-eq is used by path-fid, absc-path, abs-paths-eq, abs-path-h, abs-nlinks-h, abs-meta-h, abs-has-rootpath-h, abs-dir-h,
maplet/dir-heap/eq-objs is used by path-unfold, absc-drop, abs-tree,
maplet/dir-heap/ex1 is used by path-unfold-wand, path-split-wand, path-fold, abs-paths-eq, abs-nlinks-h,
maplet/dir-heap/ex1-shift is used by path-unfold, abs-unshared-h, abs-paths-eq, abs-meta-h,
maplet/dir-heap/ex2 is used by abs-dnode-emp,
maplet/dir-heap/ex3 is used by path-split-wand, abs-dnode-emp,
maplet/dir-heap/ex3-shift is used by tree-fold-dnode, path-unfold, path-fid, absc-path, absc-drop, abs-unshared-h, abs-tree, abs-paths-eq, abs-path-h, abs-nlinks-h, abs-meta-h, abs-is-file, abs-has-rootpath-h, abs-dir-h,
maplet/dir-heap/map-in is used by path-fid, absc-path, abs-unshared-h, abs-tree, abs-paths-eq, abs-path-h, abs-nlinks-h, abs-meta-h, abs-is-file, abs-has-rootpath-h, abs-dir-h,
maplet/dir-heap/map-same is used by abs-unshared-h, abs-paths-eq,

Used from specification directory-tree-inst

directory-tree-inst/read-notin is used by path-fid, count-entries, absc-path,

Used from specification buffer-inf-conv

buffer-inf-conv/tobuf-empty is used by abs-files-new,

Used from specification directory-tree-fids

directory-tree-fids/fids-in is used by abs-nlinks-h,
directory-tree-fids/fids-path is used by abs-nlinks-h,
directory-tree-fids/fids-dnode is used by abs-tree, abs-path-h, abs-dir-h,
directory-tree-fids/fids-fnode is used by abs-tree, abs-path-h, abs-nlinks-h, abs-dir-h,
directory-tree-fids/fids-path is used by abs-unshared-h, abs-meta-h,
directory-tree-fids/fids-str is used by abs-tree, abs-path-h, abs-dir-h,

Used from specification set-basic

set-basic/alink-set/Extension is used by counttheshit, abs-nlinks-h,
set-basic/pathset/Extension is used by counttheshit,
set-basic/alink-set/indef is used by counttheshit,
set-basic/pathset/indef is used by counttheshit,
set-basic/alink-set/In-empty is used by counttheshit, abs-nlinks-h,
set-basic/pathset/In-empty is used by counttheshit,
set-basic/alink-set/In-insert is used by counttheshit,
set-basic/pathset/In-insert is used by counttheshit,
set-basic/pathset/Size-empty is used by counttheshit,
set-basic/pathset/Size-insert is used by counttheshit,
set-basic/alink-set/ne is used by counttheshit,
set-basic/pathset/ne-01 is used by counttheshit,
set-basic/alink-set/ne-01 is used by counttheshit,
set-basic/open-file-handles/ne-01 is used by abs-delorphans,
set-basic/pathset/size-zero is used by counttheshit,
set-basic/alink-set/size-zero is used by counttheshit, abs-nlinks-h,
set-basic/open-file-handles/size-zero-01 is used by abs-delorphans,
set-basic/pathset/size-zero-01 is used by counttheshit,
set-basic/alink-set/size-zero-01 is used by counttheshit, abs-nlinks-h,

Used from specification list-last

list-last/path/bapp is used by absc-drop,
list-last/path/b-01 is used by absc-drop,
list-last/path/butlast-one is used by absc-drop,
list-last/path/prefix-empty is used by absc-drop,
list-last/path/prefix-rec-03 is used by absc-drop,

Used from specification posix-base

posix-base/meta-dir is used by abs-meta-h,
posix-base/meta-file is used by abs-meta-h,

Used from specification list-data

list-data/path/elim-list-c is used by absc-drop, abs-paths-eq,

Used from specification stream

stream/buffer-inf/to-zero is used by abs-files-new,

Used from specification file-id-data

file-id-data/elim is used by abs-unshared-h, abs-tree, abs-path-h, abs-is-file, abs-dir-h,
file-id-data/inj is used by abs-tree, abs-path-h, abs-nlinks-h, abs-files-put, abs-files-new, abs-files-del, abs-dir-h,
file-id-data/sel is used by entries-fold-fnode, abs-nlinks-h, abs-is-file,

Used from specification abstract-dir

abstract-dir/elim is used by path-unfold, path-split-wand, path-fid, absc-path, absc-drop, abs-unshared-h, abs-tree, abs-paths-eq, abs-path-h, abs-nlinks-h, abs-meta-h, abs-has-rootpath-h, abs-dnode-emp, abs-dir-h, abs-delorphans,
abstract-dir/inj is used by abs-nlinks-h, abs-meta-h, abs-has-rootpath-h,
abstract-dir/sel-03 is used by tree-fold-dnode, path-unfold, path-split-wand, path-fid, absc-path, absc-drop, abs-tree, abs-paths-eq, abs-path-h, abs-nlinks-h, abs-dnode-emp, abs-dir-h,
abstract-dir/sel-04 is used by tree-fold-dnode, path-unfold, path-split-wand, absc-drop, abs-tree, abs-paths-eq, abs-nlinks-h, abs-dnode-emp, abs-dir-h,
abstract-dir/sel-09 is used by tree-fold-dnode, path-unfold, path-split-wand, path-fid, absc-path, absc-drop, abs-tree, abs-paths-eq, abs-path-h, abs-nlinks-h, abs-dnode-emp, abs-dir-h,

Used from specification list

list/path/lastdiv-rew is used by abs-nlinks-h, abs-delorphans,
list/path/longest-common-prefix is used by abs-paths-eq,
list/path/Last is used by abs-nlinks-h,
list/path/a is used by path-unfold, path-split-wand, path-fid, absc-path, absc-drop, absc-dnode-rec, abs-tree, abs-paths-eq, abs-path-h, abs-nlinks-h, abs-has-rootpath-h, abs-dir-h, abs-delorphans,
list/path/app is used by absc-drop, abs-paths-eq,
list/path/app-01 is used by abs-paths-eq,
list/path/app-02 is used by absc-dnode-rec, abs-paths-eq,
list/path/c is used by path-unfold, path-split-wand, path-fid, absc-path, absc-drop, abs-tree, abs-paths-eq, abs-path-h, abs-has-rootpath-h, abs-dir-h,
list/path/c-03 is used by absc-drop,
list/path/e is used by absc-dnode-rec, absc-dnode-one, abs-paths-eq,
list/path/e-01 is used by absc-drop, abs-paths-eq,
list/path/e-02 is used by abs-nlinks-h,

Used from specification afs-asm

afs-asm/Insert-size is used by counttheshit,

Used from specification heap

heap/file-heap/at-alloc is used by abs-files-new,
heap/dir-heap/disj-distr-uni is used by path-split-wand,
heap/dir-heap/ext is used by abs-delorphans,
heap/dir-heap/uni-ass is used by path-split-wand,
heap/file-heap/at-del is used by abs-files-del,
heap/dir-heap/at-diffs is used by abs-delorphans,
heap/dir-heap/at-uni is used by abs-has-rootpath-h,
heap/file-heap/at-write is used by abs-files-put-nlink, abs-files-put, abs-files-new,
heap/dir-heap/disj-com-rw is used by path-split-wand,
heap/dir-heap/disj-distr-uni-com is used by path-split-wand,
heap/dir-heap/disj-l is used by abs-has-rootpath-h,
heap/dir-heap/disj-r is used by abs-has-rootpath-h,
heap/dir-heap/disj-singleton-write is used by abs-has-rootpath-h,
heap/file-heap/in-alloc is used by abs-files-new,
heap/dir-heap/in-alloc is used by abs-has-rootpath-h,
heap/file-heap/in-del is used by abs-files-del,
heap/dir-heap/in-diffs is used by abs-delorphans,
heap/file-heap/in-emp is used by abs-files-emp,
heap/dir-heap/in-emp is used by abs-nlinks-h, abs-has-rootpath-h, abs-has-rootpath,
heap/dir-heap/in-uni is used by abs-has-rootpath-h,
heap/file-heap/in-write is used by abs-files-put-nlink, abs-files-put, abs-files-new,
heap/dir-heap/in-write is used by abs-has-rootpath-h,

Used from specification oelem

oelem/nat-set/irreflexivity is used by entries-dom, counttheshit, count-entries, abs-has-rootpath-h,

Used from specification file-data

file-data/elim is used by abs-meta-h, abs-files-put,
file-data/inj is used by abs-meta-h, abs-files-put, abs-files-cong,