[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 store+set

store+set/file-data-store/Dom is used by inv-create,

Used from specification nat-basic

nat-basic/a is used by rename-fids, fids-exists, inv-read,
nat-basic/add-base is used by rename-fids, inv-read,
nat-basic/c is used by rename-fids, fids-exists, inv-read,
nat-basic/f is used by inv-read,
nat-basic/ref is used by fids-exists,
nat-basic/s-04 is used by fids-exists,

Used from specification directory-tree-base

directory-tree-base/At-same is used by fids-exists,
directory-tree-base/In-empty is used by fids-exists,
directory-tree-base/In-insert is used by fids-exists,
directory-tree-base/Size-insert is used by fids-exists,

Used from specification bag-union

bag-union/fidbag/differente-notin is used by rename-fids, inv-unlink,
bag-union/fidbag/in-diff-notfirst is used by rename-fids,
bag-union/fidbag/in-union is used by rename-fids, fids-exists, inv-create, inv-link,
bag-union/fidbag/diff-empty is used by rename-fids, inv-rmdir,
bag-union/fidbag/differente-notin is used by rename-fids,
bag-union/fidbag/in-diff-notfirst is used by rename-fids, inv-unlink,
bag-union/fidbag/in-emp is used by fids-exists, inv-format,
bag-union/fidbag/in-one is used by rename-fids, fids-exists, inv-create, inv-link, inv-unlink,
bag-union/fidbag/in-union is used by rename-fids,
bag-union/fidbag/union-ass is used by rename-fids, inv-mkdir,
bag-union/fidbag/union-com is used by rename-fids, inv-mkdir,
bag-union/fidbag/union-diff-cancel is used by rename-fids,
bag-union/fidbag/union-diff-distr is used by rename-fids,
bag-union/fidbag/union-empty is used by inv-mkdir,

Used from specification directory-tree

directory-tree/dir-put3 is used by rename-root,
directory-tree/split-at is used by rename-fids,
directory-tree/tree-induction is used by fids-exists,
directory-tree/at-del is used by rename-fids,
directory-tree/at-dnode is used by rename-fids,
directory-tree/dir-del is used by rename-root, rename-fids, inv-rmdir, inv-unlink,
directory-tree/dir-put2 is used by inv-writemeta,
directory-tree/dir-put3 is used by inv-mkdir, inv-create, inv-link,
directory-tree/dnode-elim is used by rename-fids, inv-rmdir, inv-writemeta,
directory-tree/fnode-elim is used by rename-root, rename-fids, inv-open, inv-link, inv-unlink, inv-truncate, inv-readmeta, inv-writemeta,
directory-tree/fnode-notin is used by rename-fids,
directory-tree/in-del is used by rename-root, rename-fids,
directory-tree/in-dnode-empty is used by rename-fids,
directory-tree/isdnode is used by rename-fids, inv-format,
directory-tree/isfnode is used by rename-root, rename-fids, inv-open, inv-link, inv-unlink, inv-truncate, inv-writemeta,
directory-tree/nil-at is used by rename-root, rename-fids,
directory-tree/nil-in is used by rename-root, rename-fids, inv-mkdir, inv-create, inv-link,
directory-tree/nil-put is used by inv-mkdir, inv-create, inv-link,
directory-tree/notdir-notin is used by rename-root, rename-fids,
directory-tree/one-at is used by rename-fids,
directory-tree/one-ind is used by rename-fids,
directory-tree/setmeta-elim is used by inv-writemeta,
directory-tree/split-in is used by rename-fids,

Used from specification set-union

set-union/fidset/unrax is used by fids-exists,
set-union/fidset/One is used by fids-exists,

Used from specification store

store/directory-tree-inst/exnotempty is used by fids-exists,
store/directory-tree-inst/At-in-out is used by fids-exists,
store/open-file-handles/Del-at is used by inv-close,
store/open-file-handles/Del-at-strong is used by inv-close,
store/open-file-handles/Del-in is used by inv-close,
store/file-data-store/Del-in is used by rename-fids, inv-close, inv-unlink,
store/file-data-store/In-empty is used by inv-format,
store/file-data-store/In-insert is used by inv-create, inv-write, inv-truncate, inv-writemeta,
store/file-data-store/in-neq is used by inv-create,
store/directory-tree-inst/insin is used by fids-exists,

Used from specification nat

nat/add-01 is used by rename-fids,
nat/fle is used by inv-read,
nat/fle-01 is used by inv-read,
nat/le-def is used by crash-neutral-read, crash-neutral-write, inv-read, inv-write,
nat/le-ls-simp is used by crash-neutral-read, crash-neutral-write, inv-read, inv-write,
nat/let is used by inv-read, inv-write,
nat/lez is used by inv-write,

Used from specification error-class

error-class/ecommit is used by inv-sync, inv-fsyncdir, inv-recover, inv-format,
error-class/efail is used by inv-fsync, crash-neutral-fsync, crash-neutral-fsyncdir, crash-neutral-recover,
error-class/esuccess is used by crash-neutral-sync, inv-recover, inv-format,

Used from specification error

Used from specification directory-tree-fids

directory-tree-fids/fids-path is used by rename-fids,
directory-tree-fids/fids-put1 is used by rename-fids,
directory-tree-fids/fids-put2 is used by rename-fids,
directory-tree-fids/fids-strpath is used by rename-fids,
directory-tree-fids/fidb-diff-one is used by rename-fids, inv-unlink,
directory-tree-fids/fids-del is used by rename-fids, inv-rmdir, inv-unlink,
directory-tree-fids/fids-dnode is used by rename-fids, fids-exists, inv-mkdir, inv-rmdir, inv-format,
directory-tree-fids/fids-emp is used by rename-fids, fids-exists, inv-mkdir, inv-rmdir, inv-format,
directory-tree-fids/fids-fnode is used by rename-fids, fids-exists, inv-create, inv-link, inv-unlink,
directory-tree-fids/fids-ins is used by fids-exists,
directory-tree-fids/fids-path is used by inv-open, inv-link, inv-unlink,
directory-tree-fids/fids-put2 is used by inv-mkdir, inv-create, inv-link,
directory-tree-fids/fids-put3 is used by inv-writemeta,
directory-tree-fids/fids-sub is used by rename-fids,

Used from specification set-basic

set-basic/fidset/In-empty is used by fids-exists, inv-recover, inv-format,
set-basic/fidset/In-insert is used by inv-open,
set-basic/fidset/in-04 is used by fids-exists,
set-basic/fidset/ne-01 is used by inv-close,
set-basic/fidset/size-zero-01 is used by inv-close,

Used from specification list-last

list-last/path/prefix is used by rename-fids,
list-last/path/b-01 is used by rename-root, rename-fids,
list-last/path/bapp is used by rename-fids,
list-last/path/last-elim is used by rename-fids,
list-last/path/lb is used by rename-fids,
list-last/path/postifx-app-03 is used by rename-fids,
list-last/path/prefix-app is used by rename-root, rename-fids,
list-last/path/prefix-empty is used by rename-fids,
list-last/path/prefix-eq is used by rename-fids,
list-last/path/prefix-nil is used by rename-root, rename-fids,
list-last/path/prefix-one-01 is used by rename-fids,

Used from specification posix-base

posix-base/fids-cons is used by fids-cons-reduce, fid-in-fs, inv-format,
posix-base/inf-fids is used by inv-create,
posix-base/ofh-fids is used by fid-in-fs, inv-close,
posix-base/posix-crash is used by inv-recover,
posix-base/fids-cons-in is used by rename-fids, inv-truncate, inv-readmeta, inv-writemeta,
posix-base/fids-emp is used by inv-recover, inv-format,
posix-base/ofh-fids-mod is used by inv-read, inv-write, inv-seek,
posix-base/ofh-fids-new is used by inv-open,

Used from specification file-handle

file-handle/elim is used by inv-close, inv-read, inv-write, inv-seek,
file-handle/inj is used by inv-close,
file-handle/sel-05 is used by fid-in-fs, inv-open, inv-close,
file-handle/setpos is used by crash-neutral-seek, inv-read, inv-write, inv-seek,

Used from specification list

list/path/a is used by rename-root, rename-fids,
list/path/app-04 is used by rename-fids,
list/path/e-02 is used by rename-root, rename-fids,
list/path/len is used by rename-fids,
list/path/len-02 is used by rename-fids,

Used from specification posix-pre

posix-pre/pre-fsync-elowlevel is used by inv-fsync, crash-neutral-fsync,
posix-pre/pre-close-efail is used by crash-neutral-close, inv-close,
posix-pre/pre-close-esuccess is used by inv-close,
posix-pre/pre-create-efail is used by crash-neutral-create, inv-create,
posix-pre/pre-create-esuccess is used by inv-create,
posix-pre/pre-link-efail is used by crash-neutral-link, inv-link,
posix-pre/pre-link-esuccess is used by inv-link,
posix-pre/pre-mkdir-efail is used by crash-neutral-mkdir, inv-mkdir,
posix-pre/pre-mkdir-esuccess is used by inv-mkdir,
posix-pre/pre-open-efail is used by crash-neutral-open, inv-open,
posix-pre/pre-open-esuccess is used by inv-open,
posix-pre/pre-read-efail is used by crash-neutral-read, inv-read,
posix-pre/pre-read-esuccess is used by inv-read,
posix-pre/pre-readdir-efail is used by crash-neutral-readdir, inv-readdir,
posix-pre/pre-readmeta-efail is used by crash-neutral-readmeta, inv-readmeta,
posix-pre/pre-readmeta-esuccess is used by inv-readmeta,
posix-pre/pre-renam-efail is used by crash-neutral-renam, inv-renam,
posix-pre/pre-renam-esuccess is used by rename-root, rename-fids,
posix-pre/pre-rmdir-efail is used by crash-neutral-rmdir, inv-rmdir,
posix-pre/pre-rmdir-esuccess is used by inv-rmdir,
posix-pre/pre-seek-efail is used by crash-neutral-seek, inv-seek,
posix-pre/pre-seek-esuccess is used by inv-seek,
posix-pre/pre-truncate-efail is used by crash-neutral-truncate, inv-truncate,
posix-pre/pre-truncate-esuccess is used by inv-truncate,
posix-pre/pre-unlink-efail is used by crash-neutral-unlink, inv-unlink,
posix-pre/pre-unlink-esuccess is used by inv-unlink,
posix-pre/pre-write-efail is used by crash-neutral-write, inv-write,
posix-pre/pre-write-esuccess is used by inv-write,
posix-pre/pre-writemeta-efail is used by crash-neutral-writemeta, inv-writemeta,
posix-pre/pre-writemeta-esuccess is used by inv-writemeta,

Used from specification path

path/parent-elim is used by rename-root, rename-fids,

Used from specification list-del

list-del/path/restN-len is used by rename-fids,

Used from specification file-data

file-data/setcontent is used by crash-neutral-truncate, inv-write, inv-truncate,
file-data/setmeta is used by crash-neutral-writemeta, inv-writemeta,

Used from specification seekflag

seekflag/disj-03 is used by inv-seek,

Used from specification open-file-handles-ext

open-file-handles-ext/ex-minimal-new-fd is used by inv-open,