| # zbrar0 = BRANCH_SIZE, # asar = m + 1, # asar0 = m + 1, # zbrar = BRANCH_SIZE, # asar1 = m + 1, # asar2 = m + 1, union(asar, 0, m + 1) = union(asar0, 0, m + 1), union(asar1, 0, m + 1) = union(asar2, 0, m + 1), (( (λ n. ⌜zbrar0[n].branch?⌝ ∧ btree(r2, zbrar0[n].child, zbrar0[n].adr, height, false, key-range(zbrar0, n, m + 1, ri0), iast0, asar[n], asar0[n], ok) )⊗_ (0, m + 1 ) * P0) )(zh), (( (λ n. ⌜zbrar[n].branch?⌝ ∧ btree(r, zbrar[n].child, zbrar[n].adr, height0, false, key-range(zbrar, n, m + 1, ri1), iast1, asar1[n], asar2[n], ok) )⊗_ (0, m + 1 ) * P1) )(zh3), m < BRANCH_SIZE, ((r2 => mkznode(rp0, zbrar0, false, false, m + 1)))(zh5), ((r => mkznode(rp1, zbrar, false, false, m + 1)))(zh4), disj(asar, 0, m + 1), disj(asar0, 0, m + 1), disj(asar1, 0, m + 1), disj(asar2, 0, m + 1), nsize(m + 1, nstat), sorted(zbrar0, 0, m), sorted(zbrar, 0, m), unmodified(adr, mkznode(rp1, zbrar, false, false, m + 1), iast1), unmodified(adr, mkznode(rp0, zbrar0, false, false, m + 1), iast0), adr ∈ iast1, adr ∈ iast0, iast0 ⊆ iast1, zh5 ⊥ zh, zh4 ⊥ zh3, (r0 = null ⊃ P0(zh0);r2 = r0 ∧ zh5 ∪ zh = zh0), (r1 = null ⊃ P1(zh1);r = r1 ∧ zh4 ∪ zh3 = zh1), ∀ n. ¬ m < n → asar0[n] ⊆ dom iast0, ∀ n. ¬ m < n → asar2[n] ⊆ dom iast1, ∀ rp1, r1, adr, height1, ri1, iast1, alladrs1, nstat, P1, zh1, rp0, r0, ri0, iast0, alladrs0, P0, zh0. ((btree(rp1, r1, adr, height1, false, ri1, iast1, alladrs1, alladrs1, nstat) * P1))(zh1) ∧ ((btree(rp0, r0, adr, height, false, ri0, iast0, alladrs0, alladrs0, nstat) * P0))(zh0) ∧ alladrs1 ⊆ dom iast1 ∧ alladrs0 ⊆ dom iast0 ∧ iast0 ⊆ iast1 → height = height1 ∧ ri0 = ri1 ∧ alladrs0 = alladrs1 ⊦ asar0 = asar2, union(asar0, 0, m + 1) = union(asar2, 0, m + 1), adr ∈ union(asar2, 0, m + 1), adr ∈ union(asar0, 0, m + 1) |
⊦ asar = asar0 ↔ # asar = # asar0 ∧ (∀ n. n < # asar → asar[n] = asar0[n])
# asar2 = m + 1, # asar1 = m + 1, # zbrar = BRANCH_SIZE, # asar0 = m + 1, # asar = m + 1, # zbrar0 = BRANCH_SIZE, union(asar1, 0, m + 1) = union(asar2, 0, m + 1), union(asar, 0, m + 1) = union(asar0, 0, m + 1), (( (λ n. ⌜zbrar[n].branch?⌝ ∧ btree(r, zbrar[n].child, zbrar[n].adr, height0, false, key-range(zbrar, n, m + 1, ri1), iast1, asar1[n], asar2[n], ok) )⊗_ (0, m + 1 ) * P1) )(zh3), (( (λ n. ⌜zbrar0[n].branch?⌝ ∧ btree(r2, zbrar0[n].child, zbrar0[n].adr, height, false, key-range(zbrar0, n, m + 1, ri0), iast0, asar[n], asar0[n], ok) )⊗_ (0, m + 1 ) * P0) )(zh), m < BRANCH_SIZE, ((r => mkznode(rp1, zbrar, false, false, m + 1)))(zh4), ((r2 => mkznode(rp0, zbrar0, false, false, m + 1)))(zh5), disj(asar2, 0, m + 1), disj(asar1, 0, m + 1), disj(asar0, 0, m + 1), disj(asar, 0, m + 1), nsize(m + 1, nstat), sorted(zbrar, 0, m), sorted(zbrar0, 0, m), unmodified(adr, mkznode(rp0, zbrar0, false, false, m + 1), iast0), unmodified(adr, mkznode(rp1, zbrar, false, false, m + 1), iast1), adr ∈ iast0, adr ∈ iast1, iast0 ⊆ iast1, zh4 ⊥ zh3, zh5 ⊥ zh, (r1 = null ⊃ P1(zh1);r = r1 ∧ zh4 ∪ zh3 = zh1), (r0 = null ⊃ P0(zh0);r2 = r0 ∧ zh5 ∪ zh = zh0), ∀ rp1, r1, adr, height1, ri1, iast1, alladrs1, nstat, P1, zh1, rp0, r0, ri0, iast0, alladrs0, P0, zh0. ((btree(rp1, r1, adr, height1, false, ri1, iast1, alladrs1, alladrs1, nstat) * P1))(zh1) ∧ ((btree(rp0, r0, adr, height, false, ri0, iast0, alladrs0, alladrs0, nstat) * P0))(zh0) ∧ alladrs1 ⊆ dom iast1 ∧ alladrs0 ⊆ dom iast0 ∧ iast0 ⊆ iast1 → height = height1 ∧ ri0 = ri1 ∧ alladrs0 = alladrs1, ∀ n. ¬ m < n → asar2[n] ⊆ dom iast1, ∀ n. ¬ m < n → asar0[n] ⊆ dom iast0 ⊦ union(asar0, 0, m + 1) = union(asar2, 0, m + 1), adr ∈ union(asar0, 0, m + 1), adr ∈ union(asar2, 0, m + 1), # asar0 = # asar2 ∧ (∀ n. n < # asar0 → asar0[n] = asar2[n])
Used terms: asar2, asar0