Proof step 4 from proof valid-wl-erasing-invalidate (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  # apebs = # wlar, wlar[m] = wl-entry(m0, erasing), n < # wlar, m < # wlar, ∀ n. n < # wlar → (wlar[n].status = erroneous ↔ apebs[n].bad) ∧ (wlar[n].status = free → apebs[n].vidhdr = empty) ∧ (wlar[n].status ≠ erroneous ∧ wlar[n].status ≠ erasing → apebs[n].echdr = aechdr(wlar[n].ec)) ∧ (wlar[n].status = used → (∃ v, m. valid-peb(v, m, apebs[n]) ∧ apebs[n].vidhdr.sqn = valid-sqns(v, m, apebs).max)) ⊦ valid-peb(mkpeb(aehdr, avhdr, buf, m2, false)), (wlar[n].status = erroneous ↔ apebs[m, mkpeb(aehdr, avhdr, buf, m2, false)][n].bad) ∧ (wlar[n].status = free → apebs[m, mkpeb(aehdr, avhdr, buf, m2, false)][n].vidhdr = empty) ∧ (wlar[n].status ≠ erroneous ∧ wlar[n].status ≠ erasing → apebs[m, mkpeb(aehdr, avhdr, buf, m2, false)][n].echdr = aechdr(wlar[n].ec)) ∧ ( wlar[n].status = used → (∃ v, m1. valid-peb(v, m1, apebs[m, mkpeb(aehdr, avhdr, buf, m2, false)][n]) ∧ apebs[n].vidhdr.sqn = valid-sqns(v, m1, apebs[m, mkpeb(aehdr, avhdr, buf, m2, false)]).max))

Rule argument

Additional information