[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-replay
Status:
Proved!
Axioms: 11, User Theorems: 38 (Proved: 38, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 444, Interactions: 169
key-cons-dentry(3,1)
replay-cons-add-page(24,12)
replay-dentry(0,0)
replay-log-gc-drop(5,1)
replay-one-update(39,18)
replay-safe-empty(0,0)
replay-safe-split(3,1)
orphans-cons(0,0)
replay-cons-strong(0,0)
replay-drop-data(11,5)
replay-log-non-adr(2,1)
replay-orphans-data(21,8)
replay-safe-gc-copy(26,14)
replay-safe-write(9,0)
orphans-cons-gc-one(14,2)
replay-cons-strong-append(13,6)
replay-ino(0,0)
replay-log-one(1,1)
replay-orphans-del(15,6)
replay-safe-gc-copy-old(5,2)
replay-split(1,1)
orphans-cons-reduce(9,4)
replay-cons-strong-empty-log(2,1)
replay-log-drop(5,1)
replay-log-rec(0,0)
replay-orphans-dentry(24,9)
replay-safe-gc-drop(5,2)
replay-trunc(0,0)
repalyone-monotonic(20,4)
replay-cons-strong-safe(3,1)
replay-log-empty(0,0)
replay-log-split(3,1)
replay-orphans-inode(24,9)
replay-safe-one(2,1)
replaylog-keep-adr(5,1)
replay(0,0)
replay-cons-strong-variant1(9,4)
replay-log-gc-copy(17,8)
replay-log-write(5,0)
replay-orphans-trunc(22,9)
replay-safe-rec(0,0)
replayone-keep-adr(15,3)
replay-cons-add-orphan(32,16)
replay-data(0,0)
replay-log-gc-copy-old(5,1)
replay-nonorphans-trunc(23,10)
replay-safe-drop(9,0)
replay-safe-rec-variant1(2,0)
ri-closed-gc(11,5)