[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 root-ino

root-ino/neq-0 is used by afs-cons-init,

Used from specification alink

alink/elim is used by links-putnew, links-modmeta, links-inc-nsubdirs, links-dirs-union, links-del-entry, links-dec-nsubdirs, links-add-entry, link-mod-dir-meta, afs-cons-nlink0-notin, afs-cons-links-rmorphans,
alink/inj is used by links-del-entry, links-add-entry,
alink/sel-01 is used by links-nonempty, links-dirs-union,
alink/sel-02 is used by links-nonempty, links-dirs-union,

Used from specification store+set

store+set/dir-entries/In-data-in is used by subdirs-alloc,

Used from specification abstract-file

abstract-file/elim is used by upto-same, orphans-del-file, orphans-del-dir, afs-cons-links-empty,
abstract-file/inj is used by upto-same,
abstract-file/sel-01 is used by afs-cons-pagesize,
abstract-file/sel-02 is used by orphans-del-file, afs-cons-pagesize, afs-cons-file-nlink,

Used from specification nat-basic

nat-basic/a is used by max-exists,
nat-basic/c is used by max-exists,
nat-basic/f is used by upto-less, upto-idem, max-exists,
nat-basic/l-02 is used by max-exists,
nat-basic/l-05 is used by max-exists,
nat-basic/lf is used by max-exists,
nat-basic/ls-02 is used by max-exists,
nat-basic/oz is used by max-exists,
nat-basic/ref is used by new-exists, max-exists,
nat-basic/s-04 is used by max-exists,
nat-basic/succ is used by max-exists,
nat-basic/trans is used by max-exists,
nat-basic/zero-01 is used by max-exists,

Used from specification store

store/dir-entries/Extension is used by del-entries-neq,
store/file-content/k-Extension is used by upto-same, upto-less, upto-idem, empty-upto,
store/dir-entries/At-in-out is used by links-add-entry,
store/dir-entries/At-other is used by subdirs-add-entry, links-add-entry,
store/dir-entries/At-same is used by subdirs-add-entry, links-add-entry,
store/dir-entries/Del-at is used by subdirs-del-entry, links-del-entry, del-entries-neq,
store/dir-entries/Del-at-strong is used by subdirs-del-entry, links-del-entry,
store/dir-entries/Del-in is used by subdirs-del-entry, links-del-entry, del-entries-neq,
store/dir-entries/Del-other-data is used by links-del-entry,
store/dir-entries/In-empty is used by links-putnew, links-deldir, afs-cons-non0, afs-cons-links-rmorphans, afs-cons-init, afs-cons-in-next,
store/file-content/In-empty is used by empty-upto,
store/dir-entries/In-insert is used by links-add-entry,
store/dir-entries/Size-empty is used by afs-cons-non0, afs-cons-links-rmorphans, afs-cons-init, afs-cons-in-next,
store/dir-entries/in-neq is used by subdirs-add-entry, links-add-entry,
store/dir-entries/insin is used by subdirs-add-entry, links-add-entry,
store/dir-entries/notin-del-notin is used by subdirs-del-entry, links-del-entry,

Used from specification set-union

set-union/alink-set/unrax is used by links-dirs-union,
set-union/alink-set/Delete is used by links-delsame-mod-subdirs, links-del-entry, links-add-entry,
set-union/dir-heap-refset/Delete is used by orphans-del-file, orphans-del-dir,
set-union/dir-entries/Delete is used by subdirs-put, subdirs-del-mod-size, subdirs-del-entry, subdirs-add-entry,
set-union/dir-entries/Difference is used by subdirs-put,
set-union/dir-entries/One is used by subdirs-put,
set-union/dir-entries/del-e-02 is used by subdirs-put, subdirs-del-mod-size,
set-union/dir-entries/del-in-01 is used by subdirs-put, subdirs-del-mod-size,
set-union/dir-entries/delete-insert is used by subdirs-put,
set-union/dir-entries/diff-add-del is used by subdirs-put,
set-union/dir-entries/diff-e is used by subdirs-put,
set-union/dir-entries/una is used by subdirs-put,
set-union/dir-entries/unadd is used by subdirs-put,
set-union/dir-entries/unc is used by subdirs-put,
set-union/dir-entries/une is used by subdirs-put,
set-union/dir-entries/unin-01 is used by subdirs-put,

Used from specification nat

nat/fle is used by upto-less,
nat/fle-01 is used by upto-less,
nat/le-ls-simp is used by upto-same, upto-less,
nat/lels is used by upto-same, upto-less, max-exists,
nat/let is used by upto-less,

Used from specification set-basic

set-basic/dir-heap-refset/Extension is used by orphans-del-file, orphans-del-dir,
set-basic/alink-set/Extension is used by links-putnew, links-nonempty, links-modmeta, links-inc-nsubdirs, links-dirs-union, links-delsame-mod-subdirs, links-deldir, links-del-entry, links-dec-nsubdirs, links-add-entry, link-mod-dir-meta, afs-cons-nlink0-notin, afs-cons-links-rmorphans, afs-cons-init,
set-basic/dir-entries/Extension is used by subdirs-write, subdirs-putother, subdirs-put, subdirs-modmeta, subdirs-inc-size, subdirs-delete-orphans, subdirs-del-mod-size, subdirs-del-entry, subdirs-dec-size, subdirs-alloc, subdirs-add-entry, afs-cons-init,
set-basic/alink-set/In-empty is used by links-nonempty, afs-cons-nlink0-notin, afs-cons-init,
set-basic/dir-entries/In-empty is used by subdirs-put, afs-cons-init,
set-basic/dir-entries/In-insert is used by subdirs-put, subdirs-add-entry,
set-basic/alink-set/In-insert is used by links-add-entry,
set-basic/alink-set/Size-empty is used by path-links-empty, afs-cons-links-rmorphans,
set-basic/dir-entries/in-02 is used by subdirs-put,
set-basic/dir-entries/in-04 is used by subdirs-put,
set-basic/dir-entries/ne is used by subdirs-put,
set-basic/dir-entries/ne-01 is used by subdirs-put, subdirs-del-mod-size,
set-basic/dir-heap-refset/ne-01 is used by subdirs-delete-orphans, root-not-orphan, afs-cons-links-rmorphans,
set-basic/alink-set/size-zero is used by path-links-empty, afs-cons-nlink0-notin, afs-cons-links-empty, afs-cons-init,
set-basic/dir-entries/size-zero is used by subdirs-put, subdirs-del-mod-size, afs-cons-init,
set-basic/alink-set/size-zero-01 is used by path-links-empty, afs-cons-nlink0-notin, afs-cons-nlink0-empty, afs-cons-links-rmorphans, afs-cons-links-empty, afs-cons-init,
set-basic/dir-entries/size-zero-01 is used by subdirs-put, subdirs-del-mod-size, afs-cons-init,
set-basic/dir-heap-refset/size-zero-01 is used by subdirs-delete-orphans, root-not-orphan, afs-cons-links-rmorphans,
set-basic/alink-set/size-zero-02 is used by path-links-empty, orphans-del-file, orphans-del-dir, afs-cons-nlink0-empty, afs-cons-links-rmorphans,

Used from specification abstract-dir

abstract-dir/elim is used by subdirs-modmeta, subdirs-inc-size, subdirs-delete-orphans, subdirs-dec-size, subdirs-alloc, path-uni, path-split, path-one, path-lookup, path-links-empty, path-inj, path-in-end, orphans-del-file, orphans-del-dir, links-putnew, links-put-same-entries, links-modmeta, links-inc-nsubdirs, links-dirs-union, links-del-entry, links-dec-nsubdirs, links-add-entry, link-mod-dir-meta, expath-rec, expath-one, afs-cons-nlink0-notin, afs-cons-links-rmorphans, afs-cons-links-empty,
abstract-dir/inj is used by subdirs-modmeta, subdirs-inc-size, subdirs-dec-size, subdirs-alloc, links-putnew, links-modmeta, links-inc-nsubdirs, links-dirs-union, links-del-entry, links-dec-nsubdirs, links-add-entry, link-mod-dir-meta,
abstract-dir/sel-03 is used by afs-cons-non0, afs-cons-nlink0-empty, afs-cons-links-rmorphans, afs-cons-init, afs-cons-in-next, afs-cons-dir-nlink,
abstract-dir/sel-05 is used by orphans-del-dir, afs-cons-non0, afs-cons-nlink0-empty, afs-cons-links-rmorphans, afs-cons-init, afs-cons-in-next, afs-cons-dir-nlink,
abstract-dir/sel-08 is used by afs-cons-non0, afs-cons-nlink0-empty, afs-cons-links-rmorphans, afs-cons-init, afs-cons-in-next, afs-cons-dir-nlink,
abstract-dir/sel-09 is used by subdirs-put, subdirs-del-mod-size, subdirs-del-entry, subdirs-add-entry, path-split-one, path-one, links-nonempty, links-deldir, expath-rec, expath-one, afs-cons-non0, afs-cons-nlink0-empty, afs-cons-links-rmorphans, afs-cons-init, afs-cons-in-next, afs-cons-dir-nlink,
abstract-dir/upd-04 is used by link-mod-dir-meta,

Used from specification list

list/path/lastdiv-rew is used by path-links-empty,
list/path/Nil is used by path-split,
list/path/a is used by path-uni, path-split, path-prefix, path-one, path-lookup, path-inj, path-in-start, path-in-end, path-in-dirs, meta-split, meta-exsplit, expath-split-given, expath-split, expath-rec,
list/path/app is used by path-one, expath-split-given,
list/path/c is used by path-uni, path-split, path-lookup, path-inj, path-in-start, path-in-end, path-in-dirs,
list/path/e-01 is used by path-in-dirs,

Used from specification heap

heap/dir-heap/exin is used by max-exists,
heap/file-heap/exin is used by max-exists,
heap/file-heap/ext is used by max-exists,
heap/dir-heap/ext is used by max-exists,
heap/dir-heap/uni-com is used by path-uni-com,
heap/dir-heap/at-alloc is used by subdirs-alloc, links-putnew,
heap/dir-heap/at-del is used by links-deldir,
heap/dir-heap/at-diffs is used by subdirs-delete-orphans, afs-cons-links-rmorphans,
heap/dir-heap/at-uni is used by path-uni, links-dirs-union,
heap/dir-heap/at-write is used by subdirs-write, subdirs-putother, subdirs-modmeta, subdirs-inc-size, subdirs-del-mod-size, subdirs-del-entry, subdirs-dec-size, subdirs-add-entry, links-putnew, links-modmeta-write3, links-modmeta-write2, links-modmeta, links-inc-nsubdirs, links-del-entry, links-dec-nsubdirs, links-add-entry, link-mod-dir-meta, afs-cons-init,
heap/dir-heap/disj-com-rw is used by path-uni-com,
heap/dir-heap/disj-l is used by links-dirs-union,
heap/dir-heap/in-alloc is used by subdirs-alloc, max-exists, links-putnew, afs-cons-init,
heap/file-heap/in-alloc is used by max-exists,
heap/file-heap/in-del is used by orphans-del-file,
heap/dir-heap/in-del is used by orphans-del-dir, links-deldir,
heap/dir-heap/in-diffs is used by subdirs-delete-orphans, afs-cons-links-rmorphans,
heap/file-heap/in-emp is used by max-exists, afs-cons-init,
heap/dir-heap/in-emp is used by max-exists, afs-cons-init,
heap/dir-heap/in-uni is used by path-uni, links-dirs-union,
heap/dir-heap/in-write is used by subdirs-write, subdirs-putother, subdirs-modmeta, subdirs-inc-size, subdirs-del-mod-size, subdirs-del-entry, subdirs-dec-size, subdirs-add-entry, max-exists, links-putnew, links-modmeta-write3, links-modmeta-write2, links-modmeta, links-inc-nsubdirs, links-del-entry, links-dec-nsubdirs, links-add-entry, link-mod-dir-meta, afs-cons-init,
heap/file-heap/in-write is used by max-exists,
heap/file-heap/nonnull is used by new-exists,
heap/dir-heap/nonnull is used by new-exists,
heap/dir-heap/sanity is used by max-exists, afs-cons-non0,
heap/file-heap/sanity is used by max-exists, afs-cons-non0,
heap/file-heap/size-alloc is used by max-exists,
heap/dir-heap/size-alloc is used by max-exists,
heap/dir-heap/size-emp is used by max-exists,
heap/file-heap/size-write is used by max-exists,
heap/dir-heap/size-write is used by max-exists,
heap/dir-heap/write-again is used by subdirs-put,

Used from specification nat-mult

nat-mult/mult-a is used by upto-same, upto-less, upto-idem, afs-cons-size-at-upto,
nat-mult/mult-c is used by upto-same, upto-less, upto-idem, afs-cons-size-at-upto,

Used from specification list-last

list-last/path/prefix is used by path-prefix,