[Imprint][Data Privacy Statement][E-Mail]



View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

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

kar[n1] = key-index(key1, m2), kar[2 * n1 + 2] = key-index(key0, m1), kar[2 * n1 + 1] = key-index(key, m0), ar0 = ar1, bh = bh0, bh1 = bin-heap(kar, m3), ki = bh.ar[n], ki0 = bh.ar[2 * n + 1], n = n0, 2 * n + 1 < # (bh.ar:= bh.ar[n, ki0]).ar, 2 * n + 1 < # bh.ar, n < # bh.ar, 2 * n + 1 < bh.size, ki0.idx < # ar, bubble-down-inv(n, bh, ar, bin-heap(kar, m3), ar0), no-dups-idx(kar, m3), valid-idx(kar, ar1, m3), m3 ≤ # kar, 2 * n + 1 < bh.size → (2 * n + 1 < # bh.ar ∧ n < # bh.ar) ∧ (¬ bh.ar[2 * n + 1].key < bh.ar[n].key → 2 * n + 2 < bh.size → 2 * n + 2 < # bh.ar ∧ n < # bh.ar), 2 * n1 + 1 < m3 ∧ key < key1 ∨ 2 * n1 + 2 < m3 ∧ key0 < key1 → heap-order(kar[n1, (2 * n1 + 2 < m3 ∧ key0 < key ⊃ key-index(key0, m1);key-index(key, m0))], m3), (2 * n1 + 1 < m3 → ¬ key < key1) ∧ (2 * n1 + 2 < m3 → ¬ key0 < key1) → heap-order(kar, m3), 2 * n + 2 < bh.size → 2 * n + 2 < # bh.ar, 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 ⊦ ⟪ar := ar[ki0.idx, ar[ki0.idx].idx:= n][ki.idx, ar[ki0.idx, ar[ki0.idx].idx:= n][ki.idx].idx:= (2 * n + 1)]; n1 := 2 * n + 1⟫ ( ( ( 2 * n1 + 1 < (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).size → ( 2 * n1 + 1 < # (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).ar ∧ n1 < # (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).ar) ∧ ( ¬ (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).ar[2 * n1 + 1].key < (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).ar[n1].key → 2 * n1 + 2 < (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).size → 2 * n1 + 2 < # (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).ar ∧ n1 < # (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).ar)) ∧ ( 2 * n1 + 1 < (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).size → ( 2 * n1 + 1 < # (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).ar ∧ n1 < # (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).ar) ∧ ( ¬ (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).ar[2 * n1 + 1].key < (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).ar[n1].key → 2 * n1 + 2 < (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).size → 2 * n1 + 2 < # (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).ar ∧ n1 < # (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).ar)) ∧ ( 2 * n1 + 1 < (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).size → ( 2 * n1 + 1 < # (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).ar ∧ n1 < # (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).ar) ∧ ( ¬ (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).ar[2 * n1 + 1].key < (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).ar[n1].key → 2 * n1 + 2 < (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).size → 2 * n1 + 2 < # (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).ar ∧ n1 < # (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).ar)) ∧ ( 2 * n1 + 1 < (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).size → ( 2 * n1 + 1 < # (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).ar ∧ n1 < # (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).ar) ∧ ( ¬ (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).ar[2 * n1 + 1].key < (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).ar[n1].key → 2 * n1 + 2 < (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).size → 2 * n1 + 2 < # (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).ar ∧ n1 < # (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).ar)) ∧ bubble-down-inv(n1, bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki], ar, bin-heap(kar, m3), ar0)) ∧ (n1 ≤ (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).size ⊃ (bh.ar:= bh.ar[n, ki0].ar:= (bh.ar:= bh.ar[n, ki0]).ar[2 * n + 1, ki]).size - n1 ;0 ) < (n0 ≤ bh0.size ⊃ bh0.size - n0;0)), 2 * n + 2 < bh.size ∧ bh.ar[2 * n + 2].key < ki0.key

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

Rule argument

Additional information