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

Lemma dependency for Specification aubifs-abs

A lemma (entry) may depend on lemmas (entries) below its position, but never on lemmas above its position. This means the list is a topological order of the dependency graph. An entry 'all subs proved' means that all used lemmas are (transitively) proved.

Name: Status: Subs proved? Used:
abs-keys-orphans-addprovedall subs proved abs-keys, abs-keys-add,
abs-files-unused-adrsprovedall subs proved at-content, in-content, P-ext, F-inj, file, at-files, in-files, F-ext,
abs-files-truncprovedall subs proved at-content, in-content, P-ext, F-inj, file, at-files, in-files, F-ext,
abs-files-orphansprovedall subs proved at-content, in-content, P-ext, F-inj, file, at-files, abs-keys, in-files,
abs-files-gc-copyprovedall subs proved at-content, in-content, P-ext, F-inj, file, at-files, in-files, F-ext,
abs-files-evictprovedall subs proved at-content, in-content, P-ext, F-inj, file, at-files, in-files,
abs-files-dropprovedall subs proved at-content, in-content, P-ext, F-inj, file, at-files, in-files, F-ext,
abs-files-del-orphansprovedall subs proved at-content, in-content, P-ext, F-inj, at-files, file, abs-keys, in-files, F-ext,
abs-files-del-fileprovedall subs proved at-content, in-content, P-ext, F-inj, file, at-files, in-files, F-ext,
abs-files-del-dirprovedall subs proved at-content, in-content, P-ext, F-inj, file, at-files, in-files, F-ext,
abs-files-del-dentryprovedall subs proved at-content, in-content, P-ext, F-inj, file, at-files, in-files, F-ext,
abs-files-del-dataprovedall subs proved at-content, in-content, P-ext, F-inj, file, at-files, in-files, F-ext,
abs-dirs-unused-adrsprovedall subs proved at-children, in-children, C-ext, D-inj, dir, at-dirs, in-dirs, D-ext,
abs-dirs-truncprovedall subs proved at-children, in-children, C-ext, D-inj, dir, at-dirs, in-dirs, D-ext,
abs-dirs-orphansprovedall subs proved at-children, in-children, C-ext, D-inj, at-dirs, dir, abs-keys, in-dirs, D-ext,
abs-dirs-gc-copyprovedall subs proved at-children, in-children, C-ext, D-inj, dir, at-dirs, in-dirs, D-ext,
abs-dirs-dropprovedall subs proved at-children, in-children, C-ext, D-inj, dir, at-dirs, in-dirs, D-ext,
abs-dirs-deldatakeys-2provedall subs proved at-children, in-children, C-ext, D-inj, dir, at-dirs, in-dirs, D-ext,
abs-dirs-deldatakeys-1provedall subs proved at-children, in-children, C-ext, D-inj, dir, at-dirs, in-dirs, D-ext,
abs-dirs-del-orphansprovedall subs proved at-children, in-children, C-ext, D-inj, at-dirs, dir, abs-keys, in-dirs, D-ext,
abs-dirs-del-fileprovedall subs proved at-children, in-children, C-ext, D-inj, dir, at-dirs, in-dirs, D-ext,
abs-dirs-del-dirprovedall subs proved at-children, in-children, C-ext, D-inj, dir, at-dirs, in-dirs, D-ext,
abs-dirs-del-dentryprovedall subs proved at-children, in-children, C-ext, D-inj, dir, at-dirs, in-dirs, D-ext,
abs-dirs-del-dataprovedall subs proved at-children, in-children, C-ext, D-inj, dir, at-dirs, in-dirs, D-ext,
abs-keys-addprovedall subs proved abs-keys,
F-extprovedall subs proved file, at-files, in-files,
P-extprovedall subs proved at-content, in-content,
D-extprovedall subs proved dir, at-dirs, in-dirs,
C-extprovedall subs proved at-children, in-children,
abs-orphans-diff-datakeysprovedall subs proved in-files, in-dirs,
abs-orphansprovedall subs proved at-content, in-content, at-children, in-children, file, at-files, dir, at-dirs, in-files, in-dirs, abs-keys,
abs-keys-orphans2provedall subs proved abs-keys,
abs-keys-orphans-add2provedall subs proved abs-keys,
abs-keys-orphansprovedall subs proved abs-keys,
abs-keys-emptyprovedall subs proved abs-keys,
abs-keys-delprovedall subs proved abs-keys,
F-injprovedall subs proved
abs-keysaxiom
D-injprovedall subs proved
in-contentaxiom
at-contentaxiom
in-filesaxiom
at-filesaxiom
fileaxiom
in-dirsaxiom
at-dirsaxiom
diraxiom
in-childrenaxiom
at-childrenaxiom