[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/oplus-l-at-left is used by crash-exists-h,
store+set/file-data-store/oplus-l-in is used by crash-exists-h,
store+set/open-file-handles/Diff-ext is used by ofh-fids-new,
store+set/file-data-store/oplus-l-at-right is used by crash-exists-h,

Used from specification nat-basic

nat-basic/a is used by hesselink-cons, crash-exists-h,
nat-basic/c is used by hesselink-cons, crash-exists-h,
nat-basic/ref is used by hesselink-cons, crash-exists-h,
nat-basic/s-04 is used by hesselink-cons, crash-exists-h,

Used from specification directory-tree-base

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

Used from specification bag-union

bag-union/fidbag/in-union is used by crash-exists-h,
bag-union/fidbag/in-emp is used by crash-exists-h,
bag-union/fidbag/in-one is used by crash-exists-h,

Used from specification directory-tree

directory-tree/tree-induction is used by crash-exists-h,
directory-tree/notdir-notin is used by hesselink-cons,
directory-tree/split-in is used by hesselink-cons,

Used from specification store

store/file-data-store/In-insert is used by crash-exists-h,
store/open-file-handles/exin is used by ofh-fids-mod,
store/directory-tree-inst/exnotempty is used by crash-exists-h,
store/open-file-handles/At-in-out is used by ofh-fids-new,
store/directory-tree-inst/At-in-out is used by crash-exists-h,
store/open-file-handles/At-same is used by ofh-fids-new, ofh-fids-mod,
store/file-data-store/In-empty is used by crash-exists-h,
store/open-file-handles/In-empty is used by fids-emp,
store/open-file-handles/In-insert is used by ofh-fids-new,
store/file-data-store/in-neq is used by crash-exists-h,
store/file-data-store/insin is used by crash-exists-h,
store/open-file-handles/insin is used by ofh-fids-new,
store/directory-tree-inst/insin is used by crash-exists-h,
store/open-file-handles/insins is used by ofh-fids-mod,
store/file-data-store/k-At-same is used by crash-exists-h,
store/open-file-handles/k-At-same is used by ofh-fids-new,

Used from specification directory-tree-fids

directory-tree-fids/fids-dnode is used by crash-exists-h,
directory-tree-fids/fids-emp is used by crash-exists-h,
directory-tree-fids/fids-fnode is used by crash-exists-h,
directory-tree-fids/fids-ins is used by crash-exists-h,
directory-tree-fids/fids-path is used by fids-cons-in,

Used from specification list-last

list-last/path/prefix-app-05 is used by hesselink-cons,
list-last/path/prefix-attach is used by hesselink-cons,
list-last/path/prefix-empty is used by hesselink-cons,

Used from specification set-basic

set-basic/fidset/Extension is used by ofh-fids-new, fids-emp,
set-basic/fidset/In-empty is used by fids-emp,
set-basic/fidset/In-insert is used by ofh-fids-new,

Used from specification file-handle

file-handle/elim is used by ofh-fids-new,
file-handle/inj is used by ofh-fids-new,
file-handle/sel-05 is used by ofh-fids-new, ofh-fids-mod,

Used from specification list

list/path/lastdiv-rew is used by hesselink-cons,
list/path/a is used by hesselink-cons,
list/path/app-04 is used by hesselink-cons,
list/path/e is used by hesselink-cons,
list/path/len is used by hesselink-cons,
list/path/len-02 is used by hesselink-cons,