| # asar0 = m + 1, # asar = m + 1, # zbrar = BRANCH_SIZE, zbrar[n] = mkzbranch(key, adr1, r1), union(asar0, 0, m + 1) = alladrs -- adr0, (( ( (λ n. ⌜zbrar[n].branch?⌝ ∧ btree(r, zbrar[n].child, zbrar[n].adr, height0, true, key-range(zbrar, n, m + 1, ri), iast[adr, ind], asar[n], asar0[n], ok) )⊗_ (0, m + 1 ) * r => mkznode(rp, zbrar, false, true, m + 1)) * P) )(zh0), ((btree(r, r1, adr1, height0, true, key-range(zbrar, n, m + 1, ri), iast[adr, ind], asar[n], asar0[n], ok) * P0))(zh0), n < BRANCH_SIZE, m < BRANCH_SIZE, disj(asar0, 0, m + 1), disj(asar, 0, m + 1), nsize(m + 1, nstat), sorted(zbrar, 0, m), adr0 ∈ alladrs, n ≤ m, asar[n] ⊆ dom iast ++ adr, asar[n] ⊆ asar0[n], ∀ rp, r, adr0, dirty, ri, iast, adr, ind, as, alladrs, nstat, P, zh. ( ((btree(rp, r, adr0, height0, dirty, ri, iast[adr, ind], as, alladrs, nstat) * P))(zh) ↔ ((btree(rp, r, adr0, height0, dirty, ri, iast, as, alladrs, nstat) * P))(zh)) ∨ adr ∈ as ⊦ # alladrs = 0, alladrs = ∅, (( ( (λ n. ⌜zbrar[n].branch?⌝ ∧ btree(r, zbrar[n].child, zbrar[n].adr, height0, true, key-range(zbrar, n, m + 1, ri), iast, asar[n], asar0[n], ok) )⊗_ (0, m + 1 ) * r => mkznode(rp, zbrar, false, true, m + 1)) * P) )(zh0), ((btree(r, r1, adr1, height0, true, key-range(zbrar, n, m + 1, ri), iast, asar[n], asar0[n], ok) * P0))(zh0), adr ∈ union(asar, 0, m + 1), adr0 ∈ union(asar, 0, m + 1) |
Used simplifier rules: btree-imp-dirty: ⊦ (( btree(rp, r, adr, height, dirty, fi, iast, as, alladrs, nstat) * P) )(zh) → (( btree(rp, r, adr, height, true, fi, iast, as, alladrs, nstat) * P) )(zh);%sep-ass: ⊦ (P * P3) * P4 = P * P3 * P4; from specification heap-sep[zheap]%sep-com: ⊦ P * P2 = P2 * P; from specification heap-sep[zheap]% ⊦ adr ∈ asar[n] ∧ n ≤ m → adr ∈ union(asar, 0, m + 1); (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic2%c: ⊦ m + n = n + m; from specification nat-basic2 Used terms: r, r1, adr1, true, key-range(zbrar, n, m + 1, ri), iast, adr, ind, asar[n], asar0[n], ok, P0, zh0