This is a listing of all goals defined over the current specification. Axioms are marked yellow, proved theorems green and unproved theorems blue. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| is-empty | bin_min_heap_is_empty#(bh; isempty){isempty := bh.size = 0} | An Axiom |
| empty | bin_min_heap_empty#(; bh){bh := bin-heap(mkkeyarray(1), 0)} | An Axiom |
| get-min | bin_min_heap_get_min#(bh; n){if bh.size = 0 then abort; n := bh.ar[0].idx} | An Axiom |
| next-2pot | bin_min_heap_next_2pot(minsize; n){while n < minsize do n := n * 2} | An Axiom |
| resize | bin_min_heap_resize#(minsize; bh) {if minsize > bh.size then let n = # bh.ar in {bin_min_heap_next_2pot(minsize; n); let kar = mkkeyarray(n) in {kar := copy(bh.ar, 0, kar, 0, bh.size); bh.ar := kar}} } | An Axiom |
| extract-min | bin_min_heap_extract_min#(; bh, ar, n) {bin_min_heap_get_min#(bh; n); bh.size := bh.size - 1; if bh.size ≠ 0 then {bh.ar[0] := bh.ar[bh.size]; ar[bh.ar[0].idx].idx := 0; bin_min_heap_bubble_down#(0; bh, ar)} } | An Axiom |
| insert | bin_min_heap_insert#(ki; bh, ar) {if ¬ ki.idx < # ar then abort; bin_min_heap_resize#(bh.size + 1; bh); bh.ar[bh.size] := ki; ar[ki.idx].idx := bh.size; bh.size := bh.size + 1; bin_min_heap_bubble_up#(bh.size - 1; bh, ar) } | An Axiom |
| bubble-up | bin_min_heap_bubble_up#(n; bh, ar) {let m = n in while m ≠ 0 ∧ bh.ar[m].key < bh.ar[(m - 1) / 2].key do let ki = bh.ar[m], ki0 = bh.ar[(m - 1) / 2] in {bh.ar[m] := ki0; ar[ki0.idx].idx := m; m := (m - 1) / 2; bh.ar[m] := ki; ar[ki.idx].idx := m} } | An Axiom |
| bubble-down | bin_min_heap_bubble_down#(n; bh, ar) {let m = n in while 2 * m + 1 < bh.size ∧ (bh.ar[2 * m + 1].key < bh.ar[m].key ∨ 2 * m + 2 < bh.size ∧ bh.ar[2 * m + 2].key < bh.ar[m].key) do let ki = bh.ar[m], ki0 = bh.ar[2 * m + 1] in if 2 * m + 2 < bh.size ∧ bh.ar[2 * m + 2].key < ki0.key then let ki1 = bh.ar[2 * m + 2] in {bh.ar[m] := ki1; ar[ki1.idx].idx := m; bh.ar[2 * m + 2] := ki; ar[ki.idx].idx := 2 * m + 2; m := 2 * m + 2} else {bh.ar[m] := ki0; ar[ki0.idx].idx := m; bh.ar[2 * m + 1] := ki; ar[ki.idx].idx := 2 * m + 1; m := 2 * m + 1} } | An Axiom |
| remove | bin_min_heap_remove#(n; bh, ar) {if ¬ n < bh.size then abort; bh.size := bh.size - 1; if bh.size ≠ 0 ∧ bh.size ≠ n then {bh.ar[n] := bh.ar[bh.size]; ar[bh.ar[n].idx].idx := n; if n ≠ 0 ∧ bh.ar[n].key < bh.ar[(n - 1) / 2].key then bin_min_heap_bubble_up#(n; bh, ar) else bin_min_heap_bubble_down#(n; bh, ar)} } | An Axiom |
| update | bin_min_heap_update#(n, key; bh, ar) {if ¬ n < bh.size then abort; let key0 = bh.ar[n].key in {bh.ar[n].key := key; if key < key0 then bin_min_heap_bubble_up#(n; bh, ar) else bin_min_heap_bubble_down#(n; bh, ar)} } | An Axiom |