| kar[m2] = key-index(key0, m0), kar[m1] = key-index(key, m), ar1[m] = elemindex(a, m1), kar[m1, key-index(key0, m0)][(m1 - 1) / 2] = key-index(key1, m3), kar[2 * m1 + 2] = key-index(key2, m4), kar[2 * m1 + 1] = key-index(key3, m5), 2exp-size(# kar), key1 < kar[(m1 - 1) / 2].key, (m1 - 1) / 2 < # kar, key0 < kar[(m1 - 1) / 2].key, m1 < m2, m0 < # ar1, m2 < # kar, m1 < # kar, m1 + 1 < # kar, heap-order(kar, m2 + 1), no-dups-idx(kar, m2 + 1), valid-idx(kar, ar1, m2 + 1), 1 ≤ m1, elemindex(a, m1) = elemindex(a, m3) ∧ valid-idx(kar, ar1, m1) ∧ key-index(key, m) ∈ keyset(kar, m1) → kar[m3] = key-index(key, m), 2 * m1 + 1 < m2 → ¬ key3 < key0, 2 * m1 + 2 < m2 → ¬ key2 < key0, key-index(key, m) = key-index(key0, m0) ∨ key-index(key, m) ∈ keyset(kar, m2) ⊦ #(keyset(kar, m2) ++ key-index(key0, m0)) = 0, # kar = 1, m1 = 0, m2 = m1, m2 = 1, key0 < key1, heap-order(kar[m1, key-index(key0, m0)], m2) |
Used simplifier rules: ⊦ m / 2 ≠ m + 1; (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic%m ≠ n ⊦ kar[m, ki][n] = kar[n]; (s)% ⊦ m * (n + 1) = m * n + m; (s)%mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult%mult-c: ⊦ m * n = n * m; from specification nat-mult% ⊦ m + 1 ≠ 0; (s)% ⊦ m ≤ m + n; (s)%lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic%trans: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic%nll: ⊦ ¬ key < key0 ∧ key < key1 → key0 < key1; (forward) from specification oelem[binheap-key]% ⊦ m +1 = m + 1; (s)% ⊦ key-index(key, m).key = key; (s)% ⊦ ¬ key < key; (s)%n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: m1, m6