[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 62 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 = n3 + # buf1, LEB_SIZE = n0 + # buf4, avol1[m2] = mapped(buf1), avol0[m2] = mapped(buf4), n2 + (m0 ≤ m6 ⊃ 0;m0 - m6) < EB_PAGE_SIZE, m2 < # avol1, (m0 ≤ m6 ⊃ 0;m0 - m6) < EB_PAGE_SIZE, abs(avol1, buffered(m2), mkwbuf(buf2, m6, n2 + (m0 ≤ m6 ⊃ 0;m0 - m6)), avol0, rofs), 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, # buf1 ≤ LEB_SIZE, m6 ≤ 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, rofs → m6 ≤ # buf4, ¬ rofs → # buf4 = m6 ⊦ subarray(buf4 + mkempbuf(n0), 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(buf1 + mkempbuf(n3), m0, n1 + (m0 ≤ m6 ⊃ m6 - m0;0)) + subarray(buf3, n1 + (m0 ≤ m6 ⊃ m6 - m0;0), n5)

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 63:
⊦ abs(avol0, bleb, wbuf, avol1, rofs) ↔ # avol0 = # avol1 ∧ (∀ n. n < # avol0 → (buffered(n) ≠ bleb → avol0[n] = avol1[n]) ∧ (¬ rofs ∧ buffered(n) = bleb → avol0[n] = abs⊕(avol1[n], wbuf)) ∧ ( rofs ∧ buffered(n) = bleb → wbuf.offset = # avol1[n].data ∧ avol0[n] = abs⊕(avol1[n], wbuf) ∨ wbuf.offset < # avol1[n].data ∧ wbuf.offset + wbuf.nbytes < # avol1[n].data ∧ avol0[n] = avol1[n] ∧ subarray(wbuf.content, 0, wbuf.nbytes) = subarray(avol1[n].data, wbuf.offset, wbuf.nbytes)))
Proof step 64:
# 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, LEB_SIZE = n3 + # buf1, avol0[m2] = mapped(buf4), avol1[m2] = mapped(buf1), (m0 ≤ m6 ⊃ 0;m0 - m6) < EB_PAGE_SIZE, m2 < # avol1, n2 + (m0 ≤ m6 ⊃ 0;m0 - m6) < EB_PAGE_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, m6 ≤ LEB_SIZE, # buf1 ≤ LEB_SIZE, # buf4 ≤ LEB_SIZE, m6 ≤ m0 + n1 + (m0 ≤ m6 ⊃ m6 - m0;0), m0 ≤ m6 + n2 + (m0 ≤ m6 ⊃ 0;m0 - m6), min(n1, n2) ≤ n1 + n5, ¬ rofs → # buf4 = m6, rofs → m6 ≤ # buf4, ¬ m0 ≤ m6 → m6 ≤ m0, ∀ n. n < # avol1 → (buffered(n) ≠ buffered(m2) → avol1[n] = avol0[n]) ∧ (¬ rofs ∧ buffered(n) = buffered(m2) → avol1[n] = abs⊕(avol0[n], mkwbuf(buf2, m6, n2 + (m0 ≤ m6 ⊃ 0;m0 - m6)))) ∧ ( rofs ∧ buffered(n) = buffered(m2) → mkwbuf(buf2, m6, n2 + (m0 ≤ m6 ⊃ 0;m0 - m6)).offset = # avol0[n].data ∧ avol1[n] = abs⊕(avol0[n], mkwbuf(buf2, m6, n2 + (m0 ≤ m6 ⊃ 0;m0 - m6))) ∨ mkwbuf(buf2, m6, n2 + (m0 ≤ m6 ⊃ 0;m0 - m6)).offset < # avol0[n].data ∧ mkwbuf(buf2, m6, n2 + (m0 ≤ m6 ⊃ 0;m0 - m6)).offset + mkwbuf(buf2, m6, n2 + (m0 ≤ m6 ⊃ 0;m0 - m6)).nbytes < # avol0[n].data ∧ avol1[n] = avol0[n] ∧ subarray(mkwbuf(buf2, m6, n2 + (m0 ≤ m6 ⊃ 0;m0 - m6)).content, 0, mkwbuf(buf2, m6, n2 + (m0 ≤ m6 ⊃ 0;m0 - m6)).nbytes) = subarray(avol0[n].data, mkwbuf(buf2, m6, n2 + (m0 ≤ m6 ⊃ 0;m0 - m6)).offset, mkwbuf(buf2, m6, n2 + (m0 ≤ m6 ⊃ 0;m0 - m6)).nbytes)) ⊦ subarray(buf4 + mkempbuf(n0), 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(buf1 + mkempbuf(n3), m0, n1 + (m0 ≤ m6 ⊃ m6 - m0;0)) + subarray(buf3, n1 + (m0 ≤ m6 ⊃ m6 - m0;0), n5)

Rule argument

spec: wbuf-abs name: abs-def seq: ⊦ abs(avol0, bleb, wbuf, avol1, rofs) ↔ # avol0 = # avol1 ∧ (∀ n. n < # avol0 → (buffered(n) ≠ bleb → avol0[n] = avol1[n]) ∧ ( ¬ rofs ∧ buffered(n) = bleb → avol0[n] = abs⊕(avol1[n], wbuf)) ∧ ( rofs ∧ buffered(n) = bleb → wbuf.offset = # avol1[n].data ∧ avol0[n] = abs⊕(avol1[n], wbuf) ∨ wbuf.offset < # avol1[n].data ∧ wbuf.offset + wbuf.nbytes < # avol1[n].data ∧ avol0[n] = avol1[n] ∧ subarray(wbuf.content, 0, wbuf.nbytes) = subarray (avol1[n].data, wbuf.offset, wbuf.nbytes))) subst: [rofs, avol1, wbuf, bleb, avol0] → [rofs, avol0, mkwbuf(buf2, m6, n2 + (m0 ≤ m6 ⊃ 0;m0 - m6)), buffered(m2), avol1] flags: <all paths>

Additional information

Used terms: rofs, avol0, mkwbuf(buf2, m6, n2 + (m0 ≤ m6 ⊃ 0;m0 - m6)), buffered(m2), avol1