| p_os.keys = p_os0.keys, abs-log(nx0, gstore0 ↓) = abs-log(nx, gstore2 ↓), nodes(gstore0 ↓, jro) = nodes(gstore2 ↓, jro2), remove-refsize0(gstore1) = gstore1, dom remove-refsize0(gstore2) ∩ jro2 = ∅, elems nx ∩ jro2 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ jro2, p_os0.keys.inodes?, jro1.keys.inodes?, fi1.inos < pmaxino, jro1 < jmaxino, p_os < pmaxino, ri.inos < jmaxino, inv(gstore2 \ jro2), inv(gstore1), log-cons(abs-log(nx, gstore2 ↓), nodes(gstore2 ↓, jro2)), refsize-cons(gstore1, range fi1), refsize-cons(gstore2, range ri), ri-cons(ri, nodes(gstore2 ↓, jro2)), ri-inj(fi1), ri-inj(ri), pmaxino ≤ jmaxino, fi1.lebs ⊆ dom gstore1, ri.lebs ⊆ dom gstore2, ⌊err1⌋ , jvalid2 → jvalid0, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro2), jvalid4 → jvalid3 ⊦ ⟨jvalid5 := ?⟩ ((jvalid5 → jvalid3) ∧ err1 = err1), ∃ as. as ∩ range ri = ∅ ∧ ⟨fi := ri, fo := jro1.keys, fs := nodes(gstore2 ↓, jro2) \ as, log := [], err := ESUCCESS; jvalid5 := true⟩ (p_os0.keys = fo ∧ fi1 = fi ∧ log = abs-log(nx, gstore2 ↓) ∧ fs = nodes(gstore2 ↓, jro2) ∧ (jvalid5 → jvalid3) ∧ err1 = err), jmaxino = 0, pmaxino = 0, dups(nx) |