| # vols[v] = # avols[v], # apebs0 = # wlar0, # apebs = # wlar, apebs[n0] = mkpeb(aehdr0, avhdr0, buf0, m1, false), vols[v][m] = ⌜n0⌝ , apebs0[n] = mkpeb(aehdr, avhdr, buf0, m0, boolvar), avols[v][m] = mapped(buf0, m2), avhdr0.valid?, n0 < # wlar, m < # avols[v], m2 < m0, m2 < m1, abs○(avols, apebs0, vols[v, vols[v][m, ⌜n⌝ ]], q, v, m), bflipset-cons(bflipset0, wlar0), bflipset-cons(bflipset, wlar), ebm-cons(avols), id(apebs0, apebs, mapped-pebs(vols) -- n0), ubi-io-inv(apebs0), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aehdr0, avhdr0, buf0, m1, false)), unique-sqns(apebs0), unique-sqns(apebs), valid-ebatbl(apebs0, wlar0, vols[v, vols[v][m, ⌜n⌝ ]], vtblpnum0), valid-ebatbl(apebs, wlar, vols, vtblpnum), valid-eraseq(q0), valid-eraseq(wlar0, q0), valid-eraseq(apebs0, q0), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-global-sqn(apebs0, sqnum0), valid-global-sqn(apebs, sqnum), valid-vtbl(apebs0, vols, wlar0, vtblpnum0), valid-vtbl(apebs, vols, wlar, vtblpnum), valid-wl(apebs0, wlar0), valid-wl(apebs, wlar), v ∈ avols, v ∈ vols, m0 ≤ m1, q0.lebrefs ⊆ q.lebrefs ++ (v × m), ∀ m. m < # avols[v] → (vols[v][m] = unmapped → ¬ avols[v][m].mapped?) ∧ (vols[v][m] ≠ unmapped → avols[v][m].mapped? ∧ avols[v][m].data = apebs[vols[v][m].pnum].data ∧ apebs[vols[v][m].pnum].fill ≤ avols[v][m].fill) ∧ (avols[v][m] = erased → ¬ v × m ∈ q) ⊦ abs(avols, apebs0, vols[v, vols[v][m, ⌜n⌝ ]], q0), abs(avols, apebs0, vols[v, vols[v][m, ⌜n⌝ ]], q), VTBL_VOLID ∈ vols |
Used simplifier rules: ⊦ erased ≠ mapped(buf, m); (s)% ⊦ unmapped ≠ ⌜m⌝ ; (s)% ⊦ mapped(buf, m).mapped?; (s)% ⊦ mapped(buf, m).data = buf; (s)% ⊦ ⌜m⌝ .pnum = m; (s)% ⊦ mapped(buf, m).fill = m; (s)%fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).data = buf; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).fill = m; (s)% ⊦ m ≤ n → (n < m ↔ false); (s) Used terms: m