Proof step 5 from proof bitflip-cons-set (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 6:

  ∀ n. n ∈ bflipset → n < # wlar ∧ wlar[m, wl-entry(m0, stat)][n].status = used ⊦ stat = used, (∀ n. n ∈ bflipset → n < # wlar ∧ wlar[n].status = used) ∧ ¬ m ∈ bflipset

• Proof step 13:

  ∀ n. n ∈ bflipset → n < # wlar ∧ wlar[n].status = used ⊦ stat = used, m ∈ bflipset, ∀ n. n ∈ bflipset → n < # wlar ∧ wlar[m, wl-entry(m0, stat)][n].status = used

Rule argument

Additional information