Proof step 463 from proof prepost-atomic-leb-change (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 464:

  # apebs0 = # wlar, LEB_SIZE = n2 + n0, wlar[n1] = wl-entry(m1, free), apebs0[n1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), lref = none, q0 = q, vtblpnum = n1, aehdr.valid?, n1 < # wlar, vtblpnum < # wlar, bflipset-cons(bflipset, wlar), is-aligned(n0, EB_PAGE_SIZE), ubi-io-inv(apebs0[n1, mkpeb(aehdr, avhdr, mkempbuf(LEB_SIZE), 0, false)]), ubi-io-inv(apebs0), unique-sqns(apebs0), valid-ebatbl(apebs0, wlar, vols, vtblpnum1), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs0, q), valid-global-sqn(apebs0, sqnum), valid-vtbl(apebs0, vols, wlar, vtblpnum1), valid-wl(apebs0, wlar), n0 ≤ LEB_SIZE, ⌊err0⌋ , v ∈ vols ∧ m0 < # vols[v] ∨ v = VTBL_VOLID ∧ m0 = VTBL_LNUM ⊦ vtblpnum1 = n1, avhdr.valid?, vtblpnum1 ∈ q, VTBL_VOLID ∈ vols, # apebs0 = # wlar[vtblpnum, wlar[vtblpnum].status:= erasing] ∧ unique-sqns(apebs0[n1, apebs0[n1].vidhdr:= avhdr]) ∧ valid-global-sqn(apebs0[n1, apebs0[n1].vidhdr:= avhdr], sqnum + 1) ∧ valid-wl(apebs0[n1, apebs0[n1].vidhdr:= avhdr], wlar[vtblpnum, wlar[vtblpnum].status:= erasing]) ∧ valid-eraseq(q + eq-entry(vtblpnum, lref)) ∧ valid-eraseq(wlar[vtblpnum, wlar[vtblpnum].status:= erasing], q + eq-entry(vtblpnum, lref)) ∧ valid-eraseq(apebs0[n1, apebs0[n1].vidhdr:= avhdr], q + eq-entry(vtblpnum, lref)) ∧ bflipset-cons(bflipset, wlar[vtblpnum, wlar[vtblpnum].status:= erasing]) ∧ valid-ebatbl(apebs0[n1, apebs0[n1].vidhdr:= avhdr], wlar[vtblpnum, wlar[vtblpnum].status:= erasing], vols, vtblpnum1) ∧ valid-vtbl(apebs0, vols, wlar[vtblpnum, wlar[vtblpnum].status:= erasing], vtblpnum1) ∧ id(apebs0[n1, apebs0[n1].vidhdr:= avhdr], apebs0, mapped-pebs(vols)) ∧ (q + eq-entry(vtblpnum, lref)).lebrefs = q0.lebrefs

Rule argument

Additional information