| syn ↔ true, istore1[m0] = indexblock(indx, lax, m3), zh[rp] = mkznode(r, zbrar, boolvar, true, m), zh0[rp] = mkznode(r0, zbrar0, boolvar0, false, m4), ginval0 = ginval1, gstore = gstore3, gstore0 = gstore4, istore = istore1, istore0 = istore2, maxino = maxino2, maxino0 = m0, n = istore1[m0].ref-size - m2, pstate = readonly, remove-refsize0(istore2) = istore2, remove-refsize0(gstore3) = gstore3, elems nx ∩ ginval1 = ∅, dom remove-refsize0(gstore4) ∩ ginval1 = ∅, dom gstore3 ∪ elems nx = dom gstore4 ∪ ginval1, btree-inv(rp, adr, istore3[n0, indexblock([], [], 0)], istore2, zh, ri, fi), btree-inv(rp, adr, istore3, istore2, zh, ri, fi), btree-inv(rp, @(m0, m1, m2), istore1, istore1, zh0, ri, ri), btree-inv(rp, adr, istore1[m0, indexblock(indx, lax, m3 - m2)], istore2, zh0[rp, mkznode(r0, zbrar0, boolvar0, true, m4)], ri, fi), inv(istore3[n0, indexblock([], [], 0)]), inv(istore3), inv(istore1), inv(istore2), inv(gstore3), inv(gstore4 \ ginval1), inv(indexblock(indx, lax, m3)), m0 ∈ istore1, rp ∈ zh, istore1[m0].ref-size ≥ m2, istore2 ⊑ istore3[n0, indexblock([], [], 0)], istore2 ⊑ istore3, istore3[n0, indexblock([], [], 0)] ⊑ istore1, istore2 ⊑ istore1, ⌊err⌋ , pstate1.index? → pstate1.lnum ∈ istore1, pstate1.journal? → nx ≠ [] ∧ pstate1.lnum = nx.last ∧ pstate1.lnum ∈ gstore4 ⊦ [istore[maxino0].ref-size := n] (inv(istore) ∧ istore2 ⊑ istore → (∃ ri0, fi0. btree-inv(rp, adr, istore, istore2, zh0[rp, mkznode(r0, zbrar0, boolvar0, true, m4)], ri0, fi0))), pstate1 = readonly, pstate1 = unbuffered, dups(nx), n0 ∈ istore3 |
syn ↔ true, zh0[rp] = mkznode(r0, zbrar0, boolvar0, false, m4), zh[rp] = mkznode(r, zbrar, boolvar, true, m), istore1[m0] = indexblock(indx, lax, m3), ginval0 = ginval1, gstore = gstore3, gstore0 = gstore4, istore = istore1, istore0 = istore2, maxino = maxino2, maxino0 = m0, n = istore1[m0].ref-size - m2, pstate = readonly, remove-refsize0(gstore3) = gstore3, remove-refsize0(istore2) = istore2, dom remove-refsize0(gstore4) ∩ ginval1 = ∅, elems nx ∩ ginval1 = ∅, dom gstore3 ∪ elems nx = dom gstore4 ∪ ginval1, btree-inv(rp, adr, istore1[m0, indexblock(indx, lax, m3 - m2)], istore2, zh0[rp, mkznode(r0, zbrar0, boolvar0, true, m4)], ri, fi), btree-inv(rp, @(m0, m1, m2), istore1, istore1, zh0, ri, ri), btree-inv(rp, adr, istore3, istore2, zh, ri, fi), btree-inv(rp, adr, istore3[n0, indexblock([], [], 0)], istore2, zh, ri, fi), inv(istore[maxino0, istore[maxino0].ref-size:= n]), inv(indexblock(indx, lax, m3)), inv(gstore4 \ ginval1), inv(gstore3), inv(istore2), inv(istore1), inv(istore3), inv(istore3[n0, indexblock([], [], 0)]), maxino0 ∈ istore, rp ∈ zh, m0 ∈ istore1, istore1[m0].ref-size ≥ m2, istore2 ⊑ istore[maxino0, istore[maxino0].ref-size:= n], istore2 ⊑ istore1, istore3[n0, indexblock([], [], 0)] ⊑ istore1, istore2 ⊑ istore3, istore2 ⊑ istore3[n0, indexblock([], [], 0)], ⌊err⌋ , pstate1.journal? → nx ≠ [] ∧ pstate1.lnum = nx.last ∧ pstate1.lnum ∈ gstore4, pstate1.index? → pstate1.lnum ∈ istore1 ⊦ pstate1 = unbuffered, pstate1 = readonly, dups(nx), n0 ∈ istore3, ∃ ri0, fi0. btree-inv(rp, adr, istore[maxino0, istore[maxino0].ref-size:= n], istore2, zh0[rp, mkznode(r0, zbrar0, boolvar0, true, m4)], ri0, fi0)