[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
,
Theorem base summary for Specification vfs-abs
Status:
Proved!
Axioms: 12, User Theorems: 45 (Proved: 45, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 656, Interactions: 245
abs-delorphans(17,7)
abs-files-emp(3,2)
abs-is-dnode(3,0)
abs-of-put(3,1)
absc-dnode-rec(2,1)
entries-any(5,1)
entries-fold-p(2,0)
tree-fold-dnode(3,0)
abs-dir-h(22,5)
abs-files-in(0,0)
abs-is-file(5,1)
abs-path-h(15,4)
absc-drop(27,8)
entries-del(3,1)
entries-recdel(3,1)
abs-dnode(0,0)
abs-files-new(15,5)
abs-meta-h(19,6)
abs-paths-eq(71,28)
absc-emp(0,0)
entries-dom(9,5)
entries-unfold(6,2)
abs-dnode-emp(10,2)
abs-files-put(22,9)
abs-nlinks-h(52,22)
abs-rec(0,0)
absc-entries(0,0)
entries-dom1(3,1)
path-fid(10,4)
abs-empty(0,0)
abs-files-put-nlink(11,4)
abs-of-at(0,0)
abs-tree(56,12)
absc-path(8,2)
entries-dom2(3,1)
path-fold(5,1)
abs-files-at(0,0)
abs-fnode(0,0)
abs-of-del(1,1)
abs-unshared-h(31,10)
clinks(0,0)
entries-empty(3,2)
path-split-wand(47,24)
abs-files-cong(9,4)
abs-has-rootpath(3,1)
abs-of-emp(3,2)
absc-dnode(0,0)
count-entries(17,10)
entries-fold(2,0)
path-unfold(28,12)
abs-files-del(6,3)
abs-has-rootpath-h(51,24)
abs-of-in(0,0)
absc-dnode-one(1,1)
counttheshit(30,11)
entries-fold-fnode(2,0)
path-unfold-wand(9,4)