| err = ESUCCESS, fi = fi3, fo = jro1.keys, fs = nodes(gstore2 ↓, jro4), log = abs-log(nx1, gstore2 ↓), remove-refsize0(gstore3) = gstore3, elems nx1 ∩ jro4 = ∅, dom gstore3 ∪ elems nx1 = dom gstore2 ∪ jro4, jro5.keys.inodes?, jro1.keys.inodes?, jro5 < jmaxino3, jro1 < jmaxino0, ri0.inos < jmaxino3, fi3.inos < jmaxino0, inv(gstore2 \ jro4), inv(gstore3), inv(crash(gstore2, gstore3, jro4, nx1) \ jro4), log-cons(abs-log(nx1, gstore2 ↓), nodes(gstore2 ↓, jro4)), refsize-cons(gstore2, range ri0), refsize-cons(gstore3, range fi3), ri-inj(ri0), ri-inj(fi3), jmaxino0 ≤ jmaxino3, ri0.lebs ⊆ dom gstore2, fi3.lebs ⊆ dom gstore3, jvalid8 ∧ nx1 ≠ [] → valid-journal-head(nx1, gstore2, jro4) ⊦ ⟨jvalid := true⟩ ( jro1.keys = fo ∧ jro1.keys = fo ∧ fi = fi ∧ fi3 = fi ∧ log = abs-log(nx1, gstore2 ↓) ∧ fs = nodes(gstore2 ↓, jro4) ∧ abs-log(nx1, gstore2 ↓) = log ∧ jro1.keys = fo ∧ ESUCCESS = err), jmaxino0 = 0, jmaxino3 = 0, dups(nx1) |