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

# zbrar0 = BRANCH_SIZE, # asar = # asar0, # asar2 = # asar0, # asar1 = # asar0, # zbrar = BRANCH_SIZE, # asar0 = (n0 + 1) + n, asar1[n] = asar2[n], asar[n] = asar0[n], zbrar0[n] = mkzbranch(key0, adr1, r4), zbrar[n] = mkzbranch(key0, adr1, r3), union(asar1, 0, # asar0) = union(asar2, 0, # asar0), union(asar, 0, # asar0) = union(asar0, 0, # asar0), ((btree(r, r3, adr1, height0, false, key-range(zbrar, n, # asar0, ri1), iast1, asar2[n], asar2[n], ok) * P))(zh3), (( btree(r2, r4, adr1, height, false, key-range(zbrar0, n, # asar0, ri0), iast0, asar0[n], asar0[n], ok) * (λ n1. ⌜zbrar0[n1].branch?⌝ ∧ btree(r2, zbrar0[n1].child, zbrar0[n1].adr, height, false, key-range(zbrar0, n1, # asar0, ri0), iast0, asar[n1], asar0[n1], ok) )⊗_ (0, n ) * (λ n1. ⌜zbrar0[n1].branch?⌝ ∧ btree(r2, zbrar0[n1].child, zbrar0[n1].adr, height, false, key-range(zbrar0, n1, # asar0, ri0), iast0, asar[n1], asar0[n1], ok) )⊗_ (1 + n, n0 ) * P0) )(zh), n < BRANCH_SIZE, n0 + n < BRANCH_SIZE, ((r => mkznode(rp1, zbrar, false, false, # asar0)))(zh4), ((r2 => mkznode(rp0, zbrar0, false, false, # asar0)))(zh5), disj(asar2, 0, # asar0), disj(asar1, 0, # asar0), disj(asar0, 0, # asar0), disj(asar, 0, # asar0), nsize(# asar0, nstat), sorted(zbrar, 0, n0 + n), sorted(zbrar0, 0, n0 + n), unmodified(adr, mkznode(rp0, zbrar0, false, false, # asar0), iast0), unmodified(adr, mkznode(rp1, zbrar, false, false, # asar0), iast1), adr ∈ iast0, adr ∈ iast1, P ≡ P1 * (λ n1. ⌜zbrar[n1].branch?⌝ ∧ btree(r, zbrar[n1].child, zbrar[n1].adr, height0, false, key-range(zbrar, n1, # asar0, ri1), iast1, asar1[n1], asar2[n1], ok) )⊗_ (1 + n, n0 ) * (λ n1. ⌜zbrar[n1].branch?⌝ ∧ btree(r, zbrar[n1].child, zbrar[n1].adr, height0, false, key-range(zbrar, n1, # asar0, ri1), iast1, asar1[n1], asar2[n1], ok) )⊗_ (0, n ), asar0[n] ⊆ dom iast0, asar2[n] ⊆ dom 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, ∀ n1. ¬ n0 + n < n1 → asar2[n1] ⊆ dom iast1, ∀ n1. ¬ n0 + n < n1 → asar0[n1] ⊆ dom iast0 ⊦ asar0[n] = asar2[n], union(asar0, 0, # asar0) = union(asar2, 0, # asar0), adr ∈ union(asar0, 0, # asar0), adr ∈ union(asar2, 0, # asar0)

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 108:
⊦ ((btree(rp, r, adr, height, dirty, ri, iast, as, alladrs, ok) * P))(zh) ↔ (∃ P0. P0 ≡ P ∧ ((btree(rp, r, adr, height, dirty, ri, iast, as, alladrs, ok) * P0))(zh))
Proof step 109:
# asar0 = (n0 + 1) + n, # zbrar = BRANCH_SIZE, # asar1 = # asar0, # asar2 = # asar0, # asar = # asar0, # zbrar0 = BRANCH_SIZE, zbrar[n] = mkzbranch(key0, adr1, r3), zbrar0[n] = mkzbranch(key0, adr1, r4), asar[n] = asar0[n], asar1[n] = asar2[n], union(asar, 0, # asar0) = union(asar0, 0, # asar0), union(asar1, 0, # asar0) = union(asar2, 0, # asar0), ((btree(r, r3, adr1, height0, false, key-range(zbrar, n, # asar0, ri1), iast1, asar2[n], asar2[n], ok) * P))(zh3), n0 + n < BRANCH_SIZE, n < BRANCH_SIZE, ((r2 => mkznode(rp0, zbrar0, false, false, # asar0)))(zh5), ((r => mkznode(rp1, zbrar, false, false, # asar0)))(zh4), disj(asar, 0, # asar0), disj(asar0, 0, # asar0), disj(asar1, 0, # asar0), disj(asar2, 0, # asar0), nsize(# asar0, nstat), sorted(zbrar0, 0, n0 + n), sorted(zbrar, 0, n0 + n), unmodified(adr, mkznode(rp1, zbrar, false, false, # asar0), iast1), unmodified(adr, mkznode(rp0, zbrar0, false, false, # asar0), iast0), adr ∈ iast1, adr ∈ iast0, P ≡ P1 * (λ n1. ⌜zbrar[n1].branch?⌝ ∧ btree(r, zbrar[n1].child, zbrar[n1].adr, height0, false, key-range(zbrar, n1, # asar0, ri1), iast1, asar1[n1], asar2[n1], ok) )⊗_ (1 + n, n0 ) * (λ n1. ⌜zbrar[n1].branch?⌝ ∧ btree(r, zbrar[n1].child, zbrar[n1].adr, height0, false, key-range(zbrar, n1, # asar0, ri1), iast1, asar1[n1], asar2[n1], ok) )⊗_ (0, n ), iast0 ⊆ iast1, asar2[n] ⊆ dom iast1, asar0[n] ⊆ dom iast0, 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 iast0, ∀ n1. ¬ n0 + n < n1 → asar2[n1] ⊆ 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, ∃ P1. P1 ≡ (λ n1. ⌜zbrar0[n1].branch?⌝ ∧ btree(r2, zbrar0[n1].child, zbrar0[n1].adr, height, false, key-range(zbrar0, n1, # asar0, ri0), iast0, asar[n1], asar0[n1], ok) )⊗_ (0, n ) * (λ n1. ⌜zbrar0[n1].branch?⌝ ∧ btree(r2, zbrar0[n1].child, zbrar0[n1].adr, height, false, key-range(zbrar0, n1, # asar0, ri0), iast0, asar[n1], asar0[n1], ok) )⊗_ (1 + n, n0 ) * P0 ∧ ((btree(r2, r4, adr1, height, false, key-range(zbrar0, n, # asar0, ri0), iast0, asar0[n], asar0[n], ok) * P1))(zh) ⊦ asar0[n] = asar2[n], union(asar0, 0, # asar0) = union(asar2, 0, # asar0), adr ∈ union(asar2, 0, # asar0), adr ∈ union(asar0, 0, # asar0)

