| remove-refsize0(gstore5) = gstore5, elems nx1 ∩ jro4 = ∅, dom gstore5 ∪ elems nx1 = dom gstore2 ∪ jro4, jmaxino ≠ 0, jmaxino3 ≠ 0, jro1.keys.inodes?, jro6.keys.inodes?, fi3.inos < jmaxino, ri0.inos < jmaxino3, jro1 < jmaxino, jro6 < jmaxino3, inv(gstore5), inv(gstore2 \ jro4), log-cons(abs-log(nx1, gstore2 ↓), nodes(gstore2 ↓, jro4)), refsize-cons(gstore5, range fi3), refsize-cons(gstore2, range ri0), ri-inj(fi3), ri-inj(ri0), jmaxino ≤ jmaxino3, fi3.lebs ⊆ dom gstore5, ri0.lebs ⊆ dom gstore2, ⌊err0⌋ , ¬ dups(nx1), jvalid8 ∧ nx1 ≠ [] → valid-journal-head(nx1, gstore2, jro4) ⊦ ⟨ax0 := ax; ks1 := ks0; aubifs_core_recover#(jvalid2; ax0, ks0, fi5, ro1, fo1, ax, fs1; ri1, jvalid7, err1)⟩ (ri = ri1 ∧ fi = fi5 ∧ ro = ro1 ∧ fo = fo1 ∧ fs = fs1 ∧ log = ax0 ∧ (jvalid ↔ jvalid7) ∧ ax = ax0 ∧ ks1 = ks0 ∧ err0 = err1) |
ax0 = ax, remove-refsize0(gstore5) = gstore5, elems nx1 ∩ jro4 = ∅, dom gstore5 ∪ elems nx1 = dom gstore2 ∪ jro4, jro6.keys.inodes?, jro1.keys.inodes?, jro6 < jmaxino3, jro1 < jmaxino, ri0.inos < jmaxino3, fi3.inos < jmaxino, inv(gstore2 \ jro4), inv(gstore5), log-cons(abs-log(nx1, gstore2 ↓), nodes(gstore2 ↓, jro4)), refsize-cons(gstore2, range ri0), refsize-cons(gstore5, range fi3), ri-inj(ri0), ri-inj(fi3), jmaxino ≤ jmaxino3, ri0.lebs ⊆ dom gstore2, fi3.lebs ⊆ dom gstore5, ⌊err0⌋ , jvalid8 ∧ nx1 ≠ [] → valid-journal-head(nx1, gstore2, jro4) ⊦ ⟨ks1 := ks0; aubifs_core_recover#(jvalid2; ax0, ks0, fi5, ro1, fo1, ax, fs1; ri1, jvalid7, err1)⟩ (ri = ri1 ∧ fi = fi5 ∧ ro = ro1 ∧ fo = fo1 ∧ fs = fs1 ∧ log = ax0 ∧ (jvalid ↔ jvalid7) ∧ ax = ax0 ∧ ks1 = ks0 ∧ err0 = err1), jmaxino = 0, jmaxino3 = 0, dups(nx1)