| # apebs = # wlar, # buf = n1 + n0 + n, apebs[m] = mkpeb(aehdr, avhdr, buf0, m1, false), vols[v][vtblpnum4] = ⌜m⌝ , wlar[m] = wl-entry(m0, used), vtblpnum4 < # vols[v], m < # wlar, bflipset-cons(bflipset, wlar), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf0, m1, false)), unique-sqns(apebs), valid-ebatbl(apebs, wlar, vols, vtblpnum5), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-global-sqn(apebs, sqnum), valid-peb(v, vtblpnum4, mkpeb(aehdr, avhdr, buf0, m1, false)), valid-peb(mkpeb(aehdr, avhdr, buf0, m1, false)), valid-vtbl(apebs, vols, wlar, vtblpnum5), valid-wl(apebs, wlar), v ∈ vols, vtblpnum3 + n ≤ LEB_SIZE, n0 + n ≤ # buf, ⌊err0⌋ ⊦ m = vtblpnum5, VTBL_VOLID ∈ vols, vtblpnum5 ∈ q, m ∈ q, ∃ buf1. # buf1 = # buf ∧ range=(buf1, 0, buf, 0, n0) ∧ range=(buf1, n0 + n, buf, n0 + n, n1) |
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: buf