[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

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

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

User applied rule cut formula

And obtained the following new goals

Proof step 232:
# buf3 = n5 + n1 + (m0 ≤ # buf4 ⊃ # buf4 - m0;0), # buf2 = EB_PAGE_SIZE, # lpt0 = # avol1, # avol0 = # avol1, n1 + n5 = n4 + min(n1, n2), LEB_SIZE = (n3 + n2 + (m0 ≤ # buf4 ⊃ 0;m0 - # buf4)) + # buf4, avol1[m2] = mapped(buf4 + subarray(buf2, 0, n2 + (m0 ≤ # buf4 ⊃ 0;m0 - # buf4))), avol0[m2] = mapped(buf4), n2 + (m0 ≤ # buf4 ⊃ 0;m0 - # buf4) < EB_PAGE_SIZE, m2 < # avol1, (m0 ≤ # buf4 ⊃ 0;m0 - # buf4) < EB_PAGE_SIZE, awbuf-inv(avol1, buffered(m2)), ebm-vol-inv(avol0), is-aligned(# buf4, EB_PAGE_SIZE), min(n1, n2) ≤ n1 + n5, m0 ≤ # buf4 + n2 + (m0 ≤ # buf4 ⊃ 0;m0 - # buf4), # buf4 ≤ m0 + n1 + (m0 ≤ # buf4 ⊃ # buf4 - m0;0), # buf4 ≤ LEB_SIZE, (m0 ≤ # buf4 ⊃ # buf4 - m0;0) ≤ # buf3, (m0 ≤ # buf4 ⊃ 0;m0 - # buf4) + min(n1, n2) ≤ EB_PAGE_SIZE, m0 + n1 + (m0 ≤ # buf4 ⊃ # buf4 - m0;0) ≤ LEB_SIZE, m0 ≤ # buf4, ¬ m0 ≤ # buf4 → # buf4 ≤ m0 ⊦ subarray(buf4 + mkempbuf(n3 + n2 + (m0 ≤ # buf4 ⊃ 0;m0 - # buf4)), m0, (m0 ≤ # buf4 ⊃ # buf4 - m0;0)) + subarray(buf2, (m0 ≤ # buf4 ⊃ 0;m0 - # buf4), min(n1, n2)) + subarray ( subarray(buf4 + mkempbuf(n3 + n2 + (m0 ≤ # buf4 ⊃ 0;m0 - # buf4)), m0, n1 + (m0 ≤ # buf4 ⊃ # buf4 - m0;0)) + subarray(buf3, n1 + (m0 ≤ # buf4 ⊃ # buf4 - m0;0), n5), (m0 ≤ # buf4 ⊃ # buf4 - m0;0) + min(n1, n2), n4) = subarray((buf4 + subarray(buf2, 0, n2 + (m0 ≤ # buf4 ⊃ 0;m0 - # buf4))) + mkempbuf(n3), m0, n1 + (m0 ≤ # buf4 ⊃ # buf4 - m0;0)) + subarray(buf3, n1 + (m0 ≤ # buf4 ⊃ # buf4 - m0;0), n5)
Proof step 270:
# buf3 = n5 + n1 + (m0 ≤ # buf4 ⊃ # buf4 - m0;0), # buf2 = EB_PAGE_SIZE, # lpt0 = # avol1, # avol0 = # avol1, n1 + n5 = n4 + min(n1, n2), LEB_SIZE = (n3 + n2 + (m0 ≤ # buf4 ⊃ 0;m0 - # buf4)) + # buf4, avol1[m2] = mapped(buf4 + subarray(buf2, 0, n2 + (m0 ≤ # buf4 ⊃ 0;m0 - # buf4))), avol0[m2] = mapped(buf4), n2 + (m0 ≤ # buf4 ⊃ 0;m0 - # buf4) < EB_PAGE_SIZE, m2 < # avol1, (m0 ≤ # buf4 ⊃ 0;m0 - # buf4) < EB_PAGE_SIZE, awbuf-inv(avol1, buffered(m2)), ebm-vol-inv(avol0), is-aligned(# buf4, EB_PAGE_SIZE), min(n1, n2) ≤ n1 + n5, m0 ≤ # buf4 + n2 + (m0 ≤ # buf4 ⊃ 0;m0 - # buf4), # buf4 ≤ m0 + n1 + (m0 ≤ # buf4 ⊃ # buf4 - m0;0), # buf4 ≤ LEB_SIZE, (m0 ≤ # buf4 ⊃ # buf4 - m0;0) ≤ # buf3, (m0 ≤ # buf4 ⊃ 0;m0 - # buf4) + min(n1, n2) ≤ EB_PAGE_SIZE, m0 + n1 + (m0 ≤ # buf4 ⊃ # buf4 - m0;0) ≤ LEB_SIZE, ¬ m0 ≤ # buf4 → # buf4 ≤ m0 ⊦ subarray(buf4 + mkempbuf(n3 + n2 + (m0 ≤ # buf4 ⊃ 0;m0 - # buf4)), m0, (m0 ≤ # buf4 ⊃ # buf4 - m0;0)) + subarray(buf2, (m0 ≤ # buf4 ⊃ 0;m0 - # buf4), min(n1, n2)) + subarray ( subarray(buf4 + mkempbuf(n3 + n2 + (m0 ≤ # buf4 ⊃ 0;m0 - # buf4)), m0, n1 + (m0 ≤ # buf4 ⊃ # buf4 - m0;0)) + subarray(buf3, n1 + (m0 ≤ # buf4 ⊃ # buf4 - m0;0), n5), (m0 ≤ # buf4 ⊃ # buf4 - m0;0) + min(n1, n2), n4) = subarray((buf4 + subarray(buf2, 0, n2 + (m0 ≤ # buf4 ⊃ 0;m0 - # buf4))) + mkempbuf(n3), m0, n1 + (m0 ≤ # buf4 ⊃ # buf4 - m0;0)) + subarray(buf3, n1 + (m0 ≤ # buf4 ⊃ # buf4 - m0;0), n5), m0 ≤ # buf4

Rule argument

fma: m0 ≤ # buf4

Additional information

Used formulas: m0 ≤ # buf4