| ginval1 = ginval, gstore1 = crash(gstore, gstore0, ginval, 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), n ∈ gstore0, n ∈ gstore, 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)), dups(nx), n ∈ nx |