Proof step 16 from proof prepost-extract-min (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 17:

  ar0 = ar, bh = bin-heap(kar, m), bh0 = bh1.ar:= bh1.ar[0, bh1.ar[bh1.size]], bh1 = bin-heap(kar, m - 1), 2exp-size(# kar), 0 < # bh.ar, 0 < # bh1.ar, bh1.size < # bh1.ar, heap-order(kar, m), no-dups-idx(kar, m), valid-idx(kar, ar, m), m ≤ # kar, m ≥ 1, ∃ key. key-index(key, bh.ar[0].idx) ∈ keyset(kar, m) ∧ (∀ ki. ki ∈ keyset(kar, m) → ¬ ki.key < key) ⊦ ⟪ar[bh0.ar[0].idx].idx := 0; bin_min_heap_bubble_down#(0; bh0, ar)⟫ ( bh0.size ≤ # bh0.ar ∧ no-dups-idx(bh0.ar, bh0.size) ∧ valid-idx(bh0.ar, ar, bh0.size) ∧ 2exp-size(# bh0.ar) ∧ heap-order(bh0.ar, bh0.size) ∧ id-idx(ar0, ar) ∧ (∃ key. key-index(key, bh.ar[0].idx) ∈ keyset(kar, m) ∧ keyset(bh0.ar, bh0.size) = keyset(kar, m) -- key-index(key, bh.ar[0].idx) ∧ (∀ ki. ki ∈ keyset(kar, m) → ¬ ki.key < key))), # keyset(kar, m) = 0, bh1.size = 0, keyset(kar, m) = ∅

Rule argument

Additional information

Used simplifier rules: ⊦ bin-heap(kar, m).size = m; (s)% ⊦ bin-heap(kar, m).ar = kar; (s)% ⊦ n ≥ m ↔ m ≤ n; (s)% ⊦ m ≤ n → (n - m = 0 ↔ n = m); (s)% ⊦ 0 < m ↔ m ≠ 0; (s)% ⊦ m ≠ n → (m ≤ n ↔ m < n); (s)% ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s)% ⊦ m ≠ 0 → (1 < m ↔ m ≠ 1); (ss)%n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s)% ⊦ m < n + 1 ↔ ¬ n < m; (s)% ⊦ m ≤ n → (n < m ↔ false); (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic