[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 ubi-io-inv
Status:
Proved!
Axioms: 4, User Theorems: 11 (Proved: 11, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 53, Interactions: 5
initial(0,0)
peb-inv(0,0)
peb-inv-size(2,0)
reduce-initial(17,1)
inv(0,0)
peb-inv-empty-echdr(1,0)
peb-inv-write-echdr(1,0)
ubi-io-initial-imp-inv(4,0)
inv-size(3,0)
peb-inv-empty-vidhdr(2,0)
peb-inv-write-vidhdr(2,0)
ubi-io-inv-extract(4,0)
peb-initial(0,0)
peb-inv-markbad(1,0)
reduce(16,4)