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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 18:

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

• Proof step 85:

  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), bh1.size < # bh1.ar, 0 < # bh1.ar, 0 < # bh.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) ⊦ # keyset(kar, m) = 0, bh1.size = 0, keyset(kar, m) = ∅, bh0.ar[0].idx < # ar ∧ 0 < # bh0.ar ∧ bh0.ar[0].idx < # ar ∧ 0 < # bh0.ar

Rule argument

Additional information