[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-internal-asm
Status:
Proved!
Axioms: 24, User Theorems: 43 (Proved: 43, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 575, Interactions: 69
add1(0,0)
crash-neutral-add1(17,2)
crash-neutral-entries(11,1)
crash-neutral-recover(12,1)
gc-drop(0,0)
inv-check-commit(7,1)
inv-newino(8,1)
inv-truncate(5,0)
store(0,0)
add2(0,0)
crash-neutral-add2(17,2)
crash-neutral-gc(20,2)
crash-neutral-remove(4,0)
gc-step(0,0)
inv-commit(15,1)
inv-orphans-contains(5,0)
lookup(0,0)
sync-01(0,0)
add3(0,0)
crash-neutral-add3(17,2)
crash-neutral-get(6,0)
crash-neutral-store(5,0)
get(0,0)
inv-contains(11,0)
inv-orphans-insert(5,0)
newino(0,0)
truncate(0,0)
add4(0,0)
crash-neutral-add4(17,2)
crash-neutral-lookup(12,1)
crash-neutral-sync(10,1)
inv-add1(19,0)
inv-entries(10,0)
inv-orphans-remove(5,0)
orphans-contains(0,0)
add5(0,0)
crash-neutral-add5(20,1)
crash-neutral-newino(10,2)
crash-neutral-truncate(5,0)
inv-add2(28,5)
inv-format(10,0)
inv-recover(13,0)
orphans-insert(0,0)
check-commit(0,0)
crash-neutral-check-commit(6,0)
crash-neutral-orphans-contains(5,0)
entries(0,0)
inv-add3(37,10)
inv-gc(28,6)
inv-remove(4,0)
orphans-remove(0,0)
commit(0,0)
crash-neutral-commit(13,1)
crash-neutral-orphans-insert(5,0)
format(0,0)
inv-add4(49,17)
inv-get(10,0)
inv-store(5,0)
recover(0,0)
contains(0,0)
crash-neutral-contains(11,1)
crash-neutral-orphans-remove(5,0)
gc(0,0)
inv-add5(51,9)
inv-lookup(15,0)
inv-sync(7,0)
remove(0,0)