| jvalid0 ↔ jvalid1, jvalid ↔ jvalid2, fi = ri, fi0 = fi1, fs = nodes(gstore ↓, jro0), gstore3 = gstore, jro = jro0, remove-refsize0(gstore0) = gstore0, elems nx ∩ jro0 = ∅, dom gstore0 ∪ elems nx = dom gstore ∪ jro0, p_os.keys.inodes?, jro1.keys.inodes?, ri.inos < jmaxino, jro1 < jmaxino, p_os < pmaxino, fi1.inos < pmaxino, inv(gstore0), inv(gstore \ jro0), log-cons(abs-log(nx, gstore ↓), nodes(gstore ↓, jro0)), refsize-cons(gstore, range ri), refsize-cons(gstore0, range fi1), ri-inj(ri), ri-inj(fi1), pmaxino ≤ jmaxino, ri.lebs ⊆ dom gstore, fi1.lebs ⊆ dom gstore0, jvalid3 → jvalid2, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0) ⊦ [let as = ? in {index_index_truncate#(key, n, fi0, jro, gstore, gstore0, nx, pmaxino, p_os, jvalid; as, fi); gjournal_remove_addresses#(jvalid0, fi, fi0, jro, gstore0, nx, pmaxino, p_os, jvalid; as, gstore)}] ( fi.inos < jmaxino ∧ (jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0)) ∧ fi.lebs ⊆ dom gstore ∧ refsize-cons(gstore, range fi) ∧ inv(gstore \ jro0) ∧ dom gstore0 ∪ elems nx = dom gstore ∪ jro0 ∧ ri-inj(fi) ∧ gstore =○refsize gstore3 → ⟨aubifs_core_index_truncate#(key, n, fi1, jro1.keys, p_os.keys, fs, abs-log(nx, gstore3 ↓), jvalid3; ri)⟩ (fi = ri ∧ fs = nodes(gstore3 ↓, jro0) ∧ (jvalid3 → jvalid2))), jmaxino = 0, pmaxino = 0, dups(nx) |
jvalid ↔ jvalid2, jvalid0 ↔ jvalid1, fi = ri, fi0 = fi1, fs = nodes(gstore ↓, jro0), gstore3 = gstore, jro = jro0, remove-refsize0(gstore0) = gstore0, elems nx ∩ jro0 = ∅, dom gstore0 ∪ elems nx = dom gstore ∪ jro0, jro1.keys.inodes?, p_os.keys.inodes?, fi1.inos < pmaxino, p_os < pmaxino, jro1 < jmaxino, ri.inos < jmaxino, inv(gstore \ jro0), inv(gstore0), log-cons(abs-log(nx, gstore ↓), nodes(gstore ↓, jro0)), refsize-cons(gstore0, range fi1), refsize-cons(gstore, range ri), ri-inj(fi1), ri-inj(ri), pmaxino ≤ jmaxino, fi1.lebs ⊆ dom gstore0, ri.lebs ⊆ dom gstore, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), jvalid3 → jvalid2 ⊦ [index_index_truncate#(key, n, fi0, jro, gstore, gstore0, nx, pmaxino, p_os, jvalid; as, fi); gjournal_remove_addresses#(jvalid0, fi, fi0, jro, gstore0, nx, pmaxino, p_os, jvalid; as, gstore)] ( fi.inos < jmaxino ∧ (jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0)) ∧ fi.lebs ⊆ dom gstore ∧ refsize-cons(gstore, range fi) ∧ inv(gstore \ jro0) ∧ dom gstore0 ∪ elems nx = dom gstore ∪ jro0 ∧ ri-inj(fi) ∧ gstore =○refsize gstore3 → ⟨aubifs_core_index_truncate#(key, n, fi1, jro1.keys, p_os.keys, fs, abs-log(nx, gstore3 ↓), jvalid3; ri)⟩ (fi = ri ∧ fs = nodes(gstore3 ↓, jro0) ∧ (jvalid3 → jvalid2))), jmaxino = 0, pmaxino = 0, dups(nx)