Proof step 3 from proof valid-ebatbl-update-vhdrs-unused (previous step)

Heuristic pl case distinction applied rule case distinction

And obtained the following new goals

• Proof step 4:

  wlar[m] = wl-entry(m0, stat), ∀ v, m1, n0. vols[v][m1] = ⌜n0⌝ ∧ v ∈ vols ∧ m1 < # vols[v] ↔ wlar[n0].status = used ∧ n0 < # apebs ∧ n0 < # wlar ∧ apebs[m, apeb][n0].vidhdr.valid? ∧ apebs[m, apeb][n0].vidhdr.vol = v ∧ apebs[m, apeb][n0].vidhdr.leb = m1 ∧ n0 ≠ n ⊦ stat = used, ∀ v, m, n1. vols[v][m] = ⌜n1⌝ ∧ v ∈ vols ∧ m < # vols[v] ↔ wlar[n1].status = used ∧ n1 < # apebs ∧ n1 < # wlar ∧ apebs[n1].vidhdr.valid? ∧ apebs[n1].vidhdr.vol = v ∧ apebs[n1].vidhdr.leb = m ∧ n1 ≠ n

• Proof step 11:

  wlar[m] = wl-entry(m0, stat), ∀ v, m, n1. vols[v][m] = ⌜n1⌝ ∧ v ∈ vols ∧ m < # vols[v] ↔ wlar[n1].status = used ∧ n1 < # apebs ∧ n1 < # wlar ∧ apebs[n1].vidhdr.valid? ∧ apebs[n1].vidhdr.vol = v ∧ apebs[n1].vidhdr.leb = m ∧ n1 ≠ n ⊦ stat = used, ∀ v, m1, n0. vols[v][m1] = ⌜n0⌝ ∧ v ∈ vols ∧ m1 < # vols[v] ↔ wlar[n0].status = used ∧ n0 < # apebs ∧ n0 < # wlar ∧ apebs[m, apeb][n0].vidhdr.valid? ∧ apebs[m, apeb][n0].vidhdr.vol = v ∧ apebs[m, apeb][n0].vidhdr.leb = m1 ∧ n0 ≠ n

Rule argument

Additional information