Proof step 6 from proof absexpt-vols-abs (previous step)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 7:

  v0 ∈ vols ↔ v0 ∈ avols, apebs[vols[v, fill(mkebatbl(n), unmapped)][v0][m].pnum] = mkpeb(aehdr, avhdr, buf, m0, boolvar), v0 ∈ avols → # vols[v0] = # avols[v0] ∧ (∀ m. m < # vols[v0] → (vols[v0][m] = unmapped → ¬ avols[v0][m].mapped?) ∧ ( vols[v0][m] ≠ unmapped → avols[v0][m].mapped? ∧ avols[v0][m].data = apebs[vols[v0][m].pnum].data ∧ apebs[vols[v0][m].pnum].fill ≤ avols[v0][m].fill) ∧ (avols[v0][m] = erased → ¬ v0 × m ∈ q)) ⊦ v0 = v, v ∈ vols, (v0 ∈ vols[v, fill(mkebatbl(n), unmapped)] ↔ v0 ∈ avols[v, fill(mkabstractvolume(n), erased)]) ∧ ( v0 ∈ vols[v, fill(mkebatbl(n), unmapped)] → # vols[v, fill(mkebatbl(n), unmapped)][v0] = # avols[v, fill(mkabstractvolume(n), erased)][v0] ∧ ( m < # vols[v, fill(mkebatbl(n), unmapped)][v0] → (vols[v, fill(mkebatbl(n), unmapped)][v0][m] = unmapped → ¬ avols[v, fill(mkabstractvolume(n), erased)][v0][m].mapped?) ∧ ( vols[v, fill(mkebatbl(n), unmapped)][v0][m] ≠ unmapped → avols[v, fill(mkabstractvolume(n), erased)][v0][m].mapped? ∧ avols[v, fill(mkabstractvolume(n), erased)][v0][m].data = buf ∧ m0 ≤ avols[v, fill(mkabstractvolume(n), erased)][v0][m].fill) ∧ (avols[v, fill(mkabstractvolume(n), erased)][v0][m] = erased → ¬ v0 × m ∈ q - v)))

Rule argument

Additional information

Used simplifier rules: ⊦ vols[v, ebatbl][v] = ebatbl; (s)% ⊦ v ∈ vols[v0, ebatbl] ↔ v = v0 ∨ v ∈ vols; (ws)% ⊦ v ∈ avols[v, evol]; (s)% ⊦ v ∈ avols[v0, evol] ↔ v = v0 ∨ v ∈ avols; (ws)% ⊦ v ∈ vols[v, ebatbl]; (s)% ⊦ # fill(ebatbl, ebae) = # ebatbl; (s)% ⊦ # mkebatbl(n) = n; (s)% ⊦ avols[v, evol][v] = evol; (s)% ⊦ # fill(evol, leb) = # evol; (s)% ⊦ # mkabstractvolume(n) = n; (s)% ⊦ m < n → fill(mkebatbl(n), ebae)[m] = ebae; (s)% ⊦ m < n → fill(mkabstractvolume(n), leb)[m] = leb; (s)% ⊦ ¬ erased.mapped?; (s)% ⊦ ¬ v × m ∈ q - v; (s) Used formulas: v0 = v