| # avol0 = # avol1, # lpt0 = # avol1, # buf1 = EB_PAGE_SIZE, avol0[m4] = mapped(buf2), adr = adr0, align↓(m2 + n3, EB_PAGE_SIZE) = n + m2, avol = avol0, buf = copy(buf3, 0, copy(buf1, 0, mkbuf(n + m2), 0, m2), m2, n), lpt = lpt0, m = m3, m0 = # buf2, m1 = buffered(m4).leb, n0 = n + m2, n1 = 0, ns = ns0, plog = plog0, buffered(m4).isbuf?, m4 < # avol1, m2 < EB_PAGE_SIZE, abs(avol1, buffered(m4), mkwbuf(buf1, # buf2, m2), avol0, false), awbuf-inv(avol1, buffered(m4)), ebm-vol-inv(avol0), is-aligned(# buf2, EB_PAGE_SIZE), 0 + n ≤ # buf3, m2 + n ≤ # copy(buf1, 0, mkbuf(n + m2), 0, m2), 0 + m2 ≤ # buf1, 0 + m2 ≤ # mkbuf(n + m2), # avol1[m4].data + n3 ≤ LEB_SIZE, n3 ≤ # buf3, EB_PAGE_SIZE ≤ m2 + n3, # buf2 + m2 + n3 ≤ LEB_SIZE, n ≤ # buf3, m1 < # avol → m1 < # avol ∧ (avol[m1].mapped? → avol[m1].mapped? ∧ m1 < # avol) ⊦ n3 = 0, m1 < # avol ∧ avol[m1].mapped? ∧ # avol[m1].data ≤ m0 ∧ is-aligned(m0, EB_PAGE_SIZE) ∧ is-aligned(n0, EB_PAGE_SIZE) ∧ m0 + n0 ≤ LEB_SIZE ∧ n1 + n0 ≤ # buf |
Used simplifier rules: m ≠ 0 ⊦ align↓(n0 + n1, m) = n2 + n1 → ¬ n0 < n2; (s)% ⊦ m + n < m + n0 ↔ n < n0; (s)% ⊦ m < n → n ≠ 0; (s)%fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic% ⊦ m ≤ n ↔ ¬ n < m; (ss)% ⊦ mapped(buf).data = buf; (s)% ⊦ mapped(buf).mapped?; (s)% ⊦ m < n → m ≤ n; (s)%m ≠ 0 ⊦ n = align↓(n0, m) → is-aligned(n, m); (ss)% ⊦ EB_PAGE_SIZE ≠ 0; (s)% ⊦ buffered(m).leb = m; (s)% ⊦ buffered(m).isbuf?; (s)% ⊦ m ≤ m; (s)% ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s)% ⊦ # copy(buf, m, buf0, m0, n) = # buf0; (s)% ⊦ m ≤ m + n; (s)% ⊦ # mkbuf(n) = n; (s)%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ n + 0 = n; (s)