| syn1 ↔ true, istore2[m0] = indexblock(indx, lax, m3), zh[rp] = mkznode(r, zbrar, boolvar, true, m), zh0[rp] = mkznode(r0, zbrar0, boolvar0, false, m4), adr0 = @(m0, m1, m2), err1 = err, err1 = ESUCCESS, ginval = ginval0, ginval4 = ∅, gstore = gstore3, gstore0 = gstore4, gstore1 = remove-refsize0(gstore0), gstore2 = remove-refsize0(gstore0), istore = istore4, istore0 = remove-refsize0(istore2), istore1 = istore0, maxino2 = maxino0, nx = [], pstate1 = unbuffered, remove-refsize0(remove-refsize0(gstore0)) = remove-refsize0(gstore0), remove-refsize0(istore0) = istore0, remove-refsize0(istore4) = istore4, remove-refsize0(gstore3) = gstore3, elems nx ∩ ∅ = ∅, elems nx0 ∩ ginval0 = ∅, dom remove-refsize0(gstore4) ∩ ginval0 = ∅, dom remove-refsize0(gstore0) ∪ elems nx = dom remove-refsize0(gstore0) ∪ ∅, dom gstore3 ∪ elems nx0 = dom gstore4 ∪ ginval0, btree-inv(rp, adr, istore3[n, indexblock([], [], 0)], istore4, zh, ri, fi), btree-inv(rp, adr, istore3, istore4, zh, ri, fi), btree-inv(rp, @(m0, m1, m2), istore2, istore2, zh0, ri, ri), btree-inv(rp, adr, istore2[m0, indexblock(indx, lax, m3 - m2)], istore4, zh0[rp, mkznode(r0, zbrar0, boolvar0, true, m4)], ri, fi), inv(remove-refsize0(gstore0) \ ∅), inv(remove-refsize0(gstore0)), inv(istore0), inv(istore3[n, indexblock([], [], 0)]), inv(istore4), inv(istore3), inv(gstore3), inv(gstore4 \ ginval0), inv(istore2), rp ∈ zh, istore0 ⊑ istore0, istore4 ⊑ istore2, istore4 ⊑ istore3[n, indexblock([], [], 0)], istore4 ⊑ istore3, istore3[n, indexblock([], [], 0)] ⊑ istore2, unbuffered.journal? → nx ≠ [] ∧ unbuffered.lnum = nx.last ∧ unbuffered.lnum ∈ remove-refsize0(gstore0), unbuffered.index? → unbuffered.lnum ∈ istore0, pstate.index? → pstate.lnum ∈ istore2, pstate.journal? → nx0 ≠ [] ∧ pstate.lnum = nx0.last ∧ pstate.lnum ∈ gstore4, ⌊err⌋ ∨ err = ESUCCESS ⊦ ⟪adr := @(m0, m1, m2)⟫ ( (∃ ri, fi. btree-inv(rp, adr0, istore0, istore1, zh0, ri, fi)) ∧ inv(istore0) ∧ istore1 ⊑ istore0 ∧ (pstate1.journal? → nx ≠ [] ∧ pstate1.lnum = nx.last ∧ pstate1.lnum ∈ gstore2) ∧ (pstate1.index? → pstate1.lnum ∈ istore0) ∧ (pstate1 = unbuffered → syn1)), pstate = unbuffered, pstate = readonly, dups(nx0), dups(nx), n ∈ istore3 |
syn1 ↔ true, zh0[rp] = mkznode(r0, zbrar0, boolvar0, false, m4), zh[rp] = mkznode(r, zbrar, boolvar, true, m), istore2[m0] = indexblock(indx, lax, m3), adr0 = @(m0, m1, m2), err1 = ESUCCESS, err1 = err, ginval = ginval0, ginval4 = ∅, gstore = gstore3, gstore0 = gstore4, gstore1 = remove-refsize0(gstore0), gstore2 = remove-refsize0(gstore0), istore = istore4, istore0 = remove-refsize0(istore2), istore1 = istore0, maxino2 = maxino0, nx = [], pstate1 = unbuffered, remove-refsize0(gstore3) = gstore3, remove-refsize0(istore4) = istore4, remove-refsize0(istore0) = istore0, remove-refsize0(remove-refsize0(gstore0)) = remove-refsize0(gstore0), dom remove-refsize0(gstore4) ∩ ginval0 = ∅, elems nx0 ∩ ginval0 = ∅, elems nx ∩ ∅ = ∅, dom gstore3 ∪ elems nx0 = dom gstore4 ∪ ginval0, dom remove-refsize0(gstore0) ∪ elems nx = dom remove-refsize0(gstore0) ∪ ∅, btree-inv(rp, adr, istore2[m0, indexblock(indx, lax, m3 - m2)], istore4, zh0[rp, mkznode(r0, zbrar0, boolvar0, true, m4)], ri, fi), btree-inv(rp, @(m0, m1, m2), istore2, istore2, zh0, ri, ri), btree-inv(rp, adr, istore3, istore4, zh, ri, fi), btree-inv(rp, adr, istore3[n, indexblock([], [], 0)], istore4, zh, ri, fi), inv(istore2), inv(gstore4 \ ginval0), inv(gstore3), inv(istore3), inv(istore4), inv(istore3[n, indexblock([], [], 0)]), inv(istore0), inv(remove-refsize0(gstore0)), inv(remove-refsize0(gstore0) \ ∅), rp ∈ zh, istore3[n, indexblock([], [], 0)] ⊑ istore2, istore4 ⊑ istore3, istore4 ⊑ istore3[n, indexblock([], [], 0)], istore4 ⊑ istore2, istore0 ⊑ istore0, pstate.journal? → nx0 ≠ [] ∧ pstate.lnum = nx0.last ∧ pstate.lnum ∈ gstore4, pstate.index? → pstate.lnum ∈ istore2, unbuffered.index? → unbuffered.lnum ∈ istore0, unbuffered.journal? → nx ≠ [] ∧ unbuffered.lnum = nx.last ∧ unbuffered.lnum ∈ remove-refsize0(gstore0), ⌊err⌋ ∨ err = ESUCCESS ⊦ pstate = readonly, pstate = unbuffered, dups(nx), dups(nx0), n ∈ istore3, (∃ ri, fi. btree-inv(rp, adr0, istore0, istore1, zh0, ri, fi)) ∧ inv(istore0) ∧ istore1 ⊑ istore0 ∧ (pstate1.journal? → nx ≠ [] ∧ pstate1.lnum = nx.last ∧ pstate1.lnum ∈ gstore2) ∧ (pstate1.index? → pstate1.lnum ∈ istore0) ∧ (pstate1 = unbuffered → syn1)