Proof step 96 from proof prepost-scan-all (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 97:

  # apebs = n0 + vtblpnum, # wlar0 = n0 + vtblpnum, apebs[vtblpnum].vidhdr = empty, apebs[vtblpnum] = mkpeb(aechdr(m), avhdr1, buf1, m0, false), bitflips, err = err0, err = ESUCCESS, wlar = wlar0[vtblpnum, wlar0[vtblpnum].ec:= m], vtblpnum < # wlar0, vtblpnum < # apebs, nx < vtblpnum, vtblpnum < # wlar, bflipset-cons(bflipset, subarray(wlar0, 0, vtblpnum)), indices-erasing(wlar0, nx), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aechdr(m), avhdr1, buf1, m0, false)), 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-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)), ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪vtblpnum0 := vtblpnum + 1⟫ ( vtblpnum0 ≤ # apebs ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err = ESUCCESS → # apebs = # wlar[vtblpnum, wl-entry(wlar[vtblpnum].ec, erasing)] ∧ nx < vtblpnum0 ∧ indices-erasing(wlar[vtblpnum, wl-entry(wlar[vtblpnum].ec, erasing)], nx) ∧ valid-global-sqn(subarray(apebs, 0, vtblpnum0), sqnum) ∧ valid-eraseq(subarray(wlar[vtblpnum, wl-entry(wlar[vtblpnum].ec, erasing)], 0, vtblpnum0), q + eq-entry(vtblpnum, none) ') ∧ bflipset-cons(bflipset, subarray(wlar[vtblpnum, wl-entry(wlar[vtblpnum].ec, erasing)], 0, vtblpnum0)) ∧ valid-eraseq-stronger(subarray(apebs, 0, vtblpnum0), q + eq-entry(vtblpnum, none) ') ∧ valid-wl(subarray(apebs, 0, vtblpnum0), subarray(wlar[vtblpnum, wl-entry(wlar[vtblpnum].ec, erasing)], 0, vtblpnum0)) ∧ valid-recs-sqns(apebs, recs) ∧ valid-recs(subarray(apebs, 0, vtblpnum0), subarray(wlar[vtblpnum, wl-entry(wlar[vtblpnum].ec, erasing)], 0, vtblpnum0), recs)) ∧ # apebs < n0 + vtblpnum0), n0 = 0, dups(nx)

Rule argument

Additional information