[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 bin-min-heap-prepost
Status:
Proved!
Axioms: 4, User Theorems: 14 (Proved: 14, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 659, Interactions: 154
bin-heap-inv-def(0,0)
div2-mult4-add-k(11,6)
prepost-bubble-down(154,34)
prepost-get-min(22,5)
prepost-resize(58,19)
bubble-down-inv(0,0)
key-set-in(5,1)
prepost-bubble-up(75,14)
prepost-insert(56,11)
prepost-update(84,18)
bubble-up-inv(0,0)
keyset(0,0)
prepost-empty(3,0)
prepost-next2pot(7,1)
div2-mult2-add-k(2,0)
keyset-eq-empty(5,1)
prepost-extract-min(81,21)
prepost-remove(96,23)