[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 afs-base
Status:
Proved!
Axioms: 24, User Theorems: 85 (Proved: 85, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 579, Interactions: 148
afs-cons(0,0)
afs-cons-pagesize(7,2)
expath-one(3,1)
links-dec-nsubdirs(9,1)
links-modmeta-write3(2,1)
meta(0,0)
path-file(2,0)
path-split(4,1)
subdirs-del-entry(6,2)
valid-content(0,0)
afs-cons-dir-nlink(5,1)
afs-cons-root-dir(3,1)
expath-prefix(3,1)
links-del-entry(20,2)
links-nonempty(5,2)
meta-dir(3,1)
path-here(0,0)
path-split-one(7,3)
subdirs-del-mod-size(18,1)
valid-dentry-03(0,0)
afs-cons-file-nlink(5,1)
afs-cons-root-notfile(5,1)
expath-rec(7,2)
links-deldir(3,1)
links-put-same-entries(3,0)
meta-exsplit(3,1)
path-in-dirs(3,1)
path-trans(4,1)
subdirs-delete-orphans(7,2)
valid-dentry-with-parent(0,0)
afs-cons-in-next(7,2)
afs-cons-size-at-upto(2,0)
expath-split(11,5)
links-delother(2,0)
links-putnew(11,1)
meta-file(3,1)
path-in-end(6,1)
path-uni(6,1)
subdirs-inc-size(7,1)
valid-dir-ino(0,0)
afs-cons-init(7,4)
at-upto(0,0)
expath-split-given(9,5)
links-delother-subdirs(2,0)
links-putother(2,0)
meta-path(5,2)
path-in-start(3,1)
path-uni-com(5,2)
subdirs-modmeta(8,1)
valid-file-ino(0,0)
afs-cons-links-empty(10,4)
del-entries-neq(2,1)
getinode(0,0)
links-delsame(2,0)
links-putsame(2,0)
meta-split(3,1)
path-inj(6,1)
root-not-orphan(3,1)
subdirs-put(36,1)
valid-ino(0,0)
afs-cons-links-rmorphans(13,4)
dir-empty(0,0)
in-upto(0,0)
links-delsame-mod-subdirs(2,1)
lookup-dir(1,1)
new-exists(9,3)
path-links-empty(11,4)
subdirs(0,0)
subdirs-putother(3,1)
valid-inode(0,0)
afs-cons-nlink0-empty(5,2)
empty-upto(1,1)
isexpath(4,1)
links-dirs-union(14,3)
lookup-file(3,1)
orphans(0,0)
path-lookup(6,1)
subdirs-add-entry(12,3)
subdirs-write(1,1)
valid-negdentry(0,0)
afs-cons-nlink0-notin(7,1)
expath(0,0)
link-mod-dir-meta(10,1)
links-inc-nsubdirs(9,1)
lookup-here(0,0)
orphans-del-dir(11,4)
path-one(3,1)
subdirs-alloc(7,1)
upto-idem(3,2)
valid-pagesize(0,0)
afs-cons-non0(7,2)
expath-append(3,1)
links(0,0)
links-modmeta(10,1)
lookup-rec(0,0)
orphans-del-file(11,4)
path-prefix(3,1)
subdirs-dec-size(7,1)
upto-less(5,2)
valid-parent-ino(0,0)
afs-cons-notfile(5,1)
expath-eps(2,1)
links-add-entry(33,3)
links-modmeta-write2(2,1)
max-exists(47,24)
path-expath-prefix(3,1)
path-rec(0,0)
subdirs-del(2,0)
upto-same(7,1)