| # buf3 = EB_PAGE_SIZE, (5 + 2 * lptlebs(# lpt, LEB_SIZE)) + # lpt = # avol, avol[m6] = mapped(buf1), avol[m2] = mapped(buf0), avol[0] = mapped(buf2), m6 < # avol, ebm-vol-inv(avol[m6, mapped(buf1 + buf3)]), ebm-vol-inv(avol), is-encoded(rnode(m8), buf3), is-encoded(mksb(adr, m7, m6, m2, m3, m4, 5 + 2 * lptlebs(# lpt, LEB_SIZE)), buf2), is-encoded(lpt, lebs(avol, m4, lptlebs(# lpt, LEB_SIZE))), is-encoded(log, buf1), is-encoded-pad(orphans, m3, buf0), mapped-full?(avol, m4, lptlebs(# lpt, LEB_SIZE)), # buf1 + EB_PAGE_SIZE ≤ LEB_SIZE, m6 = 1 ∧ m2 = 3 ∧ m4 = 5 ∨ m6 = 2 ∧ m2 = 4 ∧ m4 = 5 + lptlebs(# lpt, LEB_SIZE) ⊦ # buf1 = LEB_SIZE, is-encoded(lpt, lebs(avol[m6, mapped(buf1 + buf3)], m4, lptlebs(# lpt, LEB_SIZE))) |
Used simplifier rules: nat-stuff2: ⊦ n = 5 + n1 → n ≠ 0;%nat-stuff3: ⊦ n = 5 + n1 → n ≠ 1;%n < n0 ⊦ (* n) < m0 + (* n0); (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic% ⊦ m + m = 2 * 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%lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic%transitivity: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification oelem[nat-set]%n < n0 ⊦ (* n) ≠ m0 + (* n0); (s)% ⊦ m + n < m + n0 ↔ n < n0; (s)% ⊦ ¬ m + n < m; (s)%n0 < n, n + m ≤ # avol ⊦ lebs(avol[n0, aleb], n, m) = lebs(avol, n, m); (s)% ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s)% ⊦ m * n + n0 < n ↔ m = 0 ∧ n0 < n; (ws)%mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult%mult-c: ⊦ m * n = n * m; from specification nat-mult