| # vols[v] = # vols0[v], # apebs0 = # wlar0, # wlar = # wlar0, bflipset-cons(bflipset, wlar), bflipset-cons(bflipset0, wlar0), ebm-cons(avols0), is-max(apebs0, vols0, wlar0, q0, bflipset0, vtblpnum3, sqnum), ubi-io-inv(apebs0), unique-sqns(apebs0), valid-ebatbl(apebs0, wlar, vols, vtblpnum), valid-ebatbl(apebs0, wlar0, vols0, vtblpnum3), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs0, q), valid-eraseq(q0), valid-eraseq(wlar0, q0), valid-eraseq(apebs0, q0), valid-global-sqn(apebs0, vtblpnum0), valid-global-sqn(apebs0, sqnum), valid-vtbl(apebs0, vols, wlar, vtblpnum), valid-vtbl(apebs0, vols0, wlar0, vtblpnum3), valid-wl(apebs0, wlar), valid-wl(apebs0, wlar0), v ∈ vols0, v ∈ vols, v ∈ avols0, q0.lebrefs ⊆ q.lebrefs, vols0⌈vols, q⌉, m < # vols0[v] ∧ vols[v][m] ≠ unmapped → vols[v][m] = vols0[v][m], ∀ v. (v ∈ vols ↔ v ∈ avols0) ∧ ( v ∈ vols → # vols[v] = # avols0[v] ∧ (∀ m. m < # vols[v] → (vols[v][m] = unmapped → ¬ avols0[v][m].mapped?) ∧ ( vols[v][m] ≠ unmapped → avols0[v][m].mapped? ∧ avols0[v][m].data = apebs0[vols[v][m].pnum].data ∧ apebs0[vols[v][m].pnum].fill ≤ avols0[v][m].fill) ∧ (avols0[v][m] = erased → ¬ v × m ∈ q))) ⊦ VTBL_VOLID ∈ vols0, VTBL_VOLID ∈ vols, # avols0[v] = # vols0[v] ∧ ( m < # avols0[v] ∧ avols0[v][m] ≠ unmapped → (avols0[v][m] = erased → absf(v, avols0[v], apebs0, vols0[v], q0, # vols0[v])[m] = erased) ∧ (avols0[v][m].mapped? → absf(v, avols0[v], apebs0, vols0[v], q0, # vols0[v])[m] = avols0[v][m])) |
# wlar = # wlar0, # apebs0 = # wlar0, # vols[v] = # vols0[v], v ∈ vols ↔ v ∈ avols0, bflipset-cons(bflipset0, wlar0), bflipset-cons(bflipset, wlar), ebm-cons(avols0), is-max(apebs0, vols0, wlar0, q0, bflipset0, vtblpnum3, sqnum), ubi-io-inv(apebs0), unique-sqns(apebs0), valid-ebatbl(apebs0, wlar0, vols0, vtblpnum3), valid-ebatbl(apebs0, wlar, vols, vtblpnum), valid-eraseq(apebs0, q0), valid-eraseq(wlar0, q0), valid-eraseq(q0), valid-eraseq(apebs0, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-global-sqn(apebs0, sqnum), valid-global-sqn(apebs0, vtblpnum0), valid-vtbl(apebs0, vols0, wlar0, vtblpnum3), valid-vtbl(apebs0, vols, wlar, vtblpnum), valid-wl(apebs0, wlar0), valid-wl(apebs0, wlar), v ∈ avols0, v ∈ vols, v ∈ vols0, q0.lebrefs ⊆ q.lebrefs, vols0⌈vols, q⌉, m < # vols0[v] ∧ vols[v][m] ≠ unmapped → vols[v][m] = vols0[v][m], v ∈ vols → # vols[v] = # avols0[v] ∧ (∀ m. m < # vols[v] → (vols[v][m] = unmapped → ¬ avols0[v][m].mapped?) ∧ ( vols[v][m] ≠ unmapped → avols0[v][m].mapped? ∧ avols0[v][m].data = apebs0[vols[v][m].pnum].data ∧ apebs0[vols[v][m].pnum].fill ≤ avols0[v][m].fill) ∧ (avols0[v][m] = erased → ¬ v × m ∈ q)) ⊦ VTBL_VOLID ∈ vols, VTBL_VOLID ∈ vols0, # avols0[v] = # vols0[v] ∧ ( m < # avols0[v] ∧ avols0[v][m] ≠ unmapped → (avols0[v][m] = erased → absf(v, avols0[v], apebs0, vols0[v], q0, # vols0[v])[m] = erased) ∧ (avols0[v][m].mapped? → absf(v, avols0[v], apebs0, vols0[v], q0, # vols0[v])[m] = avols0[v][m]))
Used terms: v