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

Heuristic symbolic execution applied rule choose left

And obtained the following new goals

• Proof step 39:

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