| # kar0 = # kar, kar0[2 * n0 + 1] = key-index(key6, m6), kar0[3 + 4 * n0] = key-index(key7, m7), kar0[4 + 4 * n0] = key-index(key8, m4), kar0[n0] = key-index(key3, m3), kar[2 * n1 + 1] = key-index(key, m0), kar[2 * n1 + 2] = key-index(key0, m1), kar[n1] = key-index(key1, m2), kar0[2 * n0 + 2] = key-index(key2, m), keyset(kar0, n2 + n0) = keyset(kar, n2 + n0), key7 < key3, key8 < key3, 3 * n0 + 3 < n2, key8 < key7, n0 < # kar, 2 * n0 + 1 < # kar, m3 < # ar, m6 < # ar, n0 + 1 < n2, n0 + 2 < n2, 2 * n0 + 2 < # kar, key7 < key6, key8 < key6, id-idx(ar1, ar), no-dups-idx(kar, n2 + n0), no-dups-idx(kar0, n2 + n0), valid-idx(kar, ar1, n2 + n0), valid-idx(kar0, ar, n2 + n0), n2 ≤ 3 * n0 + 4, n2 + n0 ≤ # kar, (2 * n1 + 1 < n2 + n0 → ¬ key < key1) ∧ (2 * n1 + 2 < n2 + n0 → ¬ key0 < key1) → heap-order(kar, n2 + n0), 2 * n1 + 1 < n2 + n0 ∧ key < key1 ∨ 2 * n1 + 2 < n2 + n0 ∧ key0 < key1 → heap-order(kar[n1, (2 * n1 + 2 < n2 + n0 ∧ key0 < key ⊃ key-index(key0, m1);key-index(key, m0))], n2 + n0), ¬ key6 < key3 ∧ ¬ key2 < key3 → heap-order(kar0, n2 + n0), ∀ m. m < n2 + n0 ∧ m ≠ 0 → ¬ kar0[n0, key-index(key6, m6)][m].key < kar0[n0, key-index(key6, m6)][(m - 1) / 2].key, key6 < key3 ∨ key2 < key3 ⊦ key2 < key6, heap-order(kar0[n0, key-index(key6, m6)][2 * n0 + 1, key-index(key7, m7)], n2 + n0) |
Used simplifier rules: div2-mult4-add-k: ⊦ ((* n0) + 4 * n) / 2 = n0 / 2 + 2 * n;%m2 ≠ 0 ⊦ (* m2) * m + n < m + n0 ↔ (m2 - 1) * m + n < n0; (s)%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%n < n0 ⊦ (* n) ≠ m0 + (* n0); (s)%m1 ≠ 0 ⊦ m = (* m1) * m + n0 ↔ 0 = (m1 - 1) * m + n0; (s)%m ≠ n ⊦ kar[m, ki][n] = kar[n]; (s)% ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s)% ⊦ m0 * 1 = m0; (s)% ⊦ m + 1 ≠ 0; (s)% ⊦ key-index(key, m).key = key; (s) Used terms: 3 + 4 * n0