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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 245:

  # apebs0 = # wlar, LEB_SIZE = n2 + n0, LEB_SIZE = n4 + # buf1, apebs0[n1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), wlar[n1] = wl-entry(m1, free), align↑(datasize(buf, n0), EB_PAGE_SIZE) = n3 + # buf1, aehdr.valid?, n1 < # wlar, bflipset-cons(bflipset, wlar), is-aligned(n0, EB_PAGE_SIZE), is-aligned(# buf1, EB_PAGE_SIZE), ubi-io-inv (apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), buf1 + mkempbuf(n4), # buf1, false)]), ubi-io-inv(apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), mkempbuf(LEB_SIZE), 0, false)]), ubi-io-inv(apebs0), unique-sqns(apebs0), valid-ebatbl(apebs0, wlar, vols, vtblpnum1), valid-eraseq(apebs0, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-eraseq(q + eq-entry(n1, none) '), valid-global-sqn(apebs0, sqnum), valid-vtbl(apebs0, vols, wlar, vtblpnum1), valid-wl(apebs0, wlar), n3 + # buf1 ≤ # buf, n3 + # buf1 ≤ LEB_SIZE, n0 ≤ LEB_SIZE, n0 ≤ # buf, # buf1 ≤ # buf, # buf1 ≤ LEB_SIZE, ⌊err0⌋ , v ∈ vols ∧ m0 < # vols[v] ∨ v = VTBL_VOLID ∧ m0 = VTBL_LNUM, datasize(buf1, # buf1) < datasize(buf, n0) ∨ checksum(buf1 + mkempbuf(n3), datasize(buf, n0)) ≠ checksum(buf, datasize(buf, n0)) ⊦ vtblpnum1 = n1, valid-eraseq (apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), buf1 + mkempbuf(n4), # buf1, false)], q + eq-entry(n1, none) '), valid-peb(v, m0, mkpeb(aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), buf1 + mkempbuf(n4), # buf1, false)), vtblpnum1 ∈ q, VTBL_VOLID ∈ vols, ∃ buf0. buf = mkempbuf(n0) + buf0

Rule argument

Additional information