| m6 + # lpt = # avol, avol[m6 + m8] = mapped(buf0), avol[m2] = mapped(buf3), avol[m3] = mapped(buf2), avol[0] = mapped(buf1), m8 < # lpt, n1 < n, disk-layout(mksb(adr, m1, m2, m3, m4, m5, m6), # lpt), ebm-vol-inv(avol), ebm-vol-inv(avol[m6 + m8, mapped(buf0 + mkempbuf(n0) + subarray(buf, n2, n1))]), is-aligned(n, EB_PAGE_SIZE), is-aligned(n0 + # buf0, EB_PAGE_SIZE), is-aligned(n1, EB_PAGE_SIZE), is-encoded(mksb(adr, m1, m2, m3, m4, m5, m6), buf1), is-encoded(lpt, lebs(avol, m5, lptlebs(# lpt, LEB_SIZE))), is-encoded(log, buf3), is-encoded-pad(orphans, m4, buf2), mapped-full?(avol, m5, lptlebs(# lpt, LEB_SIZE)), n2 + n ≤ # buf, (n0 + # buf0) + n ≤ LEB_SIZE, n2 + n1 ≤ # buf, ⌊err0⌋ , logoff ≠ LEB_SIZE → # buf3 = logoff ⊦ 0 = m6 + m8, m2 = m6 + m8, n1 = 0, ∃ lpt0. m6 + # lpt0 = # avol ∧ mapped-full?(avol[m6 + m8, mapped(buf0 + mkempbuf(n0) + subarray(buf, n2, n1))], m5, lptlebs(# lpt0, LEB_SIZE)) ∧ is-encoded(lpt0, lebs(avol[m6 + m8, mapped(buf0 + mkempbuf(n0) + subarray(buf, n2, n1))], m5, lptlebs(# lpt0, LEB_SIZE))) |
Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss)%⊦ disk-layout(mksb(adr, m0, m1, m2, m, m3, m4), mainareasize) → ¬ m4 + n < m3 + lptlebs(mainareasize, LEB_SIZE); (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic%n + m ≤ n0 ⊦ mapped-full?(avol[n0, aleb], n, m) ↔ mapped-full?(avol, n, m); (s)%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic% ⊦ m < n → n ≠ 0; (s)%n + m ≤ n0, n + m ≤ # avol ⊦ lebs(avol[n0, aleb], n, m) = lebs(avol, n, m); (s) Used terms: lpt