| # asar1 = (n0 + 1) + n, # asar0 = # asar1, # zbrar0 = BRANCH_SIZE, # asar = # asar1, # asar2 = # asar1, adr ∈ as0 ↔ adr ∈ as1, adr ∈ as1 ↔ ¬ dirty1, zbrar0[n] = mkzbranch(key, adr0, r), union(asar2, 0, # asar1) = alladrs0 -- adr, union(asar1, 0, # asar1) = as0 -- adr, union(asar, 0, # asar1) = as1 -- adr, union(asar0, 0, # asar1) = alladrs1 -- adr, ((btree(rp0, r, adr0, height0, dirty1, key-range(zbrar0, n, # asar1, ri1), iast, asar[n], asar0[n], ok) * P2))(zh), ((btree(rp0, r, adr0, height0, dirty1, key-range(zbrar0, n, # asar1, ri0), iast, asar1[n], asar2[n], ok) * P))(zh), n < BRANCH_SIZE, n0 + n < BRANCH_SIZE, n + 1 < BRANCH_SIZE, # asar1 < BRANCH_SIZE, disj(asar2, 0, # asar1), disj(asar1, 0, # asar1), disj(asar, 0, # asar1), disj(asar0, 0, # asar1), sorted(zbrar0, 0, n0 + n), unmodified(adr, mkznode(rp, zbrar0, false, dirty1, # asar1), iast), adr ∈ alladrs1, adr ∈ alladrs0, P2 ≡ P1 * rp0 => mkznode(rp, zbrar0, false, dirty1, # asar1) * (λ n1. ⌜zbrar0[n1].branch?⌝ ∧ btree(rp0, zbrar0[n1].child, zbrar0[n1].adr, height0, dirty1, key-range(zbrar0, n1, # asar1, ri1), iast, asar[n1], asar0[n1], ok) )⊗_ (1 + n, n0 ) * (λ n1. ⌜zbrar0[n1].branch?⌝ ∧ btree(rp0, zbrar0[n1].child, zbrar0[n1].adr, height0, dirty1, key-range(zbrar0, n1, # asar1, ri1), iast, asar[n1], asar0[n1], ok) )⊗_ (0, n ), P ≡ (λ n1. ⌜zbrar0[n1].branch?⌝ ∧ btree(rp0, zbrar0[n1].child, zbrar0[n1].adr, height0, dirty1, key-range(zbrar0, n1, # asar1, ri0), iast, asar1[n1], asar2[n1], ok) )⊗_ (0, n ) * (λ n1. ⌜zbrar0[n1].branch?⌝ ∧ btree(rp0, zbrar0[n1].child, zbrar0[n1].adr, height0, dirty1, key-range(zbrar0, n1, # asar1, ri0), iast, asar1[n1], asar2[n1], ok) )⊗_ (1 + n, n0 ) * rp0 => mkznode(rp, zbrar0, false, dirty1, # asar1) * P0, asar[n] ⊆ asar0[n], asar[n] ⊆ dom iast, as1 ⊆ dom iast, as1 ⊆ alladrs1, as0 ⊆ dom iast, as0 ⊆ alladrs0, asar1[n] ⊆ asar2[n], asar1[n] ⊆ dom iast, dirty1 → dirty, ∀ rp, rp0, adr, dirty, ri0, iast, as0, alladrs0, P0, zh, ri1, as1, alladrs1, P1. ((btree(rp, rp0, adr, height0, dirty, ri0, iast, as0, alladrs0, ok) * P0))(zh) ∧ ((btree(rp, rp0, adr, height0, dirty, ri1, iast, as1, alladrs1, ok) * P1))(zh) ∧ as0 ⊆ alladrs0 ∧ as0 ⊆ dom iast ∧ as1 ⊆ alladrs1 ∧ as1 ⊆ dom iast → ri0 = ri1 ∨ rp0 = null ⊦ # alladrs0 = 0, # alladrs1 = 0, alladrs0 = ∅, alladrs1 = ∅, key-range(zbrar0, n, # asar1, ri0) = key-range(zbrar0, n, # asar1, ri1) |
# asar2 = # asar1, # asar = # asar1, # zbrar0 = BRANCH_SIZE, # asar0 = # asar1, # asar1 = (n0 + 1) + n, adr ∈ as1 ↔ ¬ dirty1, adr ∈ as0 ↔ adr ∈ as1, zbrar0[n] = mkzbranch(key, adr0, r), union(asar0, 0, # asar1) = alladrs1 -- adr, union(asar, 0, # asar1) = as1 -- adr, union(asar1, 0, # asar1) = as0 -- adr, union(asar2, 0, # asar1) = alladrs0 -- adr, ((btree(rp0, r, adr0, height0, dirty1, key-range(zbrar0, n, # asar1, ri0), iast, asar1[n], asar2[n], ok) * P))(zh), ((btree(rp0, r, adr0, height0, dirty1, key-range(zbrar0, n, # asar1, ri1), iast, asar[n], asar0[n], ok) * P2))(zh), # asar1 < BRANCH_SIZE, n + 1 < BRANCH_SIZE, n0 + n < BRANCH_SIZE, n < BRANCH_SIZE, disj(asar0, 0, # asar1), disj(asar, 0, # asar1), disj(asar1, 0, # asar1), disj(asar2, 0, # asar1), sorted(zbrar0, 0, n0 + n), unmodified(adr, mkznode(rp, zbrar0, false, dirty1, # asar1), iast), adr ∈ alladrs0, adr ∈ alladrs1, asar1[n] ⊆ dom iast, asar1[n] ⊆ asar2[n], as0 ⊆ alladrs0, as0 ⊆ dom iast, as1 ⊆ alladrs1, as1 ⊆ dom iast, asar[n] ⊆ dom iast, asar[n] ⊆ asar0[n], dirty1 → dirty, ∀ rp, rp0, adr, dirty, ri0, iast, as0, alladrs0, P0, zh, ri1, as1, alladrs1, P1. ((btree(rp, rp0, adr, height0, dirty, ri0, iast, as0, alladrs0, ok) * P0))(zh) ∧ ((btree(rp, rp0, adr, height0, dirty, ri1, iast, as1, alladrs1, ok) * P1))(zh) ∧ as0 ⊆ alladrs0 ∧ as0 ⊆ dom iast ∧ as1 ⊆ alladrs1 ∧ as1 ⊆ dom iast → ri0 = ri1 ∨ rp0 = null ⊦ # alladrs1 = 0, # alladrs0 = 0, alladrs0 = ∅, alladrs1 = ∅, key-range(zbrar0, n, # asar1, ri0) = key-range(zbrar0, n, # asar1, ri1)