| syn ↔ true, adr = adr0, ginval = ginval2, ginval0 = ginval1, gstore = gstore1, gstore0 = gstore2, istore = istore1, istore0 = istore2, maxino = maxino0, n0 = n1, remove-refsize0(istore1) = istore1, remove-refsize0(gstore1) = gstore1, elems nx ∩ ginval1 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ ginval1, inv(istore1), inv(istore2), inv(gstore1), inv(gstore2 \ ginval1), istore1 ⊑ istore2, pstate.index? → pstate.lnum ∈ istore2, pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore2 ⊦ (∀ n. ¬(n ∈ dom gstore0 ∧ ¬ n ∈ nx)) ∧ ⟨err := ENOSPC⟩ true, ∃ n. (n ∈ dom gstore0 ∧ ¬ n ∈ nx) ∧ ⟨n0 := n; err := ESUCCESS⟩ true, ⟨err := ENOSPC⟩ true, dups(nx) |