Proof step 4 from proof absexpt-pebs-write (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  vols[v][m] = ⌜n⌝ , m < # vols[v], valid-ebatbl(apebs, wlar, vols, n0), v ∈ vols, ∀ v1. (v1 ∈ vols ↔ v1 ∈ avols) ∧ ( v1 ∈ vols → # vols[v1] = # avols[v1] ∧ (∀ m1. (v1 ≠ v ∨ m1 ≠ m) ∧ m1 < # vols[v1] → (vols[v1][m1] = unmapped → ¬ avols[v1][m1].mapped?) ∧ ( vols[v1][m1] ≠ unmapped → avols[v1][m1].mapped? ∧ avols[v1][m1].data = apebs[n, apeb][vols[v1][m1].pnum].data ∧ apebs[n, apeb][vols[v1][m1].pnum].fill ≤ avols[v1][m1].fill) ∧ (avols[v1][m1] = erased → ¬ v1 × m1 ∈ q))) ⊦ (v0 ∈ vols ↔ v0 ∈ avols) ∧ ( v0 ∈ vols → # vols[v0] = # avols[v0] ∧ ( (v0 ≠ v ∨ m0 ≠ m) ∧ m0 < # vols[v0] → (vols[v0][m0] = unmapped → ¬ avols[v0][m0].mapped?) ∧ ( vols[v0][m0] ≠ unmapped → avols[v0][m0].mapped? ∧ avols[v0][m0].data = apebs[vols[v0][m0].pnum].data ∧ apebs[vols[v0][m0].pnum].fill ≤ avols[v0][m0].fill) ∧ (avols[v0][m0] = erased → ¬ v0 × m0 ∈ q)))

Rule argument

Additional information