[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 143 from proof refine-read-buf (previous step)

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

User applied rule cut formula

And obtained the following new goals

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

Rule argument

fma: m0 ≤ m6

Additional information

Used formulas: m0 ≤ m6