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

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

Heuristic elimination applied rule insert elim lemma

And obtained the following new goals

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

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