Proof step 3 from proof valid-eraseqw-free (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

  ∀ n. n ∈ q0 + eq-entry(m, lref) ' + q1 ↔ n < # wlar ∧ wlar[n].status = erasing, ∀ n. n ∈ q0 + q1 ↔ n < # wlar ∧ wlar[m, wl-entry(m0, stat)][n].status = erasing ⊦ stat = erasing, ¬ m ∈ q0 ∧ ¬ m ∈ q1

• Proof step 6:

  ∀ n. n ∈ q0 + eq-entry(m, lref) ' + q1 ↔ n < # wlar ∧ wlar[n].status = erasing ⊦ stat = erasing, m ∈ q1, m ∈ q0, ∀ n. n ∈ q0 + q1 ↔ n < # wlar ∧ wlar[m, wl-entry(m0, stat)][n].status = erasing

Rule argument

Additional information