Proof step 5 from proof refine-add-gnds (previous step)

User applied rule insert program lemma

And obtained the following new goals

• Proof step 6:

  ∃ ri, fi, ld. btree-inv(rp, adr, gstore \ ginval, istore, istore0, zh, ri, fi, ld), inv-journal(nx, gstore, gstore0, ginval), maxino ∈ nx ∧ gstore[maxino].size + gndlist.flashsize ≤ LEB_SIZE ∧ ¬ gstore[maxino].failed ⊦ ⟪btree_add_gnds#(maxino, gndlist, nx; ax, gstore; err)⟫ ((∃ ri, fi, ld. btree-inv(rp, adr, gstore \ ginval, istore, istore0, zh, ri, fi, ld)) ∧ inv-journal(nx, gstore, gstore0, ginval) ∧ true)

• Proof step 7:

  gstore = gstore0, ax = ax0, elems nx0 ∩ ginval0 = ∅, dom gstore2 ∪ elems nx0 = dom gstore0 ∪ ginval0, remove-refsize0(gstore2) = gstore2, remove-refsize0(istore0) = istore0, gstore0[maxino] = groupblock(gndlist0, lax, m, m0, m1, false), maxino ∈ nx0, m0 + gndlist.flashsize ≤ LEB_SIZE, btree-inv(rp, adr, gstore0 \ ginval0, istore, istore0, zh, fi, fi0, ld), inv(gstore0 \ ginval0), inv(gstore2), flushed(gstore0 \ (ginval0 ∪ elems nx0)), gstore2 \ ginval0 lpt= gstore0 \ elems nx0, ri-inj(fi), ri-inj(fi0), btree-inv(rp, adr, gstore0 \ ginval0, istore, istore0, zh, ri, fi1, ld0), inv(istore), inv(istore0), flushed(istore0), istore0 ⊑ istore, maxino ∈ gstore0, inv(groupblock(gndlist0, lax, m, m0, m1, false)), ¬ dups(nx0), ¬ maxino ∈ ginval0, (∀ ri, fi, ld. ¬ btree-inv(rp, adr, gstore0 \ ginval0, istore, istore0, zh, ri, fi, ld)) ∨ ¬ inv-journal(nx0, gstore0, gstore2, ginval0) ∨ ¬ maxino ∈ nx0 ∨ ¬ gstore0[maxino].size + gndlist.flashsize ≤ LEB_SIZE ∨ gstore0[maxino].failed ⊦

• Proof step 9:

  gstore = gstore0, ax = ax0, elems nx0 ∩ ginval0 = ∅, dom gstore2 ∪ elems nx0 = dom gstore0 ∪ ginval0, remove-refsize0(gstore2) = gstore2, remove-refsize0(istore0) = istore0, gstore0[maxino] = groupblock(gndlist0, lax, m, m0, m1, false), maxino ∈ nx0, m0 + gndlist.flashsize ≤ LEB_SIZE, btree-inv(rp, adr, gstore0 \ ginval0, istore, istore0, zh, fi, fi0, ld), inv(gstore0 \ ginval0), inv(gstore2), flushed(gstore0 \ (ginval0 ∪ elems nx0)), gstore2 \ ginval0 lpt= gstore0 \ elems nx0, ri-inj(fi), ri-inj(fi0), btree-inv(rp, adr, gstore0 \ ginval0, istore, istore0, zh, ri, fi1, ld0), inv(istore), inv(istore0), flushed(istore0), istore0 ⊑ istore, maxino ∈ gstore0, inv(groupblock(gndlist0, lax, m, m0, m1, false)), ¬ dups(nx0), ¬ maxino ∈ ginval0, ∃ ri, fi, ld. btree-inv(rp, adr, gstore0 \ ginval0, istore, istore0, zh, ri, fi, ld), inv-journal(nx0, gstore0, gstore2, ginval0), maxino ∈ nx0, gstore0[maxino].size + gndlist.flashsize ≤ LEB_SIZE, ¬ gstore0[maxino].failed, rp0 = rp, adr0 = adr, ginval1 = ginval0, istore1 = istore, istore2 = istore0, zh0 = zh, nx1 = nx0, gstore1 = gstore2, maxino0 = maxino, gndlist1 = gndlist ⊦ [btree_add_gnds#(maxino, gndlist, nx0; ax, gstore0; err)] ( (∃ ri, fi, ld. btree-inv(rp0, adr0, gstore0 \ ginval1, istore1, istore2, zh0, ri, fi, ld)) ∧ inv-journal(nx1, gstore0, gstore1, ginval1) ∧ true → ⟨index+persistence_add_gnds#(maxino, gndlist, nx0; ax0, gstore; err0)⟩ (gstore = gstore0 ∧ btree-inv(rp, adr, gstore0 \ ginval0, istore, istore0, zh, fi, fi0, ld) ∧ ax = ax0 ∧ err = err0))

Rule argument

Additional information