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

kar[n] = key-index(key1, m2), kar[2 * n + 2] = key-index(key0, m1), kar[2 * n + 1] = key-index(key, m0), ar0 = ar, bh = bin-heap(kar, m3), no-dups-idx(kar, m3), valid-idx(kar, ar, m3), m3 ≤ # kar, 2 * n + 1 < m3 ∧ key < key1 ∨ 2 * n + 2 < m3 ∧ key0 < key1 → heap-order(kar[n, (2 * n + 2 < m3 ∧ key0 < key ⊃ key-index(key0, m1);key-index(key, m0))], m3), (2 * n + 1 < m3 → ¬ key < key1) ∧ (2 * n + 2 < m3 → ¬ key0 < key1) → heap-order(kar, m3) ⊦ ⟪while 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) do let ki = bh.ar[n], ki0 = bh.ar[2 * n + 1] in if 2 * n + 2 < bh.size ∧ bh.ar[2 * n + 2].key < ki0.key then let ki1 = bh.ar[2 * n + 2] in {bh.ar[n] := ki1; ar[ki1.idx].idx := n; bh.ar[2 * n + 2] := ki; ar[ki.idx].idx := 2 * n + 2; n := 2 * n + 2} else {bh.ar[n] := ki0; ar[ki0.idx].idx := n; bh.ar[2 * n + 1] := ki; ar[ki.idx].idx := 2 * n + 1; n := 2 * n + 1}⟫ ( bh.size = m3 ∧ # bh.ar = # kar ∧ id-idx(ar0, ar) ∧ no-dups-idx(bh.ar, bh.size) ∧ valid-idx(bh.ar, ar, bh.size) ∧ heap-order(bh.ar, bh.size) ∧ keyset(kar, bh.size) = keyset(bh.ar, bh.size))

User applied rule invariant right

And obtained the following new goals

Proof step 14:
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), n = n0, 2 * n + 1 < bh.size, bubble-down-inv(n, bh, ar, bin-heap(kar, m3), ar0), no-dups-idx(kar, m3), valid-idx(kar, ar1, m3), m3 ≤ # kar, (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 ⊦ ⟪let ki = bh.ar[n], ki0 = bh.ar[2 * n + 1] in if 2 * n + 2 < bh.size ∧ bh.ar[2 * n + 2].key < ki0.key then let ki1 = bh.ar[2 * n + 2] in {bh.ar[n] := ki1; ar[ki1.idx].idx := n; bh.ar[2 * n + 2] := ki; ar[ki.idx].idx := 2 * n + 2; n := 2 * n + 2} else {bh.ar[n] := ki0; ar[ki0.idx].idx := n; bh.ar[2 * n + 1] := ki; ar[ki.idx].idx := 2 * n + 1; n := 2 * n + 1}⟫ ( ( ( 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)) ∧ ( 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)) ∧ ( 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)) ∧ ( 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)) ∧ bubble-down-inv(n, bh, ar, bin-heap(kar, m3), ar0)) ∧ (n ≤ bh.size ⊃ bh.size - n;0) < (n0 ≤ bh0.size ⊃ bh0.size - n0;0))
Proof step 165:
kar[2 * n1 + 1] = key-index(key, m0), kar[2 * n1 + 2] = key-index(key0, m1), kar[n1] = key-index(key1, m2), ar0 = ar1, bh1 = bin-heap(kar, m3), bubble-down-inv(n, bh, ar, bin-heap(kar, m3), ar0), no-dups-idx(kar, m3), valid-idx(kar, ar1, m3), m3 ≤ # kar, (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.size = m3 ∧ # bh.ar = # kar ∧ id-idx(ar0, ar) ∧ no-dups-idx(bh.ar, bh.size) ∧ valid-idx(bh.ar, ar, bh.size) ∧ heap-order(bh.ar, bh.size) ∧ keyset(kar, bh.size) = keyset(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)

Rule argument

bound: (n ≤ bh.size ⊃ bh.size - n;0) inv: ( 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)) ∧ ( 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)) ∧ ( 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)) ∧ ( 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)) ∧ bubble-down-inv(n, bh, ar, bin-heap(kar, m3), ar0) fmapos: right 1

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);% ⊦ bin-heap(kar, m).size = m; (s)% ⊦ bin-heap(kar, m).ar = kar; (s)% ⊦ id-idx(ar, ar); (s)% ⊦ key-index(key, m).key = key; (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)%fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat%let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat% ⊦ m < n → n ≠ 0; (s)% ⊦ m ≤ n → (n < m ↔ false); (s)% ⊦ m * n + n0 < n ↔ m = 0 ∧ n0 < n; (ws)%mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult%mult-c: ⊦ m * n = n * m; from specification nat-mult%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic% ⊦ m < n → (n ≤ m ↔ false); (s) Used formulas: ( 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)) ∧ ( 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)) ∧ ( 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)) ∧ ( 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)) ∧ bubble-down-inv(n, bh, ar, bin-heap(kar, m3), ar0), (n ≤ bh.size ⊃ bh.size - n;0) = (n ≤ bh.size ⊃ bh.size - n;0)