Proof step 102 from proof prepost-bubble-down (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 103:

  # bh0.ar = # kar, kar[n1] = key-index(key1, m2), kar[2 * n1 + 2] = key-index(key0, m1), kar[2 * n1 + 1] = key-index(key, m0), keyset(bh0.ar, bh0.size) = keyset(kar, bh0.size), 2 * n0 + 1 < # kar, n0 < # kar, 2 * n0 + 1 < bh0.size, bh0.ar[2 * n0 + 1].idx < # ar, bh0.ar[n0].idx < # ar, heap-order(bh0.ar[n0, bh0.ar[2 * n0 + 1]], bh0.size), id-idx(ar1, ar), no-dups-idx(bh0.ar, bh0.size), no-dups-idx(kar, bh0.size), valid-idx(bh0.ar, ar, bh0.size), valid-idx(kar, ar1, bh0.size), bh0.size ≤ # kar, ¬ bh0.ar[2 * n0 + 1].key < bh0.ar[n0].key ∧ (2 * n0 + 2 < bh0.size → ¬ bh0.ar[2 * n0 + 2].key < bh0.ar[n0].key) → heap-order(bh0.ar, bh0.size), 2 * n1 + 1 < bh0.size ∧ key < key1 ∨ 2 * n1 + 2 < bh0.size ∧ key0 < key1 → heap-order(kar[n1, (2 * n1 + 2 < bh0.size ∧ key0 < key ⊃ key-index(key0, m1);key-index(key, m0))], bh0.size), (2 * n1 + 1 < bh0.size → ¬ key < key1) ∧ (2 * n1 + 2 < bh0.size → ¬ key0 < key1) → heap-order(kar, bh0.size), 2 * n0 + 2 < bh0.size → 2 * n0 + 2 < # kar, bh0.ar[2 * n0 + 1].key < bh0.ar[n0].key ∨ 2 * n0 + 2 < bh0.size ∧ bh0.ar[2 * n0 + 2].key < bh0.ar[n0].key ⊦ 2 * n0 + 2 < bh0.size ∧ bh0.ar[2 * n0 + 2].key < bh0.ar[2 * n0 + 1].key, ( 3 + 4 * n0 < bh0.size → 3 + 4 * n0 < # kar ∧ (¬ bh0.ar[3 + 4 * n0].key < bh0.ar[n0].key → 4 + 4 * n0 < bh0.size → 4 + 4 * n0 < # kar)) ∧ no-dups-idx(bh0.ar[n0, bh0.ar[2 * n0 + 1]][2 * n0 + 1, bh0.ar[n0]], bh0.size) ∧ valid-idx (bh0.ar[n0, bh0.ar[2 * n0 + 1]][2 * n0 + 1, bh0.ar[n0]], ar[bh0.ar[2 * n0 + 1].idx, ar[bh0.ar[2 * n0 + 1].idx].idx:= n0] [bh0.ar[n0].idx, ar[bh0.ar[2 * n0 + 1].idx, ar[bh0.ar[2 * n0 + 1].idx].idx:= n0][bh0.ar[n0].idx].idx:= (2 * n0 + 1) ], bh0.size) ∧ ( (3 + 4 * n0 < bh0.size → ¬ bh0.ar[3 + 4 * n0].key < bh0.ar[n0].key) ∧ (4 + 4 * n0 < bh0.size → ¬ bh0.ar[4 + 4 * n0].key < bh0.ar[n0].key) → heap-order(bh0.ar[n0, bh0.ar[2 * n0 + 1]][2 * n0 + 1, bh0.ar[n0]], bh0.size)) ∧ ( 3 + 4 * n0 < bh0.size ∧ bh0.ar[3 + 4 * n0].key < bh0.ar[n0].key ∨ 4 + 4 * n0 < bh0.size ∧ bh0.ar[4 + 4 * n0].key < bh0.ar[n0].key → heap-order (bh0.ar[n0, bh0.ar[2 * n0 + 1]] [2 * n0 + 1, (4 + 4 * n0 < bh0.size ∧ bh0.ar[4 + 4 * n0].key < bh0.ar[3 + 4 * n0].key ⊃ bh0.ar[4 + 4 * n0];bh0.ar[3 + 4 * n0]) ], bh0.size)) ∧ keyset(bh0.ar[n0, bh0.ar[2 * n0 + 1]][2 * n0 + 1, bh0.ar[n0]], bh0.size) = keyset(kar, bh0.size) ∧ ¬ (bh0.size - n0) + 2 * n0 < bh0.size

Rule argument

Additional information

Used simplifier rules: bubble-down-inv: ⊦ bubble-down-inv(n, bh, ar, bh0, ar0) ↔ bh.size ≤ # bh.ar ∧ # bh.ar = # bh0.ar ∧ bh.size = bh0.size ∧ id-idx(ar0, ar) ∧ no-dups-idx(bh.ar, bh.size) ∧ valid-idx(bh.ar, ar, bh.size) ∧ ( ( 2 * n + 1 < bh.size → ¬ bh.ar[2 * n + 1].key < bh.ar[n].key) ∧ ( 2 * n + 2 < bh.size → ¬ bh.ar[2 * n + 2].key < bh.ar[n].key) → heap-order(bh.ar, bh.size)) ∧ ( 2 * n + 1 < bh.size ∧ bh.ar[2 * n + 1].key < bh.ar[n].key ∨ 2 * n + 2 < bh.size ∧ bh.ar[2 * n + 2].key < bh.ar[n].key → heap-order (bh.ar [n, ( 2 * n + 2 < bh.size ∧ bh.ar[2 * n + 2].key < bh.ar[2 * n + 1].key ⊃ bh.ar[2 * n + 2] ;bh.ar[2 * n + 1] ) ], bh.size)) ∧ keyset(bh.ar, bh.size) = keyset(bh0.ar, bh0.size);% ⊦ m < n + 1 ↔ ¬ n < m; (s)%n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s)% ⊦ ¬ n < n; (s)% ⊦ n0 < m0 → (m0 * m + n0 < m0 * n ↔ m < n); (s)% ⊦ m * n + n0 < n ↔ m = 0 ∧ n0 < n; (ws)% ⊦ m +1 = m + 1; (s)%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 ≤ n ↔ ¬ n < m; (ss)% ⊦ ¬ m < n → ¬ m + m0 < n; (s)% ⊦ m < n → n ≠ 0; (s)%fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic% ⊦ m + 1 ≤ n ↔ m < n; (s)%m < # kar ⊦ kar[m, ki][m, ki0] = kar[m, ki0]; (s)% ⊦ id-idx(ar1, ar0[n, ar0[n].idx:= m]) ↔ id-idx(ar1, ar0); (s)%m < # kar ⊦ kar[m, ki][m] = ki; (s)% ⊦ m < n → (n ≤ m ↔ false); (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)%m1 ≠ 0 ⊦ m = (* m1) * m + n0 ↔ 0 = (m1 - 1) * m + n0; (s)%m ≠ n ⊦ kar[m, ki][n] = kar[n]; (s)%n < n0 ⊦ (* n) ≠ m0 + (* n0); (s)%m1 < m2 ⊦ (* m2) * m + n = (* m1) * m + n0 ↔ (m2 - m1) * m + n = n0; (s)% ⊦ (bh.ar:= kar).size = bh.size; (s)%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%mult-c: ⊦ m * n = n * m; from specification nat-mult%mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult% ⊦ m * (n + 1) = m * n + m; (s)% ⊦ # kar[n, ki] = # kar; (s)% ⊦ (bh.ar:= kar).ar = kar; (s)% ⊦ # ar[n, ei] = # ar; (s)% ⊦ bin-heap(kar, m).size = m; (s)% ⊦ bin-heap(kar, m).ar = kar; (s)