| ginval1 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), nx0 = nx, remove-refsize0(istore1) = istore1, remove-refsize0(gstore0) = gstore0, elems nx ∩ ginval = ∅, dom gstore0 ∪ elems nx = dom gstore ∪ ginval, inv(istore1), inv(istore2), inv(gstore0), inv(gstore \ ginval), istore1 ⊑ istore2, pstate.index? → pstate.lnum ∈ istore2, pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore ⊦ ⟨skip⟩ (ginval1 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ nx0 = nx), pstate = readonly, dups(nx) |