[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 aubifs-abs
Status:
Proved!
Axioms: 11, User Theorems: 42 (Proved: 42, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 362, Interactions: 112
C-ext(4,2)
abs-dirs-del-data(2,0)
abs-dirs-drop(7,1)
abs-files-del-dir(3,1)
abs-files-trunc(9,0)
abs-keys-orphans-add(11,3)
at-content(0,0)
in-children(0,0)
D-ext(4,2)
abs-dirs-del-dentry(7,1)
abs-dirs-gc-copy(6,2)
abs-files-del-file(3,1)
abs-files-unused-adrs(12,4)
abs-keys-orphans-add2(13,5)
at-dirs(0,0)
in-content(0,0)
D-inj(1,0)
abs-dirs-del-dir(3,0)
abs-dirs-orphans(12,3)
abs-files-del-orphans(14,6)
abs-keys(0,0)
abs-keys-orphans2(9,3)
at-files(0,0)
in-dirs(0,0)
Diff-union-comm(8,5)
abs-dirs-del-file(3,0)
abs-dirs-trunc(9,0)
abs-files-drop(9,0)
abs-keys-add(1,1)
abs-orphans(16,4)
dir(0,0)
in-files(0,0)
F-ext(4,2)
abs-dirs-del-orphans(14,6)
abs-dirs-unused-adrs(12,4)
abs-files-evict(9,3)
abs-keys-del(1,1)
abs-orphans-diff-datakeys(9,3)
dups-eqsize-entries(31,13)
F-inj(1,0)
abs-dirs-deldatakeys-1(4,0)
abs-files-del-data(7,2)
abs-files-gc-copy(6,3)
abs-keys-empty(2,1)
afs-cons-remove-orphans(18,4)
dups-eqsize-ls(36,15)
P-ext(4,2)
abs-dirs-deldatakeys-2(10,1)
abs-files-del-dentry(2,1)
abs-files-orphans(15,4)
abs-keys-orphans(11,3)
at-children(0,0)
file(0,0)