| zh1[r0] = mkznode(r1, zbrar, false, true, m0), adr = zh[r].zbranches[n].adr, err = ESUCCESS, err0 = ESUCCESS, gstore0 = gstore2, istore1 = istore2, n = n0, n1 = 0, pstate0 = index(m), r = r0, rc = zh[r].zbranches[n].child, remove-refsize0(gstore1) = gstore1, remove-refsize0(istore0) = istore0, zh = zh0, as ∩ as0 = ∅, elems nx ∩ ginval1 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ ginval1, ((btree(rp, r0, adr3, height, dirty, ri, nodes(istore2) | as, as, alladrs, ok) * P))(zh1), n < zh[r].usedsize, n < # zh[r].zbranches, commit-inv(n, pstate, istore1, istore0, nx, gstore2, gstore1, ginval1, syn, err, rp, r, adr3, height, dirty, ri, istore, as, as0, alladrs, P, zh), inv(gstore2 \ ginval1), inv(gstore1), inv(istore2), inv(istore0), refsize-cons(istore2, as0 ∪ as), r0 ∈ zh1, m ∈ istore2, as ⊆ dom nodes(istore2), as ⊆ alladrs, alladrs ⊆ dom nodes(istore2), as0 ⊆ dom nodes(istore2), istore0 ⊑ istore2, height = 0 → as = ∅, ∀ 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 < height → 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))) ⊦ dups(nx), adr3 ∈ as, rc ≠ null ∧ zh[rc].dirty, commit-inv (n + 1, pstate, istore1, istore0, nx, gstore2, gstore1, ginval1, syn, err, rp, r, adr3, height, dirty, ri, istore, as, as0, alladrs, P, zh) ∧ zh[r].usedsize - n + 1 < zh0[r].usedsize - n0 |
zh1[r0] = mkznode(r1, zbrar, false, true, m0), remove-refsize0(gstore1) = gstore1, remove-refsize0(istore0) = istore0, as ∩ as0 = ∅, elems nx ∩ ginval1 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ ginval1, ((btree(rp, r0, adr3, height, dirty, ri, nodes(istore2) | as, as, alladrs, ok) * P))(zh1), n0 < zh0[r0].usedsize, n0 < # zh0[r0].zbranches, commit-inv (n0, pstate, istore2, istore0, nx, gstore2, gstore1, ginval1, syn, ESUCCESS, rp, r0, adr3, height, dirty, ri, istore, as, as0, alladrs, P, zh0), inv(gstore2 \ ginval1), inv(gstore1), inv(istore2), inv(istore0), refsize-cons(istore2, as0 ∪ as), r0 ∈ zh1, m ∈ istore2, as ⊆ dom nodes(istore2), as ⊆ alladrs, alladrs ⊆ dom nodes(istore2), as0 ⊆ dom nodes(istore2), istore0 ⊑ istore2, height = 0 → as = ∅, ∀ 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 < height → 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))) ⊦ commit-inv (n0 + 1, pstate, istore2, istore0, nx, gstore2, gstore1, ginval1, syn, ESUCCESS, rp, r0, adr3, height, dirty, ri, istore, as, as0, alladrs, P, zh0), dups(nx), adr3 ∈ as, zh0[r0].zbranches[n0].child ≠ null ∧ zh0[zh0[r0].zbranches[n0].child].dirty
Used simplifier rules: ⊦ as ⊆ as; (s)% ⊦ as ⊆ dom iast → dom(iast | as) = as; (s)% ⊦ m < n → n ≠ 0; (s)%sub-trans: ⊦ as ⊆ as0 ∧ as0 ⊆ as1 → as ⊆ as1; (forward) from specification set-basic[node-store]%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%sep-com: ⊦ P * P2 = P2 * P; from specification heap-sep[zheap]%sep-ass: ⊦ (P * P3) * P4 = P * P3 * P4; from specification heap-sep[zheap]%btree-adrs: ⊦ (( btree (rp, rp0, adr0, height, dirty, fi, iast, as, alladrs, nstat) * P) )(zh) → as ⊆ dom iast; (forward) from specification btree-inv% ⊦ ¬ n < n; (s)% ⊦ m < n + 1 ↔ ¬ n < m; (s)% ⊦ n < m → (m - n) + n = m; (s)%n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s)%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ m < n → (n ≤ m ↔ false); (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ m + 1 ≤ n ↔ m < n; (s)