Proof step 31 from proof refine-check-commit (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  ⟨aubifs_core_commit#(ri, jro1.keys; fs, fi1, fo, log; jvalid2, err0)⟩ (fs = nodes(gstore0 ↓, jro) ∧ fi1 = fi0 ∧ fo = p_os0.keys ∧ log = abs-log(nx0, gstore0 ↓) ∧ (jvalid2 ↔ jvalid4) ∧ err0 = err1), p_os.keys = fo, fs = nodes(gstore2 ↓, jro2), log = abs-log(nx, gstore2 ↓), remove-refsize0(gstore1) = gstore1, ro = jro1.keys, dom remove-refsize0(gstore2) ∩ jro2 = ∅, elems nx ∩ jro2 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ jro2, jmaxino ≠ 0, pmaxino ≠ 0, p_os.keys.inodes?, jro1.keys.inodes?, fi1.inos < pmaxino, jro1 < jmaxino, p_os < pmaxino, ri.inos < jmaxino, inv(gstore2 \ jro2), inv(gstore1), log-cons(abs-log(nx, gstore2 ↓), nodes(gstore2 ↓, jro2)), refsize-cons(gstore1, range fi1), refsize-cons(gstore2, range ri), ri-cons(ri, nodes(gstore2 ↓, jro2)), ri-inj(fi1), ri-inj(ri), pmaxino ≤ jmaxino, fi1.lebs ⊆ dom gstore1, ri.lebs ⊆ dom gstore2, ¬ dups(nx), jvalid2 → jvalid0, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro2), jvalid4 → jvalid3 ⊦ ⟨fail#(; ; err); jvalid := ?⟩ ( p_os0.keys = p_os.keys ∧ fi0 = fi1 ∧ abs-log(nx, gstore2 ↓) = abs-log(nx0, gstore0 ↓) ∧ nodes(gstore2 ↓, jro2) = nodes(gstore0 ↓, jro) ∧ (jvalid → jvalid3) ∧ err1 = err), ⟨choose as with as ∩ range ri = ∅ in fi1 := ri, fo := ro, fs := fs \ as, log := [], err := ESUCCESS; jvalid := true⟩ (p_os0.keys = fo ∧ fi0 = fi1 ∧ log = abs-log(nx0, gstore0 ↓) ∧ fs = nodes(gstore0 ↓, jro) ∧ (jvalid → jvalid3) ∧ err1 = err), p_os0.keys = p_os.keys ∧ fi0 = fi1 ∧ abs-log(nx, gstore2 ↓) = abs-log(nx0, gstore0 ↓) ∧ nodes(gstore2 ↓, jro2) = nodes(gstore0 ↓, jro) ∧ (jvalid2 → jvalid3) ∧ err1 = ESUCCESS

Rule argument

Additional information