| ri-cons(ri, fs), node-cons(nd.key, nd), node-cons(nd0.key, nd0), node-cons(nd1.key, nd1), node-cons(nd2.key, nd2), jro.keys = ro, p_os.keys = fo, fi = ri, fi0 = fi1, log = abs-log(nx, gstore ↓), fs = nodes(gstore ↓, jro0), jvalid → jvalid0, ri-inj(ri), ri-inj(fi1), log-cons(log, fs), ro.inodes?, fo.inodes?, jro < jmaxino, p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, jmaxino ≠ 0, pmaxino ≠ 0, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro0), ri-inj(fi), ri-inj(fi0), adr = adr0, adr1 = adr2, adr3 = adr4, adr5 = adr6 ⊦ ⟪gjournal_journal_add4# (nd, nd0, nd1, nd2, jvalid2, fi, fi0, gstore0, pmaxino, p_os; adr, adr1, adr3, adr5, jvalid1, jmaxino0, jro0, gstore, nx, jvalid0; err)⟫ ⟨aubifs_core_journal_add4#(nd, nd0, nd1, nd2, ri, fi1, ro, fo; adr0, adr2, adr4, adr6, fs, log; jvalid, err0)⟩ ( (jro.keys = ro ∧ p_os.keys = fo ∧ fi = ri ∧ fi0 = fi1 ∧ log = abs-log(nx, gstore ↓) ∧ fs = nodes(gstore ↓, jro0) ∧ (jvalid → jvalid0)) ∧ adr = adr0 ∧ adr1 = adr2 ∧ adr3 = adr4 ∧ adr5 = adr6 ∧ err = err0) |