| jvalid ↔ jvalid0, fi = fi1, fi0 = ri, gstore = gstore1, gstore0 = gstore2, jro = jro0, remove-refsize0(gstore1) = gstore1, elems nx ∩ jro0 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ jro0, p_os.keys.inodes?, jro1.keys.inodes?, fi1.inos < pmaxino, ri.inos < jmaxino, p_os < pmaxino, jro1 < jmaxino, inv(gstore1), inv(gstore2 \ jro0), log-cons(abs-log(nx, gstore2 ↓), nodes(gstore2 ↓, jro0)), refsize-cons(gstore1, range fi1), refsize-cons(gstore2, range ri), ri-inj(fi1), ri-inj(ri), pmaxino ≤ jmaxino, fi1.lebs ⊆ dom gstore1, ri.lebs ⊆ dom gstore2, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro0), jvalid2 → jvalid0 ⊦ ⟪index_sync#(fi0, fi, jro, gstore0, gstore, nx, pmaxino, p_os; ; jvalid, err)⟫ ⟨aubifs_core_journal_sync#(ri, fi1, jro1.keys, p_os.keys, nodes(gstore2 ↓, jro0), abs-log(nx, gstore2 ↓); ; jvalid2, err0)⟩ ((jvalid2 → jvalid) ∧ err = err0), jmaxino = 0, pmaxino = 0, dups(nx) |
remove-refsize0(gstore1) = gstore1, elems nx ∩ jro0 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ jro0, jmaxino ≠ 0, pmaxino ≠ 0, jro1.keys.inodes?, p_os.keys.inodes?, jro1 < jmaxino, p_os < pmaxino, ri.inos < jmaxino, fi1.inos < pmaxino, inv(gstore2 \ jro0), inv(gstore1), log-cons(abs-log(nx, gstore2 ↓), nodes(gstore2 ↓, jro0)), refsize-cons(gstore2, range ri), refsize-cons(gstore1, range fi1), ri-inj(ri), ri-inj(fi1), pmaxino ≤ jmaxino, ri.lebs ⊆ dom gstore2, fi1.lebs ⊆ dom gstore1, ¬ dups(nx), jvalid2 → jvalid0, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro0) ⊦ ⟪index_sync#(ri, fi1, jro0, gstore2, gstore1, nx, pmaxino, p_os; ; jvalid0, err)⟫ ⟨aubifs_core_journal_sync#(ri, fi1, jro1.keys, p_os.keys, nodes(gstore2 ↓, jro0), abs-log(nx, gstore2 ↓); ; jvalid2, err0)⟩ ((jvalid2 → jvalid0) ∧ err = err0)