[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 104 from proof inv-commit-rec-ind (previous step)

# asar = (n1 + n0) + 1, # zbrar2 = BRANCH_SIZE, # asar0 = # asar, zh2[r1] = mkznode(r2, zbrar0, boolvar0, false, m4), istore[adr] = istore3[adr], zh0[r1] = mkznode(r3, zbrar1, boolvar2, true, m2), istore1[adr] = istore3[adr], zbrar2[n0] = mkzbranch(key, adr2, r1), remove-refsize0(istore0) = istore0, remove-refsize0(gstore1) = gstore1, union(asar0, 0, # asar) = alladrs -- adr, alladrs0 ∩ (union(asar, 0, # asar) \ asar[n0]) = ∅, alladrs0 ∩ as0 = ∅, elems nx ∩ ginval1 = ∅, as ∩ as0 = ∅, union(asar, 0, # asar) ∩ as0 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ ginval1, (( btree(r0, r1, adr4, height1, false, key-range(zbrar2, n0, # asar, ri), nodes(istore3) | alladrs0, alladrs0, alladrs0, ok) * (λ n. ⌜zbrar2[n].branch?⌝ ∧ btree (r0, zbrar2[n].child, zbrar2[n].adr, height1, true, key-range(zbrar2, n, # asar, ri), nodes(istore) | union(asar, 0, # asar), asar[n], asar0[n], ok) )⊗_ (0, n0 ) * (λ n. ⌜zbrar2[n].branch?⌝ ∧ btree (r0, zbrar2[n].child, zbrar2[n].adr, height1, true, key-range(zbrar2, n, # asar, ri), nodes(istore) | union(asar, 0, # asar), asar[n], asar0[n], ok) )⊗_ (1 + n0, n1 ) * r0 => mkznode(rp, zbrar2, false, true, # asar) * P) )(zh2), n0 < # asar, n0 < BRANCH_SIZE, n0 + 1 < BRANCH_SIZE, # asar < BRANCH_SIZE, btree-sub-clean(r0, n0, zh0), disj(asar0, 0, # asar), disj(asar, 0, # asar), inv(istore3), inv(istore0), inv(istore1), inv(gstore1), inv(gstore2 \ ginval1), inv(istore), refsize-cons(istore1, as0 ∪ as), refsize-cons(istore, as0 ∪ union(asar, 0, # asar)), refsize-cons(istore3, (as0 ∪ (union(asar, 0, # asar) \ asar[n0])) ∪ alladrs0), sorted(zbrar2, 0, n1 + n0), r1 ∈ zh2, adr ∈ alladrs, m ∈ istore, m3 ∈ istore, m ∈ istore1, r0 ∈ zh1, adr ∈ istore1, r1 ∈ zh0, adr ∈ istore3, adr ∈ istore, m ∈ istore3, m3 ∈ istore3, m1 ∈ istore3, adr4 ∈ alladrs0, adr4 ∈ istore3, alladrs0 ∩ dom nodes(istore) ⊆ dom nodes(istore) ∩ union(asar, 0, # asar), alladrs0 ∩ dom nodes(istore) ⊆ asar0[n0], asar[n0] ⊆ dom nodes(istore), asar[n0] ⊆ dom nodes(istore) ∩ union(asar, 0, # asar), asar[n0] ⊆ asar0[n0], as0 ⊆ dom nodes(istore1), alladrs ⊆ dom nodes(istore1), as ⊆ alladrs, as ⊆ dom nodes(istore1), union(asar, 0, # asar) ∩ dom nodes(istore1) ⊆ as, alladrs0 ∩ dom nodes(istore) ⊆ asar[n0], union(asar, 0, # asar) ∩ dom nodes(istore1) ⊆ alladrs, alladrs0 ⊆ dom nodes(istore3), istore0 ⊑ istore3, istore ⊑ istore3, istore0 ⊑ istore, istore0 ⊑ istore1, istore1 ⊑ istore, istore1 ⊑ istore3, height1 = 0 → asar[n0] = ∅, height1 = 0 → alladrs0 = ∅ ++ adr4, ∀ n. ¬ n1 + n0 < n → asar[n] ⊆ dom nodes(istore) ∩ union(asar, 0, # asar), ∀ n. ¬ n1 + n0 < n → asar[n] ⊆ alladrs, ∀ n. ¬ n1 + n0 < n → asar[n] ⊆ dom nodes(istore), ∀ n. ¬ n1 + n0 < n → asar[n] ⊆ dom nodes(istore1), ∀ n. n < # asar → asar[n] ⊆ alladrs, ∀ n. n < # asar → asar[n] ⊆ dom nodes(istore) ∩ union(asar, 0, # asar), ∀ height0, zh, r0, r, zbrar, boolvar, m0, adr0, adr1, istore1, istore, pstate, m, istore0, gstore0, nx, ginval, as, as0, gstore, rp, dirty, ri, alladrs, P, adr, ino, ns, err, bv. height0 < height1 +1 → zh[r0] = mkznode(r, zbrar, boolvar, true, m0) ∧ adr0 = adr1 ∧ istore1 = istore ∧ pstate = index(m) ∧ remove-refsize0(istore0) = istore0 ∧ remove-refsize0(gstore0) = gstore0 ∧ elems nx ∩ ginval = ∅ ∧ as ∩ as0 = ∅ ∧ dom gstore0 ∪ elems nx = dom gstore ∪ ginval ∧ ((btree(rp, r0, adr1, height0, dirty, ri, nodes(istore) | as, as, alladrs, ok) * P))(zh) ∧ inv(istore0) ∧ inv(istore) ∧ inv(gstore0) ∧ inv(gstore \ ginval) ∧ refsize-cons(istore, as0 ∪ as) ∧ m ∈ istore ∧ r0 ∈ zh ∧ as0 ⊆ dom nodes(istore) ∧ alladrs ⊆ dom nodes(istore) ∧ as ⊆ alladrs ∧ as ⊆ dom nodes(istore) ∧ istore0 ⊑ istore ∧ ¬ dups(nx) ∧ ¬ adr1 ∈ as ∧ (height0 = 0 → as = ∅) → ⟪btree_commit_rec#(r0, adr, istore0, ginval, gstore, gstore0, nx, ino, ns; adr1, err, zh, istore, pstate, bv)⟫ ( istore1 ⊑ istore ∧ (pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore) ∧ (pstate.index? → pstate.lnum ∈ istore) ∧ (pstate = unbuffered → bv) ∧ inv(istore) ∧ istore0 ⊑ istore ∧ r0 ∈ zh ∧ (err = ESUCCESS → ¬ zh[r0].dirty ∧ pstate.index?) ∧ (∃ as1, alladrs1. refsize-cons(istore, as0 ∪ as1) ∧ as1 ∩ dom nodes(istore1) ⊆ as ∧ as1 ∩ as0 = ∅ ∧ alladrs1 ⊆ alladrs ∪ as1 ∧ ((btree(rp, r0, (err = ESUCCESS ⊃ adr1;adr0), height0, err ≠ ESUCCESS, ri, nodes(istore) | as1, as1, alladrs1, ok) * P))(zh))) ⊦ # alladrs = 0, # alladrs0 = 0, alladrs = ∅, alladrs0 = ∅, dups(nx), adr2 ∈ asar[n0], adr ∈ union(asar, 0, # asar), adr ∈ as, mkznode(rp, zbrar2[n0, mkzbranch(key, adr4, r1)], false, true, # asar) = zh2[r0].zbranches:= zbrar2[n0, mkzbranch(key, adr4, r1)] ∧ (( r0 =>_ * bnode (r0, zbrar2[n0, mkzbranch(key, adr4, r1)], 0, # asar, # asar, height1 + 1, true, ri, nodes(istore3) | (alladrs0 ∪ (union(asar, 0, # asar) \ asar[n0])), alladrs0 ∪ ((union(asar, 0, # asar) \ asar[n0]) -- adr), alladrs -- adr) * P) )(zh2)

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 105:
⊦ zh ≡ zh0 -- r → (((r => znd * P0))(zh0) ↔ P0(zh) ∧ zh0[r] = znd ∧ r ∈ zh0)
Proof step 106:
# asar0 = # asar, # zbrar2 = BRANCH_SIZE, # asar = (n1 + n0) + 1, zh2[r0] = mkznode(rp, zbrar2, false, true, # asar), zbrar2[n0] = mkzbranch(key, adr2, r1), istore1[adr] = istore3[adr], zh0[r1] = mkznode(r3, zbrar1, boolvar2, true, m2), istore[adr] = istore3[adr], zh2[r1] = mkznode(r2, zbrar0, boolvar0, false, m4), remove-refsize0(gstore1) = gstore1, remove-refsize0(istore0) = istore0, union(asar0, 0, # asar) = alladrs -- adr, union(asar, 0, # asar) ∩ as0 = ∅, as ∩ as0 = ∅, elems nx ∩ ginval1 = ∅, alladrs0 ∩ as0 = ∅, alladrs0 ∩ (union(asar, 0, # asar) \ asar[n0]) = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ ginval1, (( P * (λ n. ⌜zbrar2[n].branch?⌝ ∧ btree (r0, zbrar2[n].child, zbrar2[n].adr, height1, true, key-range(zbrar2, n, # asar, ri), nodes(istore) | union(asar, 0, # asar), asar[n], asar0[n], ok) )⊗_ (1 + n0, n1 ) * (λ n. ⌜zbrar2[n].branch?⌝ ∧ btree (r0, zbrar2[n].child, zbrar2[n].adr, height1, true, key-range(zbrar2, n, # asar, ri), nodes(istore) | union(asar, 0, # asar), asar[n], asar0[n], ok) )⊗_ (0, n0 ) * btree(r0, r1, adr4, height1, false, key-range(zbrar2, n0, # asar, ri), nodes(istore3) | alladrs0, alladrs0, alladrs0, ok)) )(zh2 -- r0), # asar < BRANCH_SIZE, n0 + 1 < BRANCH_SIZE, n0 < BRANCH_SIZE, n0 < # asar, btree-sub-clean(r0, n0, zh0), disj(asar, 0, # asar), disj(asar0, 0, # asar), inv(istore), inv(gstore2 \ ginval1), inv(gstore1), inv(istore1), inv(istore0), inv(istore3), refsize-cons(istore3, (as0 ∪ (union(asar, 0, # asar) \ asar[n0])) ∪ alladrs0), refsize-cons(istore, as0 ∪ union(asar, 0, # asar)), refsize-cons(istore1, as0 ∪ as), sorted(zbrar2, 0, n1 + n0), adr4 ∈ istore3, adr4 ∈ alladrs0, m1 ∈ istore3, m3 ∈ istore3, m ∈ istore3, adr ∈ istore, adr ∈ istore3, r1 ∈ zh0, adr ∈ istore1, r0 ∈ zh1, m ∈ istore1, m3 ∈ istore, m ∈ istore, adr ∈ alladrs, r1 ∈ zh2, r0 ∈ zh2, zh2 -- r0 ≡ zh2 -- r0, alladrs0 ⊆ dom nodes(istore3), union(asar, 0, # asar) ∩ dom nodes(istore1) ⊆ alladrs, alladrs0 ∩ dom nodes(istore) ⊆ asar[n0], union(asar, 0, # asar) ∩ dom nodes(istore1) ⊆ as, as ⊆ dom nodes(istore1), as ⊆ alladrs, alladrs ⊆ dom nodes(istore1), as0 ⊆ dom nodes(istore1), asar[n0] ⊆ asar0[n0], asar[n0] ⊆ dom nodes(istore) ∩ union(asar, 0, # asar), asar[n0] ⊆ dom nodes(istore), alladrs0 ∩ dom nodes(istore) ⊆ asar0[n0], alladrs0 ∩ dom nodes(istore) ⊆ dom nodes(istore) ∩ union(asar, 0, # asar), istore1 ⊑ istore3, istore1 ⊑ istore, istore0 ⊑ istore1, istore0 ⊑ istore, istore ⊑ istore3, istore0 ⊑ istore3, height1 = 0 → alladrs0 = ∅ ++ adr4, height1 = 0 → asar[n0] = ∅, ∀ n. n < # asar → asar[n] ⊆ dom nodes(istore) ∩ union(asar, 0, # asar), ∀ n. n < # asar → asar[n] ⊆ alladrs, ∀ n. ¬ n1 + n0 < n → asar[n] ⊆ dom nodes(istore1), ∀ n. ¬ n1 + n0 < n → asar[n] ⊆ dom nodes(istore), ∀ n. ¬ n1 + n0 < n → asar[n] ⊆ alladrs, ∀ n. ¬ n1 + n0 < n → asar[n] ⊆ dom nodes(istore) ∩ union(asar, 0, # asar), ∀ height0, zh, r0, r, zbrar, boolvar, m0, adr0, adr1, istore1, istore, pstate, m, istore0, gstore0, nx, ginval, as, as0, gstore, rp, dirty, ri, alladrs, P, adr, ino, ns, err, bv. height0 < height1 +1 → zh[r0] = mkznode(r, zbrar, boolvar, true, m0) ∧ adr0 = adr1 ∧ istore1 = istore ∧ pstate = index(m) ∧ remove-refsize0(istore0) = istore0 ∧ remove-refsize0(gstore0) = gstore0 ∧ elems nx ∩ ginval = ∅ ∧ as ∩ as0 = ∅ ∧ dom gstore0 ∪ elems nx = dom gstore ∪ ginval ∧ ((btree(rp, r0, adr1, height0, dirty, ri, nodes(istore) | as, as, alladrs, ok) * P))(zh) ∧ inv(istore0) ∧ inv(istore) ∧ inv(gstore0) ∧ inv(gstore \ ginval) ∧ refsize-cons(istore, as0 ∪ as) ∧ m ∈ istore ∧ r0 ∈ zh ∧ as0 ⊆ dom nodes(istore) ∧ alladrs ⊆ dom nodes(istore) ∧ as ⊆ alladrs ∧ as ⊆ dom nodes(istore) ∧ istore0 ⊑ istore ∧ ¬ dups(nx) ∧ ¬ adr1 ∈ as ∧ (height0 = 0 → as = ∅) → ⟪btree_commit_rec#(r0, adr, istore0, ginval, gstore, gstore0, nx, ino, ns; adr1, err, zh, istore, pstate, bv)⟫ ( istore1 ⊑ istore ∧ (pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore) ∧ (pstate.index? → pstate.lnum ∈ istore) ∧ (pstate = unbuffered → bv) ∧ inv(istore) ∧ istore0 ⊑ istore ∧ r0 ∈ zh ∧ (err = ESUCCESS → ¬ zh[r0].dirty ∧ pstate.index?) ∧ (∃ as1, alladrs1. refsize-cons(istore, as0 ∪ as1) ∧ as1 ∩ dom nodes(istore1) ⊆ as ∧ as1 ∩ as0 = ∅ ∧ alladrs1 ⊆ alladrs ∪ as1 ∧ ((btree(rp, r0, (err = ESUCCESS ⊃ adr1;adr0), height0, err ≠ ESUCCESS, ri, nodes(istore) | as1, as1, alladrs1, ok) * P))(zh))) ⊦ # alladrs0 = 0, # alladrs = 0, alladrs = ∅, alladrs0 = ∅, dups(nx), adr ∈ as, adr ∈ union(asar, 0, # asar), adr2 ∈ asar[n0], mkznode(rp, zbrar2[n0, mkzbranch(key, adr4, r1)], false, true, # asar) = zh2[r0].zbranches:= zbrar2[n0, mkzbranch(key, adr4, r1)] ∧ (( r0 =>_ * bnode (r0, zbrar2[n0, mkzbranch(key, adr4, r1)], 0, # asar, # asar, height1 + 1, true, ri, nodes(istore3) | (alladrs0 ∪ (union(asar, 0, # asar) \ asar[n0])), alladrs0 ∪ ((union(asar, 0, # asar) \ asar[n0]) -- adr), alladrs -- adr) * P) )(zh2)

Rule argument

spec: separation, inst: zheap name: free-known seq: ⊦ zh ≡ zh0 -- r → (((r => znd * P0))(zh0) ↔ P0(zh) ∧ zh0[r] = znd ∧ r ∈ zh0) subst: [zh, zh0, P0, znd, r] → [zh2 -- r0, zh2, P * (λ n. ⌜zbrar2[n].branch?⌝ ∧ btree (r0, zbrar2[n].child, zbrar2[n].adr, height1, true, key-range(zbrar2, n, # asar, ri), nodes(istore) | union(asar, 0, # asar), asar[n], asar0[n], ok) )⊗_ (1 + n0, n1 ) * (λ n. ⌜zbrar2[n].branch?⌝ ∧ btree (r0, zbrar2[n].child, zbrar2[n].adr, height1, true, key-range(zbrar2, n, # asar, ri), nodes(istore) | union(asar, 0, # asar), asar[n], asar0[n], ok) )⊗_ (0, n0 ) * btree (r0, r1, adr4, height1, false, key-range(zbrar2, n0, # asar, ri), nodes(istore3) | alladrs0, alladrs0, alladrs0, ok), mkznode(rp, zbrar2, false, true, # asar), r0] flags: <all paths>

Additional information

Used simplifier rules: ⊦ zh ≡ zh; (s)%sep-ass: ⊦ (P * P3) * P4 = P * P3 * P4; from specification heap-sep[zheap]%sep-com: ⊦ P * P2 = P2 * P; from specification heap-sep[zheap] Used terms: zh2 -- r0, zh2, P * (λ n. ⌜zbrar2[n].branch?⌝ ∧ btree (r0, zbrar2[n].child, zbrar2[n].adr, height1, true, key-range(zbrar2, n, # asar, ri), nodes(istore) | union(asar, 0, # asar), asar[n], asar0[n], ok) )⊗_ (1 + n0, n1 ) * (λ n. ⌜zbrar2[n].branch?⌝ ∧ btree (r0, zbrar2[n].child, zbrar2[n].adr, height1, true, key-range(zbrar2, n, # asar, ri), nodes(istore) | union(asar, 0, # asar), asar[n], asar0[n], ok) )⊗_ (0, n0 ) * btree (r0, r1, adr4, height1, false, key-range(zbrar2, n0, # asar, ri), nodes(istore3) | alladrs0, alladrs0, alladrs0, ok), mkznode(rp, zbrar2, false, true, # asar), r0