| p_os0.keys = jro1.keys, [] = abs-log(nx0, gstore0 ↓), nodes(gstore2 ↓, jro2) \ as0 = nodes(gstore0 ↓, jro), remove-refsize0(gstore1) = gstore1, as0 ∩ range fi0 = ∅, dom remove-refsize0(gstore2) ∩ jro2 = ∅, elems nx ∩ jro2 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ jro2, p_os.keys.inodes?, jro1.keys.inodes?, fi1.inos < pmaxino, jro1 < jmaxino, p_os < pmaxino, fi0.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 fi0), ri-cons(fi0, nodes(gstore2 ↓, jro2)), ri-inj(fi1), ri-inj(fi0), pmaxino ≤ jmaxino, fi1.lebs ⊆ dom gstore1, fi0.lebs ⊆ dom gstore2, jvalid2 → jvalid0, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro2) ⊦ ⟨jvalid := true⟩ (jro1.keys = jro1.keys ∧ fi0 = fi0 ∧ [] = [] ∧ nodes(gstore0 ↓, jro) = nodes(gstore0 ↓, jro) ∧ ESUCCESS = ESUCCESS), ∃ err0. ⌊err0⌋ ∧ ⟨err := err0; jvalid := ?⟩ (jro1.keys = p_os.keys ∧ fi0 = fi1 ∧ abs-log(nx, gstore2 ↓) = [] ∧ nodes(gstore2 ↓, jro2) = nodes(gstore0 ↓, jro) ∧ ESUCCESS = err), jmaxino = 0, pmaxino = 0, dups(nx), jro1.keys = p_os.keys ∧ fi0 = fi1 ∧ abs-log(nx, gstore2 ↓) = [] ∧ nodes(gstore2 ↓, jro2) = nodes(gstore0 ↓, jro) |