| jvalid0 ↔ jvalid2, ax = ax0, ax0 = ax1, fi = fi5, fo = fo1, fs = fs1, ks = ks0, ks1 = ks0, log = ax1, remove-refsize0(gstore5) = gstore5, ro = ro1, 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, ⌊err1⌋ , jvalid8 ∧ nx1 ≠ [] → valid-journal-head(nx1, gstore2, jro4) ⊦ ∃ err0. (⌊err0⌋ ∨ err0 = ESUCCESS) ∧ ⟨err := err0; if err = ESUCCESS then {ri := fi, ro := fo, ax := log; ks := ro; jvalid := true} else ri := ?, fi := ?, fs := ?, log := ?, ro := ?, fo := ?, ax := ?, ks := ?, jvalid := ?⟩ (ri2 = ri ∧ fi0 = fi ∧ ro0 = ro ∧ fo0 = fo ∧ fs0 = fs ∧ log0 = ax ∧ (jvalid1 ↔ jvalid) ∧ log = ax ∧ ks1 = ks ∧ err1 = err), jmaxino = 0, jmaxino3 = 0, dups(nx1) |
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, ⌊err1⌋ , ¬ dups(nx1), jvalid8 ∧ nx1 ≠ [] → valid-journal-head(nx1, gstore2, jro4) ⊦ ∃ err0. (⌊err0⌋ ∨ err0 = ESUCCESS) ∧ ⟨err := err0; if err = ESUCCESS then {ri := fi, ro := fo, ax := ax1; ks := ro; jvalid := true} else ri := ?, fi := ?, fs := ?, ax1 := ?, ro := ?, fo := ?, ax := ?, ks := ?, jvalid := ?⟩ (ri2 = ri ∧ fi0 = fi ∧ ro0 = ro ∧ fo0 = fo ∧ fs0 = fs ∧ log0 = ax ∧ (jvalid1 ↔ jvalid) ∧ ax1 = ax ∧ ks0 = ks ∧ err1 = err)