| ar1[m] = elemindex(a, m1), kar[m1] = key-index(key, m), ar = ar1[bh.ar[n].idx, ar1[bh.ar[n].idx].idx:= n], ar0 = ar1, bh = bh1.ar:= bh1.ar[n, bh1.ar[bh1.size]], bh0 = bin-heap(kar, m0), bh1 = bh0.size:= (bh0.size - 1), n = m1, 2exp-size(# kar), n < # bh.ar, bh.ar[n].idx < # ar1, n < bh0.size, n < # bh1.ar, bh1.size < # bh1.ar, heap-order(kar, m0), no-dups-idx(kar, m0), valid-idx(kar, ar1, m0), key-index(key, m) ∈ keyset(kar, m0), m0 ≤ # kar, bh0.size ≥ 1 ⊦ # keyset(kar, m0) = 0, bh1.size = 0, bh1.size = n, keyset(kar, m0) = ∅, n = 0, n < # bh.ar ∧ (n - 1) / 2 < # bh.ar ∧ 2 ≠ 0 ∧ n ≥ 1 |
Used simplifier rules: mult-c: ⊦ m * n = n * m; from specification nat-mult%mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult% ⊦ m * n + n0 < n ↔ m = 0 ∧ n0 < n; (ws)% ⊦ m +1 = m + 1; (s)%fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat%trans: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic%lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic% ⊦ m + 1 ≤ n ↔ m < n; (s)%n0 ≤ n ⊦ m ≤ n - n0 ↔ m + n0 ≤ n; (s)%m0 ≠ 0 ⊦ n ≤ m / m0 ↔ n * m0 ≤ m; (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ m < 1 ↔ m = 0; (s)% ⊦ m ≤ n ↔ ¬ n < m; (ss)%fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic% ⊦ m < n → n ≠ 0; (s)% ⊦ # kar[n, ki] = # kar; (s)% ⊦ m < # kar → kar[m, ki][m] = ki; (s)% ⊦ bin-heap(kar, m).ar:= kar0 = bin-heap(kar0, m); (s)%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ m ≤ n → (n < m ↔ false); (s)% ⊦ m < n + 1 ↔ ¬ n < m; (s)%n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s)% ⊦ keyset(kar, 0) = ∅; (s)% ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s)% ⊦ m ≠ n → (m ≤ n ↔ m < n); (s)% ⊦ bin-heap(kar, m).ar = kar; (s)% ⊦ m ≤ n → (n - m = 0 ↔ n = m); (s)% ⊦ n ≥ m ↔ m ≤ n; (s)% ⊦ bin-heap(kar, m).size:= m0 = bin-heap(kar, m0); (s)% ⊦ bin-heap(kar, m).size = m; (s)