| jvalid ↔ jvalid3, fi = fi1, fo = p_os.keys, fs = nodes(gstore4 ↓, jro0), ks = datakeys(key, n, ri), log = abs-log(nx, gstore4 ↓), remove-refsize0(gstore3) = gstore3, ri0 = ri, ro = jro1.keys, elems nx ∩ jro0 = ∅, dom gstore3 ∪ elems nx = dom gstore ∪ jro0, dom gstore4 ∪ jro0 = dom gstore ∪ jro0, jro1.keys.inodes?, p_os.keys.inodes?, fi1.inos < pmaxino, p_os < pmaxino, jro1 < jmaxino, ri.inos < jmaxino, gstore =○refsize gstore4, inv(gstore4 \ jro0), inv(gstore3), inv(gstore \ jro0), log-cons(abs-log(nx, gstore4 ↓), nodes(gstore4 ↓, jro0)), refsize-cons(gstore3, range fi1), refsize-cons(gstore4, range ri), refsize-cons(gstore, range(ri \ datakeys(key, n, ri))), ri-inj(fi1), ri-inj(ri), ri-inj(ri \ datakeys(key, n, ri)), pmaxino ≤ jmaxino, fi1.lebs ⊆ dom gstore3, ri.lebs ⊆ dom gstore4, (ri \ datakeys(key, n, ri)).lebs ⊆ dom gstore, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore4, jro0), jvalid3 → jvalid2, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0) ⊦ ⟨ri := ri \ ks⟩ (ri0 \ datakeys(key, n, ri0) = ri ∧ (jvalid3 → jvalid2)), jmaxino = 0, pmaxino = 0, dups(nx) |