| err2 = err1, remove-refsize0(istore1) = istore1, remove-refsize0(gstore1) = gstore1, elems nx1 ∩ ginval3 = ∅, dom gstore1 ∪ elems nx1 = dom gstore4 ∪ ginval3, btree-inv(rp1, adr2, istore2, istore1, zh, ri, fi3), btree-inv(rp1, adr2, istore2, istore1, zh, fi7, fi6), inv(istore1), inv(istore2), inv(gstore1), inv(gstore4 \ ginval3), ri-inj(fi6), ri-inj(fi7), istore1 ⊑ istore2, ⌊err1⌋ , pstate1.index? → pstate1.lnum ∈ istore2, pstate1.journal? → nx1 ≠ [] ∧ pstate1.lnum = nx1.last ∧ pstate1.lnum ∈ gstore4 ⊦ ⟨ginval0 := ?, syn := ?, gstore0 := ?, gstore := ?, nx := ?, maxino := ?, ginval := ?, maxino0 := ?, nx0 := ?, ginval1 := ?, fi0 := ?, fi := ?⟩ ( fi4 = fi0 ∧ fi5 = fi ∧ ginval2 = ginval0 ∧ gstore2 = gstore0 ∧ gstore3 = gstore ∧ nx2 = nx ∧ maxino1 = maxino ∧ ginval4 = ginval ∧ (syn0 ↔ syn) ∧ maxino2 = maxino0 ∧ nx5 = nx0 ∧ ginval5 = ginval1 ∧ err1 = err2), dups(nx1) |