Proof step 7 from proof inv-store (previous step)

Heuristic symbolic execution applied rule let right

And obtained the following new goals

• Proof step 8:

  gstore[adr1] = mkgnode(nd, m, boolvar, boolvar0), adr0 = adr1, fi1 = fi, gstore1 = gstore, jro = jro0, remove-refsize0(gstore0) = gstore0, elems nx ∩ jro0 = ∅, dom gstore0 ∪ elems nx = dom gstore ∪ jro0, fi0.inos < pmaxino, fi.inos < jmaxino, p_os < pmaxino, jro1 < jmaxino, inv(gstore0), inv(gstore \ jro0), key-cons(key, nd), refsize-cons(gstore0, range fi0), refsize-cons(gstore, range fi), ri-inj(fi0), ri-inj(fi), adr1 ∈ gstore, pmaxino ≤ jmaxino, fi0.lebs ⊆ dom gstore0, fi.lebs ⊆ dom gstore, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0) ⊦ ⟪index_index_store#(key, adr0, fi0, jro, gstore, gstore0, nx, pmaxino, p_os, jvalid0; adr, jvalid, fi); let n = ? in {if jvalid then {index_get_gblock_refsize#(adr.lnum, fi, fi0, jro, gstore, gstore0, nx, pmaxino, p_os, jvalid0; ; n); index_set_gblock_refsize#(adr.lnum, n - adr.size, fi, fi0, jro, gstore0, nx, pmaxino, p_os, jvalid0; gstore)}; index_get_gblock_refsize#(adr0.lnum, fi, fi0, jro, gstore, gstore0, nx, pmaxino, p_os, jvalid0; ; n); index_set_gblock_refsize#(adr0.lnum, n + adr0.size, fi, fi0, jro, gstore0, nx, pmaxino, p_os, jvalid0; gstore)}; jmaxino := max(key.ino + 1, jmaxino)⟫ ( jro1 < jmaxino ∧ pmaxino ≤ jmaxino ∧ fi1.inos ∪ (key.inode? ⊃ ∅ ++ key.ino;∅) < jmaxino ∧ jmaxino ≠ 0 ∧ (jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0)) ∧ fi1[key, adr1].lebs ⊆ dom gstore ∧ refsize-cons(gstore, range fi1[key, adr1]) ∧ inv(gstore \ jro0) ∧ dom gstore0 ∪ elems nx = dom gstore ∪ jro0 ∧ ri-inj(fi1[key, adr1]) ∧ gstore =○refsize gstore1 ∧ fi = fi1[key, adr1]), jmaxino = 0, pmaxino = 0, dups(nx), adr1 ∈ fi

Rule argument

Additional information