| # kar0 = # kar, kar[2 * n1 + 1] = key-index(key, m0), kar[2 * n1 + 2] = key-index(key0, m1), kar[n1] = key-index(key1, m2), keyset(kar0, m) = keyset(kar, m), kar0[2 * n + 1].idx < kar0[n].idx, 2 * n + 1 < # kar, 2 * n + 1 < m, n < # kar, kar0[2 * n + 1].idx < # ar, heap-order(kar0[n, kar0[2 * n + 1]], m), id-idx(ar1, ar), no-dups-idx(kar0, m), no-dups-idx(kar, m), valid-idx(kar0, ar, m), valid-idx(kar, ar1, m), # ar ≤ kar0[n].idx, m ≤ # kar, ¬ kar0[2 * n + 1].key < kar0[n].key ∧ (2 * n + 2 < m → ¬ kar0[2 * n + 2].key < kar0[n].key) → heap-order(kar0, m), 2 * n + 2 < m → 2 * n + 2 < # kar, (2 * n1 + 1 < m → ¬ key < key1) ∧ (2 * n1 + 2 < m → ¬ key0 < key1) → heap-order(kar, m), 2 * n1 + 1 < m ∧ key < key1 ∨ 2 * n1 + 2 < m ∧ key0 < key1 → heap-order(kar[n1, (2 * n1 + 2 < m ∧ key0 < key ⊃ key-index(key0, m1);key-index(key, m0))], m), kar0[2 * n + 1].key < kar0[n].key ∨ 2 * n + 2 < m ∧ kar0[2 * n + 2].key < kar0[n].key ⊦ 2 * n + 2 < m ∧ kar0[2 * n + 2].key < kar0[2 * n + 1].key |
Used simplifier rules: ⊦ 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%fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat% ⊦ m < n → n ≠ 0; (s)% ⊦ m * n + n0 < n ↔ m = 0 ∧ n0 < n; (ws)%mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult%mult-c: ⊦ m * n = n * m; from specification nat-mult%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic%m < m0 ⊦ kar[m] = key-index(key, n) ∧ valid-idx(kar, ar, m0) → ¬ # ar ≤ n; (s)% ⊦ key = ki.key ∧ m = ki.idx ↔ ki = key-index(key, m); (elim) Used terms: kar0[n], key2, m3