| # wlar = # wlar0, # apebs = # wlar0, # apebs0 = # wlar0, UBI_ERASE_RETRIES = n0 + vtblpnum2, apebs[m] = mkpeb(aehdr, avhdr, buf, m2, false), wlar[m] = wl-entry(m1, erasing), wlar0[m] = wl-entry(m0, erasing), vtblpnum = m, m < # wlar0, bflipset-cons(bflipset, wlar), bflipset-cons(bflipset, wlar0), id○(wlar, wlar0, m), id○(apebs, apebs0, m), ubi-io-inv(apebs), ubi-io-inv(apebs0), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf, m2, false)), unique-sqns(apebs), unique-sqns(apebs0), valid-ebatbl(apebs, wlar, vols, vtblpnum1), valid-ebatbl(apebs0, wlar0, vols, vtblpnum1), valid-eraseq(apebs, q0 + eq-entry(m, lref) ' + q1), valid-eraseq(wlar, q0 + eq-entry(m, lref) ' + q1), valid-eraseq(apebs0, q0 + eq-entry(m, lref) ' + q1), valid-eraseq(wlar0, q0 + eq-entry(m, lref) ' + q1), valid-eraseq(q0 + eq-entry(m, lref) ' + q1), valid-global-sqn(apebs, sqnum), valid-global-sqn(apebs0, sqnum), valid-vtbl(apebs, vols, wlar, vtblpnum1), valid-vtbl(apebs0, vols, wlar0, vtblpnum1), valid-wl(apebs, wlar), valid-wl(apebs0, wlar0), vtblpnum2 ≤ UBI_ERASE_RETRIES + 1, vtblpnum2 ≤ UBI_ERASE_RETRIES ⊦ [abort] ( ubi-io-inv(apebs) → ⟪wlar[m].ec := wlar[m].ec + 1; if err = ESUCCESS then aubi_io_write_echdr#(m, aechdr(wlar[m].ec); apebs; err) else debug#("ubi: erase of PEB " + m.toString + " failed"); vtblpnum := vtblpnum2 + 1⟫ ( vtblpnum ≤ UBI_ERASE_RETRIES + 1 ∧ m < # apebs ∧ id○(apebs, apebs0, m) ∧ id○(wlar, wlar0, m) ∧ # apebs = # wlar ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, sqnum) ∧ valid-wl(apebs, wlar) ∧ valid-eraseq(wlar, q0 + eq-entry(m, lref) ' + q1) ∧ valid-eraseq(apebs, q0 + eq-entry(m, lref) ' + q1) ∧ bflipset-cons(bflipset, wlar) ∧ valid-ebatbl(apebs, wlar, vols, vtblpnum1) ∧ valid-vtbl(apebs, vols, wlar, vtblpnum1) ∧ ubi-io-inv(apebs) ∧ (err = ESUCCESS → apebs[m].echdr = aechdr(wlar[m].ec) ∧ apebs[m].vidhdr = empty ∧ ¬ apebs[m].bad) ∧ UBI_ERASE_RETRIES < n0 + vtblpnum)), err = ESUCCESS, vtblpnum1 = m, ubi-io-erase-pre(vtblpnum, apebs), vtblpnum1 ∈ q1, vtblpnum1 ∈ q0, VTBL_VOLID ∈ vols |