| # wlar0 = n0 + vtblpnum, # apebs = n0 + vtblpnum, avhdr.sqn = valid-sqns(v, m1, apebs, vtblpnum).max, wlar0[m3] = wl-entry(m6, stat), apebs[m3] = mkpeb(aehdr, avhdr, buf, m5, boolvar), recs[v × m1] = recovery-entry(m3, avhdr.sqn), apebs[vtblpnum] = mkpeb(aechdr(m), avidhdr(v, m1, m2, 0, m4), buf1, m0, false), nx < vtblpnum, m3 < vtblpnum, m3 < n0 + vtblpnum, bflipset-cons(bflipset, subarray(wlar0, 0, vtblpnum)), indices-erasing(wlar0, nx), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aechdr(m), avidhdr(v, m1, m2, 0, m4), buf1, m0, false)), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf, m5, boolvar)), unique-sqns(apebs), valid-eraseq(subarray(wlar0, 0, vtblpnum), q), valid-eraseq-stronger(subarray(apebs, 0, vtblpnum), q), valid-global-sqn(subarray(apebs, 0, vtblpnum), sqnum), valid-peb(v, m1, mkpeb(aehdr, avhdr, buf, m5, boolvar)), valid-recs(subarray(apebs, 0, vtblpnum), subarray(wlar0, 0, vtblpnum), recs), valid-recs-sqns(apebs, recs), valid-wl(subarray(apebs, 0, vtblpnum), subarray(wlar0, 0, vtblpnum)), v × m1 ∈ recs, avhdr.sqn ≤ m2 ⊦ n0 = 0, dups(nx), m3 ∈ q, ∃ m7, m8, m9. avidhdr(v, m1, m2, 0, m4) = avidhdr(v, m1, m7, m8, m9) ∧ (m8 ≠ 0 → m8 ≤ datasize(buf1) ∧ m9 = checksum(buf1, m8)), indices-erasing(wlar0[vtblpnum, wl-entry(m, used)][m3, wl-entry(m6, erasing)], nx) ∧ valid-global-sqn(subarray(apebs, 0, vtblpnum + 1), max(sqnum, m2 + 1)) ∧ valid-eraseq-stronger(subarray(apebs, 0, vtblpnum + 1), q + eq-entry(m3, v × m1) ') ∧ valid-wl(subarray(apebs, 0, vtblpnum + 1), subarray(wlar0[vtblpnum, wl-entry(m, used)][m3, wl-entry(m6, erasing)], 0, vtblpnum + 1)) ∧ valid-recs-sqns(apebs, recs[v × m1, recovery-entry(vtblpnum, m2)]) |
Used terms: m2, 0, m4