[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 24 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), 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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 25:
# kar0 = # kar, kar[n1] = key-index(key1, m2), kar[2 * n1 + 2] = key-index(key0, m1), kar[2 * n1 + 1] = key-index(key, m0), 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

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s)%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic