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