Rule argument

spec: <toplevel> name: btree-remove-context seq: ⊦ (( btree (rp, r, adr, height, dirty, ri, iast, as, alladrs, ok) * P) )(zh) ↔ (∃ P0. P0 ≡ P ∧ (( btree (rp, r, adr, height, dirty, ri, iast, as, alladrs, ok) * P0) )(zh)) subst: [zh, P, alladrs, as, iast, ri, dirty, height, adr, r, rp] → [zh, (λ n1. ⌜zbrar0[n1].branch?⌝ ∧ btree (r2, zbrar0[n1].child, zbrar0[n1].adr, height, false, key-range(zbrar0, n1, # asar0, ri0), iast0, asar[n1], asar0[n1], ok) )⊗_ (0, n ) * (λ n1. ⌜zbrar0[n1].branch?⌝ ∧ btree (r2, zbrar0[n1].child, zbrar0[n1].adr, height, false, key-range(zbrar0, n1, # asar0, ri0), iast0, asar[n1], asar0[n1], ok) )⊗_ (1 + n, n0 ) * P0, asar0[n], asar0[n], iast0, key-range(zbrar0, n, # asar0, ri0), false, height, adr1, r4, r2] flags: <all paths>

Additional information

Used terms: zh, (λ n1. ⌜zbrar0[n1].branch?⌝ ∧ btree (r2, zbrar0[n1].child, zbrar0[n1].adr, height, false, key-range(zbrar0, n1, # asar0, ri0), iast0, asar[n1], asar0[n1], ok) )⊗_ (0, n ) * (λ n1. ⌜zbrar0[n1].branch?⌝ ∧ btree (r2, zbrar0[n1].child, zbrar0[n1].adr, height, false, key-range(zbrar0, n1, # asar0, ri0), iast0, asar[n1], asar0[n1], ok) )⊗_ (1 + n, n0 ) * P0, asar0[n], asar0[n], iast0, key-range(zbrar0, n, # asar0, ri0), false, height, adr1, r4, r2