| remove-refsize0(gstore3) = gstore3, elems nx1 ∩ jro4 = ∅, dom gstore3 ∪ elems nx1 = dom gstore2 ∪ jro4, jmaxino0 ≠ 0, jmaxino3 ≠ 0, jro1.keys.inodes?, jro5.keys.inodes?, fi3.inos < jmaxino0, ri0.inos < jmaxino3, jro1 < jmaxino0, jro5 < jmaxino3, inv(crash(gstore2, gstore3, jro4, nx1) \ jro4), inv(gstore3), inv(gstore2 \ jro4), log-cons(abs-log(nx1, gstore2 ↓), nodes(gstore2 ↓, jro4)), refsize-cons(gstore3, range fi3), refsize-cons(gstore2, range ri0), ri-inj(fi3), ri-inj(ri0), jmaxino0 ≤ jmaxino3, fi3.lebs ⊆ dom gstore3, ri0.lebs ⊆ dom gstore2, ⌊err1⌋ , ¬ dups(nx1), jvalid8 ∧ nx1 ≠ [] → valid-journal-head(nx1, gstore2, jro4) ⊦ ⟨err := err1; 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 ∧ jro1.keys = ks ∧ err1 = err) |
err = err1, remove-refsize0(gstore3) = gstore3, elems nx1 ∩ jro4 = ∅, dom gstore3 ∪ elems nx1 = dom gstore2 ∪ jro4, jro5.keys.inodes?, jro1.keys.inodes?, jro5 < jmaxino3, jro1 < jmaxino0, ri0.inos < jmaxino3, fi3.inos < jmaxino0, inv(gstore2 \ jro4), inv(gstore3), inv(crash(gstore2, gstore3, jro4, nx1) \ jro4), log-cons(abs-log(nx1, gstore2 ↓), nodes(gstore2 ↓, jro4)), refsize-cons(gstore2, range ri0), refsize-cons(gstore3, range fi3), ri-inj(ri0), ri-inj(fi3), jmaxino0 ≤ jmaxino3, ri0.lebs ⊆ dom gstore2, fi3.lebs ⊆ dom gstore3, ⌊err1⌋ , jvalid8 ∧ nx1 ≠ [] → valid-journal-head(nx1, gstore2, jro4) ⊦ ⟨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 ∧ jro1.keys = ks ∧ err1 = err), jmaxino0 = 0, jmaxino3 = 0, dups(nx1)