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

# 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

Heuristic elimination applied rule insert elim lemma

And obtained the following new goals

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

Rule argument

spec: bin-min-heap name: elim seq: ⊦ kar = bh.ar ∧ m = bh.size ↔ bh = bin-heap(kar, m) subst: [bh, kar, m] → [bh0, kar0, m]

Additional information

Used simplifier rules: ⊦ kar = bh.ar ∧ m = bh.size ↔ bh = bin-heap(kar, m); (elim) Used terms: bh0, kar0, m