[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-inv
Status:
Proved!
Axioms: 7, User Theorems: 47 (Proved: 47, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 606, Interactions: 132
2exp-size(0,0)
heap-order-add-parent-key(17,5)
heap-order-pull-down-parent(20,0)
key-set-write-nodups(28,12)
keyset-subarray-eq(20,10)
no-dups-idx-mvlast(14,3)
no-dups-shorter(3,0)
valid-idx-outofbounds(5,2)
2exp-size-0(2,0)
heap-order-add-smaller(14,1)
heap-order-pull-up-child(31,3)
key-set-write-other(7,3)
keyset-subarray-eq-add(3,1)
no-dups-idx-rec(32,8)
no-dups-update-key(14,0)
valid-idx-rec(13,3)
2exp-size-1(1,0)
heap-order-min(25,8)
heap-order-remove-last(7,1)
keyset-base(0,0)
keyset-xchg(15,5)
no-dups-idx-rem1(6,1)
valid-idx(0,0)
valid-idx-remlast(18,3)
2exp-size-mult2(3,1)
heap-order-overwrite-children-at(21,2)
key-index-in-keyset-array-extract(5,2)
keyset-overwrite-add(11,4)
no-dups(0,0)
no-dups-idx-remlast(14,3)
valid-idx-0(1,1)
valid-idx-update-key(11,1)
heap-order(0,0)
heap-order-overwrite-children-ok(21,5)
key-set-1(2,1)
keyset-rec(0,0)
no-dups-0(1,0)
no-dups-idx-xchg(48,0)
valid-idx-imp-1(7,2)
valid-idx-xhg(31,5)
heap-order-0(1,0)
heap-order-overwrite-parent-ok(23,0)
key-set-extract-index(12,4)
keyset-size-bound(8,4)
no-dups-idx(0,0)
no-dups-keyset-size(30,14)
valid-idx-last-valid(3,1)
heap-order-1(1,0)
heap-order-overwrite0(18,2)
key-set-write-last(2,1)
keyset-size-bound0(3,2)
no-dups-idx-0(1,0)
no-dups-keyset-size-simp(2,1)
valid-idx-move-last(31,7)