| jro = jro0, gstore = crash(gstore0, gstore1, jro0, nx), gstore2 = gstore1, nx0 = nx, pmaxino = jmaxino, p_os = jro1, fi = fi0, jvalid, jro2 < jmaxino0, jro1 < jmaxino, jmaxino ≤ jmaxino0, fi1.inos < jmaxino0, fi0.inos < jmaxino, jmaxino0 ≠ 0, jmaxino ≠ 0, jvalid0 ∧ nx ≠ [] → valid-journal-head(nx, gstore0, jro0), fi1.lebs ⊆ dom gstore0, fi0.lebs ⊆ dom gstore1, refsize-cons(gstore0, range fi1), refsize-cons(gstore1, range fi0), inv-journal(nx, gstore0, gstore1, jro0), ri-inj(fi1), ri-inj(fi0) ⊦ ⟪gjournal_recover# (jvalid1; log, ks, jmaxino1, jro3, fi2, fi, jro, gstore, gstore2, nx0, pmaxino, p_os, jvalid2; jvalid3, jmaxino2, jvalid4, err)⟫ ( err = ESUCCESS → jvalid2 ∧ jro3 < jmaxino1 ∧ p_os < pmaxino ∧ pmaxino ≤ jmaxino1 ∧ fi2.inos < jmaxino1 ∧ fi.inos < pmaxino ∧ jmaxino1 ≠ 0 ∧ pmaxino ≠ 0 ∧ (jvalid3 ∧ nx0 ≠ [] → valid-journal-head(nx0, gstore, jro)) ∧ fi2.lebs ⊆ dom gstore ∧ fi.lebs ⊆ dom gstore2 ∧ refsize-cons(gstore, range fi2) ∧ refsize-cons(gstore2, range fi) ∧ inv-journal(nx0, gstore, gstore2, jro) ∧ ri-inj(fi2) ∧ ri-inj(fi)) |