| # vols[v] = # vols0[v], # avols0[v] = # vols0[v], # wlar = # wlar0, # apebs0 = # wlar0, apebs0[n] = mkpeb(aehdr, avhdr, buf, m0, false), vols0[v][m] = ⌜n⌝ , avols0[v][m] = mapped(buf0, m1), avhdr.valid?, m1 < m0, m < # vols0[v], n < # wlar0, bflipset-cons(bflipset0, wlar0), bflipset-cons(bflipset, wlar), ebm-cons(avols0), is-max(apebs0, vols0, wlar0, q0, bflipset0, vtblpnum3, sqnum), ubi-io-inv(apebs0), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf, m0, false)), 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⌉, vols[v][m] ≠ unmapped → vols[v][m] = ⌜n⌝ , ∀ m. m < # vols0[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 |
Used simplifier rules: ⊦ erased ≠ mapped(buf, m); (s)% ⊦ mapped(buf, m).mapped?; (s)% ⊦ mapped(buf, m).data = buf; (s)% ⊦ mapped(buf, m).fill = m; (s)%fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat% ⊦ ⌜m⌝ .pnum = m; (s)% ⊦ unmapped ≠ ⌜m⌝ ; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).data = buf; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).fill = m; (s)% ⊦ ¬ n < n; (s) Used terms: m