[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 85 from proof btree-clean-fwd (previous step)

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

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 86:
⊦ m0 < m → nP0 ⊗_(n, m) = nP0 ⊗_(n, m0) * nP0(n + m0) * nP0 ⊗_(n + m0 + 1, m - m0 - 1)
Proof step 87:
# zbrar0 = BRANCH_SIZE, # asar = (n0 + n) + 1, # asar0 = # asar, # zbrar = BRANCH_SIZE, # asar1 = # asar, # asar2 = # asar, asar1[n] = asar2[n], zbrar[n] = mkzbranch(key, adr0, r3), zbrar0[n] = mkzbranch(key, adr0, r4), union(asar, 0, # asar) = union(asar0, 0, # asar), union(asar1, 0, # asar) = union(asar2, 0, # asar), (( ( ( btree(r, r3, adr0, height0, false, key-range(zbrar, n, # asar, ri1), iast, asar2[n], asar2[n], ok) * (λ n1. ⌜zbrar[n1].branch?⌝ ∧ btree(r, zbrar[n1].child, zbrar[n1].adr, height0, false, key-range(zbrar, n1, # asar, ri1), iast, asar1[n1], asar2[n1], ok) )⊗_ (0, n )) * (λ n1. ⌜zbrar[n1].branch?⌝ ∧ btree(r, zbrar[n1].child, zbrar[n1].adr, height0, false, key-range(zbrar, n1, # asar, ri1), iast, asar1[n1], asar2[n1], ok) )⊗_ (1 + n, n0 )) * P1) )(zh3), (( ( (λ n1. ⌜zbrar0[n1].branch?⌝ ∧ btree(r2, zbrar0[n1].child, zbrar0[n1].adr, height, false, key-range(zbrar0, n1, # asar, ri0), iast, asar[n1], asar0[n1], ok) )⊗_ (0, n ) * ( ⌜zbrar0[0 + n].branch?⌝ ∧ btree (r2, zbrar0[0 + n].child, zbrar0[0 + n].adr, height, false, key-range(zbrar0, 0 + n, # asar, ri0), iast, asar[0 + n], asar0[0 + n], ok)) * (λ n1. ⌜zbrar0[n1].branch?⌝ ∧ btree(r2, zbrar0[n1].child, zbrar0[n1].adr, height, false, key-range(zbrar0, n1, # asar, ri0), iast, asar[n1], asar0[n1], ok) )⊗_ (0 + n + 1, # asar - n - 1 )) * P0) )(zh), n < BRANCH_SIZE, n0 + n < BRANCH_SIZE, n < # asar, ((r2 => mkznode(rp0, zbrar0, false, false, # asar)))(zh5), ((r => mkznode(rp1, zbrar, false, false, # asar)))(zh4), disj(asar, 0, # asar), disj(asar0, 0, # asar), disj(asar1, 0, # asar), disj(asar2, 0, # asar), nsize(# asar, nstat), sorted(zbrar0, 0, n0 + n), sorted(zbrar, 0, n0 + n), unmodified(adr, mkznode(rp1, zbrar, false, false, # asar), iast), unmodified(adr, mkznode(rp0, zbrar0, false, false, # asar), iast), adr ∈ iast, asar2[n] ⊆ dom iast, zh5 ⊥ zh, zh4 ⊥ zh3, (r0 = null ⊃ P0(zh0);r2 = r0 ∧ zh5 ∪ zh = zh0), (r1 = null ⊃ P1(zh1);r = r1 ∧ zh4 ∪ zh3 = zh1), ∀ n1. ¬ n0 + n < n1 → asar0[n1] ⊆ dom iast, ∀ n1. ¬ n0 + n < n1 → asar2[n1] ⊆ dom iast, ∀ rp0, r0, adr, ri0, iast, as0, alladrs0, nstat, P0, zh0, rp1, r1, height1, ri1, as1, alladrs1, P1, zh1. ((btree(rp0, r0, adr, height, false, ri0, iast, as0, alladrs0, nstat) * P0))(zh0) ∧ ((btree(rp1, r1, adr, height1, false, ri1, iast, as1, alladrs1, nstat) * P1))(zh1) → height = height1 ∧ as0 = as1 ∧ ri0 = ri1 ∧ alladrs0 = alladrs1 ⊦ asar0[n] = asar2[n], union(asar0, 0, # asar) = union(asar2, 0, # asar), adr ∈ union(asar2, 0, # asar), adr ∈ union(asar0, 0, # asar)

Rule argument

spec: iter-n, inst: zheap name: Sep-unfold seq: ⊦ m0 < m → nP0 ⊗_(n, m) = nP0 ⊗_(n, m0) * nP0(n + m0) * nP0 ⊗_(n + m0 + 1, m - m0 - 1) subst: [m0, m, n, nP0] → [n, # asar, 0, λ n1. ⌜zbrar0[n1].branch?⌝ ∧ btree (r2, zbrar0[n1].child, zbrar0[n1].adr, height, false, key-range(zbrar0, n1, # asar, ri0), iast, asar[n1], asar0[n1], ok)] flags: <all paths>

Additional information

Used simplifier rules: nat-le-eq: ⊦ n = n0 + n1 → (n ≤ n0 ↔ n1 = 0 ∧ n = n0);% ⊦ m < n ↔ ¬ n ≤ m; (ss)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic% ⊦ m + 1 ≠ 0; (s) Used terms: n, # asar, 0, λ n1. ⌜zbrar0[n1].branch?⌝ ∧ btree (r2, zbrar0[n1].child, zbrar0[n1].adr, height, false, key-range(zbrar0, n1, # asar, ri0), iast, asar[n1], asar0[n1], ok)