| # apebs = # wlar, # vols[v] = # avols[v], # buf2 = n2 + n0 + n, avols[v][vtblpnum5] = mapped(buf1, m0), vols[v][vtblpnum5] = ⌜n1⌝ , apebs[n1] = mkpeb(aehdr, avhdr, buf1, m, false), n1 < # wlar, vtblpnum5 < # avols[v], bflipset-cons(bflipset, wlar), ebm-cons(avols), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf1, m, false)), unique-sqns(apebs), valid-ebatbl(apebs, wlar, vols, vtblpnum3), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-global-sqn(apebs, sqnum), valid-vtbl(apebs, vols, wlar, vtblpnum3), valid-wl(apebs, wlar), v ∈ avols, v ∈ vols, vtblpnum4 + n ≤ LEB_SIZE, n0 + n ≤ # buf2, m ≤ m0, ⌊err0⌋ ⊦ VTBL_VOLID ∈ vols, ∃ buf1. # buf1 = # buf2 ∧ range=(buf1, 0, buf2, 0, n0) ∧ range=(buf1, n0 + n, buf2, n0 + n, n2) |
Used simplifier rules: ⊦ range=(buf, n, buf, n, m) ↔ n + m ≤ # buf; (s)% ⊦ n + 0 = n; (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic% ⊦ m ≤ m; (s)% ⊦ m ≤ n ↔ ¬ n < m; (ss)%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic%fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat% ⊦ m < n → n ≠ 0; (s)% ⊦ m + m0 < n → ¬ n + n0 < m; (s) Used terms: buf2