[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 vfs-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:
path-fidprovedall subs proved entries-unfold, entries-dom1, entries-dom2, abs-dnode, abs-is-file,
abs-nlinks-hprovedall subs proved abs-is-file, abs-dir-h, abs-has-rootpath, entries-recdel, entries-dom1, entries-dom2, abs-dnode, absc-path, path-unfold, abs-fnode, abs-path-h,
abs-delorphansprovedall subs proved abs-path-h, abs-has-rootpath,
entries-unfoldprovedall subs proved entries-recdel, entries-dom1, entries-dom2, entries-del, abs-rec,
abs-has-rootpathprovedall subs proved abs-has-rootpath-h,
path-unfold-wandprovedall subs proved path-unfold,
path-split-wandprovedall subs proved entries-del, abs-rec, entries-dom1, entries-dom2, abs-dnode,
path-foldprovedall subs proved path-unfold,
entries-fold-pprovedall subs proved entries-del, abs-rec,
abs-unshared-hprovedall subs proved abs-fnode, abs-is-dnode, absc-path, path-unfold, abs-path-h,
abs-paths-eqprovedall subs proved absc-emp, entries-recdel, entries-dom2, entries-dom1, abs-is-dnode, absc-path, path-unfold, abs-dir-h, abs-path-h,
abs-meta-hprovedall subs proved abs-dnode, abs-files-at, abs-is-file, absc-path, path-unfold, abs-path-h, abs-dir-h,
entries-delprovedall subs proved entries-dom1,
abs-dir-hprovedall subs proved entries-recdel, entries-dom2, entries-dom1, abs-fnode, abs-dnode,
path-unfoldprovedall subs proved entries-recdel, entries-dom1, entries-dom2, absc-entries, absc-dnode-rec, abs-dnode, absc-emp,
absc-pathprovedall subs proved entries-dom2, absc-entries, absc-dnode-rec, absc-emp,
abs-has-rootpath-hprovedall subs proved entries-dom2, entries-dom1, abs-empty, entries-any, abs-dnode, abs-fnode,
abs-path-hprovedall subs proved abs-fnode, entries-dom1, entries-recdel, abs-dnode, abs-is-file,
abs-treeprovedall subs proved entries-dom1, entries-dom2, entries-recdel, abs-fnode, abs-dnode,
entries-dom1provedall subs proved entries-dom,
entries-dom2provedall subs proved entries-dom,
entries-domprovedall subs proved abs-empty, entries-any,
entries-emptyprovedall subs proved entries-any, abs-empty,
absc-dropprovedall subs proved absc-entries, absc-dnode-rec, absc-emp,
absc-dnode-recprovedall subs proved absc-dnode, absc-entries,
abs-is-dnodeprovedall subs proved abs-dnode,
abs-is-fileprovedall subs proved abs-dnode, abs-fnode,
entries-anyprovedall subs proved abs-rec,
entries-recdelprovedall subs proved abs-rec,
tree-fold-dnodeprovedall subs proved abs-dnode,
entries-fold-fnodeprovedall subs proved abs-fnode, abs-rec,
entries-foldprovedall subs proved abs-rec,
absc-dnode-oneprovedall subs proved absc-dnode,
abs-of-putprovedall subs proved abs-of-at, abs-of-in,
abs-of-empprovedall subs proved abs-of-in,
abs-of-delprovedall subs proved abs-of-at, abs-of-in,
abs-files-put-nlinkprovedall subs proved abs-files-at, abs-files-in,
abs-files-putprovedall subs proved abs-files-at, abs-files-in,
abs-files-newprovedall subs proved abs-files-at, abs-files-in,
abs-files-empprovedall subs proved abs-files-in,
abs-files-delprovedall subs proved abs-files-at, abs-files-in,
abs-files-congprovedall subs proved abs-files-at, abs-files-in,
abs-dnode-empprovedall subs proved abs-empty, abs-dnode,
abs-recaxiom
absc-entriesaxiom
absc-dnodeaxiom
absc-empaxiom
abs-of-inaxiom
abs-of-ataxiom
abs-files-inaxiom
abs-files-ataxiom
abs-emptyaxiom
abs-dnodeaxiom
abs-fnodeaxiom