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: |
|---|---|---|
| keyset | ⊦ keyset(bh) = keyset(bh.ar, bh.size) | An Axiom |
| bin-heap-inv-def | ⊦ bin-heap-inv(bh, ar) ↔ bh.size ≤ # bh.ar ∧ no-dups-idx(bh.ar, bh.size) ∧ valid-idx(bh.ar, ar, bh.size) ∧ 2exp-size(# bh.ar) ∧ heap-order(bh.ar, bh.size) | An Axiom |
| bubble-up-inv | ⊦ bubble-up-inv(n, bh, ar, bh0, ar0) ↔ n < bh.size ∧ bh.size ≤ # bh.ar ∧ # bh.ar = # bh0.ar ∧ bh.size = bh0.size ∧ id-idx(ar0, ar) ∧ no-dups-idx(bh.ar, bh.size) ∧ valid-idx(bh.ar, ar, bh.size) ∧ (n = 0 ∨ ¬ bh.ar[n].key < bh.ar[(n - 1) / 2].key → heap-order(bh.ar, bh.size)) ∧ (n ≠ 0 ∧ bh.ar[n].key < bh.ar[(n - 1) / 2].key → heap-order(bh.ar[n, bh.ar[(n - 1) / 2]], bh.size)) ∧ keyset(bh.ar, bh.size) = keyset(bh0.ar, bh0.size) | An Axiom |
| bubble-down-inv | ⊦ bubble-down-inv(n, bh, ar, bh0, ar0) ↔ bh.size ≤ # bh.ar ∧ # bh.ar = # bh0.ar ∧ bh.size = bh0.size ∧ id-idx(ar0, ar) ∧ no-dups-idx(bh.ar, bh.size) ∧ valid-idx(bh.ar, ar, bh.size) ∧ ( (2 * n + 1 < bh.size → ¬ bh.ar[2 * n + 1].key < bh.ar[n].key) ∧ (2 * n + 2 < bh.size → ¬ bh.ar[2 * n + 2].key < bh.ar[n].key) → heap-order(bh.ar, bh.size)) ∧ ( 2 * n + 1 < bh.size ∧ bh.ar[2 * n + 1].key < bh.ar[n].key ∨ 2 * n + 2 < bh.size ∧ bh.ar[2 * n + 2].key < bh.ar[n].key → heap-order(bh.ar[n, (2 * n + 2 < bh.size ∧ bh.ar[2 * n + 2].key < bh.ar[2 * n + 1].key ⊃ bh.ar[2 * n + 2];bh.ar[2 * n + 1])], bh.size)) ∧ keyset(bh.ar, bh.size) = keyset(bh0.ar, bh0.size) | An Axiom |
| div2-mult2-add-k | ⊦ ((* n0) + 2 * n) / 2 = n0 / 2 + n | A User Theorem |
| div2-mult4-add-k | ⊦ ((* n0) + 4 * n) / 2 = n0 / 2 + 2 * n | A User Theorem |
| key-set-in | ⊦ bin-heap-inv(bh, ar) → (ki ∈ keyset(bh) ↔ (∃ m. m < bh.size ∧ ki = bh.ar[m])) | A User Theorem |
| keyset-eq-empty | ⊦ bin-heap-inv(bh, ar) → (keyset(bh) = ∅ ↔ bh.size = 0) | A User Theorem |
| prepost-bubble-down | bh0 = bh, ar0 = ar, bubble-down-inv(n, bh, ar, bh0, ar0) ⊦ ⟪bin_min_heap_bubble_down#(n; bh, ar)⟫ ( bh.size = bh0.size ∧ # bh.ar = # bh0.ar ∧ id-idx(ar0, ar) ∧ no-dups-idx(bh.ar, bh.size) ∧ valid-idx(bh.ar, ar, bh.size) ∧ heap-order(bh.ar, bh.size) ∧ keyset(bh0) = keyset(bh)) | A User Theorem |
| prepost-bubble-up | bh0 = bh, ar0 = ar, bubble-up-inv(n, bh, ar, bh0, ar0) ⊦ ⟪bin_min_heap_bubble_up#(n; bh, ar)⟫ ( bh.size = bh0.size ∧ # bh.ar = # bh0.ar ∧ id-idx(ar0, ar) ∧ no-dups-idx(bh.ar, bh.size) ∧ valid-idx(bh.ar, ar, bh.size) ∧ heap-order(bh.ar, bh.size) ∧ keyset(bh0) = keyset(bh)) | A User Theorem |
| prepost-empty | ⊦ ⟪bin_min_heap_empty#(; bh)⟫ (bin-heap-inv(bh, ar) ∧ keyset(bh) = ∅) | A User Theorem |
| prepost-extract-min | bin-heap-inv(bh, ar), keyset(bh) ≠ ∅, ar0 = ar, bh0 = bh ⊦ ⟪bin_min_heap_extract_min#(; bh, ar, n)⟫ ( bin-heap-inv(bh, ar) ∧ id-idx(ar0, ar) ∧ (∃ key. key-index(key, n) ∈ keyset(bh0) ∧ keyset(bh) = keyset(bh0) -- key-index(key, n) ∧ (∀ ki. ki ∈ keyset(bh0) → ¬ ki.key < key))) | A User Theorem |
| prepost-get-min | bin-heap-inv(bh, ar), keyset(bh) ≠ ∅ ⊦ ⟪bin_min_heap_get_min#(bh; n)⟫ ∃ key. key-index(key, n) ∈ keyset(bh) ∧ (∀ ki. ki ∈ keyset(bh) → ¬ ki.key < key) | A User Theorem |
| prepost-insert | bin-heap-inv(bh, ar), ar0 = ar, bh0 = bh, ki.idx < # ar, ∀ ki0. ki0 ∈ keyset(bh0) → ki0.idx ≠ ki.idx ⊦ ⟪bin_min_heap_insert#(ki; bh, ar)⟫ (bin-heap-inv(bh, ar) ∧ id-idx(ar0, ar) ∧ keyset(bh) = keyset(bh0) ++ ki) | A User Theorem |
| prepost-next2pot | 2exp-size(n) ⊦ ⟪bin_min_heap_next_2pot(minsize; n)⟫ (2exp-size(n) ∧ n ≥ minsize) | A User Theorem |
| prepost-remove | bin-heap-inv(bh, ar), ar0 = ar, bh0 = bh, key-index(key, m) ∈ keyset(bh0), ar[m].idx = n ⊦ ⟪bin_min_heap_remove#(n; bh, ar)⟫ (bin-heap-inv(bh, ar) ∧ id-idx(ar0, ar) ∧ keyset(bh) = keyset(bh0) -- key-index(key, m)) | A User Theorem |
| prepost-resize | bin-heap-inv(bh, ar), bh0 = bh ⊦ ⟪bin_min_heap_resize#(minsize; bh)⟫ (bin-heap-inv(bh, ar) ∧ bh.size = bh0.size ∧ # bh.ar ≥ minsize ∧ subarray(bh.ar, 0, bh.size) = subarray(bh0.ar, 0, bh0.size)) | A User Theorem |
| prepost-update | bin-heap-inv(bh, ar), ar0 = ar, bh0 = bh, key-index(key0, m) ∈ keyset(bh0), ar[m].idx = n ⊦ ⟪bin_min_heap_update#(n, key; bh, ar)⟫ (bin-heap-inv(bh, ar) ∧ id-idx(ar0, ar) ∧ keyset(bh) = (keyset(bh0) -- key-index(key0, m)) ++ key-index(key, m)) | A User Theorem |