[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 22 from proof prepost-bubble-down (previous step)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 23:
# bh0.ar = # kar, kar[2 * n1 + 1] = key-index(key, m0), kar[2 * n1 + 2] = key-index(key0, m1), kar[n1] = key-index(key1, m2), keyset(bh0.ar, bh0.size) = keyset(kar, bh0.size), 2 * n0 + 2 < bh0.size, bh0.ar[2 * n0 + 2].key < bh0.ar[2 * n0 + 1].key, 2 * n0 + 1 < bh0.size, n0 < # kar, 2 * n0 + 1 < # kar, 2 * n0 + 2 < # kar, bh0.ar[2 * n0 + 2].idx < # ar, bh0.ar[n0].idx < # ar, heap-order(bh0.ar[n0, bh0.ar[2 * n0 + 2]], 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 ∧ ¬ 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, 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), bh0.ar[2 * n0 + 1].key < bh0.ar[n0].key ∨ bh0.ar[2 * n0 + 2].key < bh0.ar[n0].key ⊦ ( 2 * (2 * n0 + 2) + 1 < bh0.size → 2 * (2 * n0 + 2) + 1 < # kar ∧ ( ¬ bh0.ar[n0, bh0.ar[2 * n0 + 2]][2 * (2 * n0 + 2) + 1].key < bh0.ar[n0].key → 2 * (2 * n0 + 2) + 2 < bh0.size → 2 * (2 * n0 + 2) + 2 < # kar)) ∧ no-dups-idx(bh0.ar[n0, bh0.ar[2 * n0 + 2]][2 * n0 + 2, bh0.ar[n0]], bh0.size) ∧ valid-idx (bh0.ar[n0, bh0.ar[2 * n0 + 2]][2 * n0 + 2, bh0.ar[n0]], ar[bh0.ar[2 * n0 + 2].idx, ar[bh0.ar[2 * n0 + 2].idx].idx:= n0] [bh0.ar[n0].idx, ar[bh0.ar[2 * n0 + 2].idx, ar[bh0.ar[2 * n0 + 2].idx].idx:= n0][bh0.ar[n0].idx].idx:= (2 * n0 + 2) ], bh0.size) ∧ ( (2 * (2 * n0 + 2) + 1 < bh0.size → ¬ bh0.ar[n0, bh0.ar[2 * n0 + 2]][2 * (2 * n0 + 2) + 1].key < bh0.ar[n0].key) ∧ (2 * (2 * n0 + 2) + 2 < bh0.size → ¬ bh0.ar[n0, bh0.ar[2 * n0 + 2]][2 * n0 + 2, bh0.ar[n0]][2 * (2 * n0 + 2) + 2].key < bh0.ar[n0].key) → heap-order(bh0.ar[n0, bh0.ar[2 * n0 + 2]][2 * n0 + 2, bh0.ar[n0]], bh0.size)) ∧ ( 2 * (2 * n0 + 2) + 1 < bh0.size ∧ bh0.ar[n0, bh0.ar[2 * n0 + 2]][2 * (2 * n0 + 2) + 1].key < bh0.ar[n0].key ∨ 2 * (2 * n0 + 2) + 2 < bh0.size ∧ bh0.ar[n0, bh0.ar[2 * n0 + 2]][2 * n0 + 2, bh0.ar[n0]][2 * (2 * n0 + 2) + 2].key < bh0.ar[n0].key → heap-order (bh0.ar[n0, bh0.ar[2 * n0 + 2]] [2 * n0 + 2, ( 2 * (2 * n0 + 2) + 2 < bh0.size ∧ bh0.ar[n0, bh0.ar[2 * n0 + 2]][2 * n0 + 2, bh0.ar[n0]][2 * (2 * n0 + 2) + 2].key < bh0.ar[n0, bh0.ar[2 * n0 + 2]][2 * (2 * n0 + 2) + 1].key ⊃ bh0.ar[n0, bh0.ar[2 * n0 + 2]][2 * n0 + 2, bh0.ar[n0]][2 * (2 * n0 + 2) + 2] ;bh0.ar[n0, bh0.ar[2 * n0 + 2]][2 * (2 * n0 + 2) + 1] ) ], bh0.size)) ∧ keyset(bh0.ar[n0, bh0.ar[2 * n0 + 2]][2 * n0 + 2, bh0.ar[n0]], bh0.size) = keyset(kar, bh0.size) ∧ bh0.size < (bh0.size - n0) + 2 * n0 + 2

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 + 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 → 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%n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s)% ⊦ m < 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)%m ≠ n ⊦ kar[m, ki][n] = kar[n]; (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% ⊦ 2 * m ≠ 2 * n + 1; (s)%n < n0 ⊦ m + (* n) = m0 + (* n0) ↔ m = m0 + (n0 - n); (s)% ⊦ (bh.ar:= kar).size = bh.size; (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)