| # vols[v] = # avols[v], # apebs = # wlar, # buf1 = # buf2, # buf2 = n3 + n0 + n, apebs[n1] = mkpeb(aehdr, avhdr, buf0, m, false), vols[v][vtblpnum5] = ⌜n1⌝ , avols[v][vtblpnum5] = mapped(buf0, m0), vtblpnum5 < # avols[v], n1 < # wlar, bflipset-cons(bflipset, wlar), ebm-cons(avols), range=(buf1, n0 + n, buf2, n0 + n, n3), range=(buf1, 0, buf2, 0, n0), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf0, m, false)), unique-sqns(apebs), valid-ebatbl(apebs, wlar, vols, vtblpnum3), valid-eraseq(apebs, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-global-sqn(apebs, sqnum), valid-vtbl(apebs, vols, wlar, vtblpnum3), valid-wl(apebs, wlar), v ∈ vols, v ∈ avols, m ≤ m0, n0 + n ≤ # buf2, vtblpnum4 + n ≤ LEB_SIZE, ⌊err1⌋ , ¬ VTBL_VOLID ∈ vols ⊦ ⟨buf2 := buf1⟩ (buf1 = buf2) |