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

# kar0 = # kar, kar[n1] = key-index(key1, m2), kar[2 * n1 + 2] = key-index(key0, m1), kar[2 * n1 + 1] = key-index(key, m0), kar0[2 * n0 + 1] = key-index(key2, m), keyset(kar0, n2 + n0) = keyset(kar, n2 + n0), kar0[n0].idx < # ar, kar0[2 * n0 + 2].idx < # ar, 2 * n0 + 2 < # kar, 2 * n0 + 1 < # kar, n0 < # kar, n0 + 1 < n2, kar0[2 * n0 + 2].key < key2, n0 + 2 < n2, heap-order(kar0[n0, kar0[2 * n0 + 2]], n2 + n0), id-idx(ar1, ar), no-dups-idx(kar, n2 + n0), no-dups-idx(kar0, n2 + n0), valid-idx(kar, ar1, n2 + n0), valid-idx(kar0, ar, n2 + n0), n2 + n0 ≤ # kar, 2 * n1 + 1 < n2 + n0 ∧ key < key1 ∨ 2 * n1 + 2 < n2 + n0 ∧ key0 < key1 → heap-order(kar[n1, (2 * n1 + 2 < n2 + n0 ∧ key0 < key ⊃ key-index(key0, m1);key-index(key, m0))], n2 + n0), (2 * n1 + 1 < n2 + n0 → ¬ key < key1) ∧ (2 * n1 + 2 < n2 + n0 → ¬ key0 < key1) → heap-order(kar, n2 + n0), ¬ key2 < kar0[n0].key ∧ ¬ kar0[2 * n0 + 2].key < kar0[n0].key → heap-order(kar0, n2 + n0), key2 < kar0[n0].key ∨ kar0[2 * n0 + 2].key < kar0[n0].key ⊦ ( 2 * (2 * n0 + 2) + 1 < n2 + n0 → 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 < n2 + n0 → 2 * (2 * n0 + 2) + 2 < # kar)) ∧ no-dups-idx(kar0[n0, kar0[2 * n0 + 2]][2 * n0 + 2, kar0[n0]], n2 + n0) ∧ 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) ], n2 + n0) ∧ ( (2 * (2 * n0 + 2) + 1 < n2 + n0 → ¬ kar0[2 * (2 * n0 + 2) + 1].key < kar0[n0].key) ∧ (2 * (2 * n0 + 2) + 2 < n2 + n0 → ¬ 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]], n2 + n0)) ∧ ( 2 * (2 * n0 + 2) + 1 < n2 + n0 ∧ kar0[2 * (2 * n0 + 2) + 1].key < kar0[n0].key ∨ 2 * (2 * n0 + 2) + 2 < n2 + n0 ∧ 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 < n2 + n0 ∧ kar0[n0, kar0[2 * n0 + 2]][2 * n0 + 2, kar0[n0]][2 * (2 * n0 + 2) + 2].key < kar0[2 * (2 * n0 + 2) + 1].key ⊃ kar0[n0, kar0[2 * n0 + 2]][2 * n0 + 2, kar0[n0]][2 * (2 * n0 + 2) + 2] ;kar0[2 * (2 * n0 + 2) + 1] ) ], n2 + n0)) ∧ keyset(kar0[n0, kar0[2 * n0 + 2]][2 * n0 + 2, kar0[n0]], n2 + n0) = keyset(kar, n2 + n0)

Heuristic elimination applied rule insert elim lemma

And obtained the following new goals

Proof step 29:
# kar0 = # kar, kar0[2 * n0 + 1] = key-index(key2, m), kar[2 * n1 + 1] = key-index(key, m0), kar[2 * n1 + 2] = key-index(key0, m1), kar[n1] = key-index(key1, m2), kar0[2 * n0 + 2] = key-index(key3, m3), keyset(kar0, n2 + n0) = keyset(kar, n2 + n0), n0 + 2 < n2, key3 < key2, n0 + 1 < n2, n0 < # kar, 2 * n0 + 1 < # kar, 2 * n0 + 2 < # kar, m3 < # ar, kar0[n0].idx < # ar, heap-order(kar0[n0, kar0[2 * n0 + 2]], n2 + n0), id-idx(ar1, ar), no-dups-idx(kar0, n2 + n0), no-dups-idx(kar, n2 + n0), valid-idx(kar0, ar, n2 + n0), valid-idx(kar, ar1, n2 + n0), n2 + n0 ≤ # kar, ¬ key2 < kar0[n0].key ∧ ¬ key3 < kar0[n0].key → heap-order(kar0, n2 + n0), (2 * n1 + 1 < n2 + n0 → ¬ key < key1) ∧ (2 * n1 + 2 < n2 + n0 → ¬ key0 < key1) → heap-order(kar, n2 + n0), 2 * n1 + 1 < n2 + n0 ∧ key < key1 ∨ 2 * n1 + 2 < n2 + n0 ∧ key0 < key1 → heap-order(kar[n1, (2 * n1 + 2 < n2 + n0 ∧ key0 < key ⊃ key-index(key0, m1);key-index(key, m0))], n2 + n0), key2 < kar0[n0].key ∨ key3 < kar0[n0].key ⊦ ( 2 * (2 * n0 + 2) + 1 < n2 + n0 → 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 < n2 + n0 → 2 * (2 * n0 + 2) + 2 < # kar)) ∧ no-dups-idx(kar0[n0, kar0[2 * n0 + 2]][2 * n0 + 2, kar0[n0]], n2 + n0) ∧ valid-idx (kar0[n0, kar0[2 * n0 + 2]][2 * n0 + 2, kar0[n0]], ar[m3, ar[m3].idx:= n0][kar0[n0].idx, ar[m3, ar[m3].idx:= n0][kar0[n0].idx].idx:= (2 * n0 + 2)], n2 + n0) ∧ ( (2 * (2 * n0 + 2) + 1 < n2 + n0 → ¬ kar0[2 * (2 * n0 + 2) + 1].key < kar0[n0].key) ∧ (2 * (2 * n0 + 2) + 2 < n2 + n0 → ¬ 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]], n2 + n0)) ∧ ( 2 * (2 * n0 + 2) + 1 < n2 + n0 ∧ kar0[2 * (2 * n0 + 2) + 1].key < kar0[n0].key ∨ 2 * (2 * n0 + 2) + 2 < n2 + n0 ∧ 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 < n2 + n0 ∧ kar0[n0, kar0[2 * n0 + 2]][2 * n0 + 2, kar0[n0]][2 * (2 * n0 + 2) + 2].key < kar0[2 * (2 * n0 + 2) + 1].key ⊃ kar0[n0, kar0[2 * n0 + 2]][2 * n0 + 2, kar0[n0]][2 * (2 * n0 + 2) + 2] ;kar0[2 * (2 * n0 + 2) + 1] ) ], n2 + n0)) ∧ keyset(kar0[n0, kar0[2 * n0 + 2]][2 * n0 + 2, kar0[n0]], n2 + n0) = keyset(kar, n2 + n0)

Rule argument

spec: key-index name: elim seq: ⊦ key = ki.key ∧ m = ki.idx ↔ ki = key-index(key, m) subst: [ki, key, m] → [kar0[2 * n0 + 2], key3, m3]

Additional information

Used simplifier rules: ⊦ key = ki.key ∧ m = ki.idx ↔ ki = key-index(key, m); (elim) Used terms: kar0[2 * n0 + 2], key3, m3