Proof step 40 from proof prepost-write-lebs (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  # avol1 = n3 + n5 + n2 + n4, # buf = (n2 + n4) * LEB_SIZE, # avol0 = # avol1, lebs(avol0, n5, n4) = subarray(buf, 0, n4 * LEB_SIZE), n5 + n4 < # avol1, ebm-vol-inv(avol0), ebm-vol-inv(avol1), ebm-vol-inv(avol0[n5 + n4, mapped(mkbuf(0))]), ebm-vol-inv(avol0[n5 + n4, mapped(subarray(buf, n4 * LEB_SIZE, LEB_SIZE))]), is-aligned(LEB_SIZE, EB_PAGE_SIZE), mapped-full?(avol0, n5, n4), range=(avol0, 0, avol1, 0, n5), range=(avol0, n5 + n2 + n4, avol1, n5 + n2 + n4, n3), n5 + n2 + n4 ≤ # avol1, n4 * LEB_SIZE + LEB_SIZE ≤ # buf, 1 ≤ n2 ⊦ n3 + n2 = 0, lebs(avol0, n5, n4) + subarray(buf, n4 * LEB_SIZE, LEB_SIZE) = subarray(buf, 0, LEB_SIZE * n4 + LEB_SIZE), n2 = 0

Rule argument

Additional information

Used simplifier rules: not-zero: 0 < n ⊦ (* n) ≤ m → m ≠ 0; (forward) from specification nat% ⊦ m < 1 ↔ m = 0; (s)% ⊦ ¬ n < n; (s)% ⊦ m < n + 1 ↔ ¬ n < m; (s)%m + n < # avol ⊦ mapped-full?(avol[m + n, mapped(buf)], n, m + 1) ↔ # buf = LEB_SIZE ∧ mapped-full?(avol, n, m); (s)%mult-c: ⊦ m * n = n * m; from specification nat-mult%mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult% ⊦ m * (n + 1) = m * n + m; (s)%n + m + 1 ≤ # avol, # buf = LEB_SIZE ⊦ lebs(avol[n + m, mapped(buf)], n, m + 1) = lebs(avol, n, m) + buf; (s)% ⊦ # subarray(buf, m, n) = n; (s)% ⊦ m + 1 ≤ n ↔ m < n; (s)%n < m0 ⊦ range=(avol[n, aleb], m0, avol0, m1, m) ↔ range=(avol, m0, avol0, m1, m); (s)% ⊦ m + m0 ≤ m ↔ m0 = 0; (s)% ⊦ m + n < m + n0 ↔ n < n0; (s)%m0 + m ≤ n ⊦ range=(avol[n, aleb], m0, avol0, m1, m) ↔ range=(avol, m0, avol0, m1, m); (s)% ⊦ ¬ m + n < m; (s)% ⊦ m ≤ n ↔ ¬ n < m; (ss)% ⊦ n + 0 = n; (s)%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s)% ⊦ ¬ ⌊ESUCCESS⌋ ; (s)% ⊦ mapped(buf).mapped?; (s)% ⊦ # avol[n, aleb] = # avol; (s)%m < # avol ⊦ avol[m, aleb][m, aleb0] = avol[m, aleb0]; (s)% ⊦ m < n → (n ≤ m ↔ false); (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)%append-a: ⊦ (buf + buf0) + buf1 = buf + buf0 + buf1; from specification array-splice[buffer]% ⊦ mkempbuf(0) + buf = buf; (s)% ⊦ mkbuf(0) + buf = buf; (s)% ⊦ # mkbuf(n) = n; (s)% ⊦ mapped(buf).data = buf; (s)% ⊦ m < # avol → avol[m, aleb][m] = aleb; (s)