| remove-refsize0(gstore1) = gstore1, remove-refsize0(istore1) = istore1, elems nx ∩ ginval1 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ ginval1, inv(gstore2 \ ginval1), inv(gstore1), inv(istore2), inv(istore1), istore1 ⊑ istore2, pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore2, pstate.index? → pstate.lnum ∈ istore2 ⊦ ⟨pstate := readonly⟩ (ESUCCESS = ESUCCESS), ⟨skip⟩ (ESUCCESS = ESUCCESS), ⟨err := EIO; syn := err = ESUCCESS; skip or pstate := readonly⟩ syn, pstate = readonly, pstate = unbuffered, dups(nx) |