Proof step 108 from proof refine-read-buf (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 109:

  # buf3 = n5 + n1, # avol0 = # avol1, # lpt0 = # avol1, # buf2 = EB_PAGE_SIZE, n1 + n5 = n4 + min(n1, n2), m0 + n3 + n2 = LEB_SIZE, avol0[m2] = mapped(buf4), avol1[m2] = mapped(buf4 + subarray(buf2, 0, n2 + (m0 - # buf4))), # buf4 < m0, m0 < EB_PAGE_SIZE + # buf4, m2 < # avol1, n2 + (m0 - # buf4) < EB_PAGE_SIZE, awbuf-inv(avol1, buffered(m2)), ebm-vol-inv(avol0), is-aligned(# buf4, EB_PAGE_SIZE), n1 ≤ n2 + n3, m0 + min(n1, n2) ≤ EB_PAGE_SIZE + # buf4, # buf4 ≤ LEB_SIZE, # buf4 ≤ m0 + n1, min(n1, n2) ≤ n1 + n5 ⊦ subarray(buf2, m0 - # buf4, min(n1, n2)) + subarray(mkempbuf(n1) + subarray(buf3, n1, n5), min(n1, n2), n4) = subarray(subarray(buf2, 0, n2 + (m0 - # buf4)) + mkempbuf(n3), m0 - # buf4, n1) + subarray(buf3, n1, n5), EB_PAGE_SIZE = 1

Rule argument

Additional information

Used simplifier rules: nat0: ⊦ n0 = n1 + n → (n1 + m ≤ n0 ↔ m ≤ n);% ⊦ m < m + n ↔ n ≠ 0; (s)% ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s)% ⊦ m + n < m + n0 ↔ n < n0; (s)% ⊦ m +1 = m + 1; (s)% ⊦ EB_PAGE_SIZE + n = 0 ↔ false; (s)% ⊦ m < n → n ≠ 0; (s)%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]%lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s)%n ≤ m ⊦ (m - n) + m0 ≤ n0 ↔ m + m0 ≤ n0 + n; (s)% ⊦ # subarray(buf, m, n) = n; (s)% ⊦ #(buf + buf0) = # buf + # buf0; (s)% ⊦ mkempbuf(0) + buf = buf; (s)% ⊦ m < n → (n ≤ m ↔ false); (s)% ⊦ m0 + m1 < n → min(n, m0) = m0; (s)% ⊦ m ≤ n → (n < m ↔ false); (s)% ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s)%n2 ≤ n1 ⊦ subarray(mkempbuf(n0 + n1), n0, n2) = mkempbuf(n2); (s)%# buf ≤ n0, n0 + m ≤ # buf + # buf0 ⊦ subarray(buf + buf0, n0, m) = subarray(buf0, n0 - # buf, m); (s)% ⊦ 0 ≤ m; (s)% ⊦ n ≤ n0 → (m + (n0 - n)) + n = m + n0; (s)% ⊦ # mkempbuf(n) = n; (s)% ⊦ m + n = m + n0 ↔ n = n0; (s)%n ≤ m ⊦ (m - n) + n0 = n1 ↔ m + n0 = n + n1; (s)% ⊦ EB_PAGE_SIZE ≠ 0; (s)% ⊦ 0 < m ↔ m ≠ 0; (s)% ⊦ m ≤ m + n; (s)% ⊦ n < m → (m - n) + n = m; (s)%append-a: ⊦ (buf + buf0) + buf1 = buf + buf0 + buf1; from specification array-splice[buffer]%c: ⊦ m + n = n + m; from specification nat-basic% ⊦ n + 0 = n; (s)% ⊦ m < n → m ≤ n; (s)% ⊦ m ≤ n ↔ ¬ n < m; (ss)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic