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