| # apebs0 = # wlar, LEB_SIZE = n3 + align↑(datasize(buf, n0), EB_PAGE_SIZE), LEB_SIZE = n2 + n0, LEB_SIZE = n4 + align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), wlar[n1] = wl-entry(m1, free), apebs0[n1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), q0 = q, vols0 = vols, vtblpnum0 = vtblpnum1, vtblpnum2 = n1, vtblpnum3 = m0, aehdr.valid?, n1 < # wlar, vtblpnum3 < # vols[v], bflipset-cons(bflipset, wlar), is-aligned(n0, EB_PAGE_SIZE), ubi-io-inv (apebs0 [n1, mkpeb (aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false) ]), ubi-io-inv(apebs0), ubi-io-inv(apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), mkempbuf(LEB_SIZE), 0, false)]), 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), v ∈ vols, n0 ≤ # buf, n0 ≤ LEB_SIZE, align↑(datasize(buf, n0), EB_PAGE_SIZE) ≤ LEB_SIZE, align↑(datasize(buf, n0), EB_PAGE_SIZE) ≤ # buf, align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE) ≤ LEB_SIZE, v ∈ vols ∧ m0 < # vols[v] ∨ v = VTBL_VOLID ∧ m0 = VTBL_LNUM ⊦ vols[v][vtblpnum3] = unmapped, vtblpnum1 = n1, VTBL_VOLID ∈ vols, vtblpnum1 ∈ q, ∃ buf0. buf = mkempbuf(n0) + buf0, v = VTBL_VOLID ∧ m0 = VTBL_LNUM, vols[v][vtblpnum3] ≠ unmapped ∧ vtblpnum3 < # vols[v] ∧ v ∈ vols |