| bleb = buffered(m) ∨ (bleb = nobuffer ∨ is-aligned(# avol[bleb.leb].data, EB_PAGE_SIZE)) ∧ m < # avol ∧ avol[m].mapped? ∧ m0 = # avol[m].data, awbuf-inv(avol, bleb), # lpt = # avol, synced(avol0), adr = adr0, m1 = m2, nx = nx0, lpt0 = lpt, avol0 ↓ avol, ns = ns0 ⊦ ⟨awbuf_move_buf#(m, m0, adr0, m2, nx0, avol, lpt, ns0, isbuf; bleb; err)⟩ (synced(avol0) ∧ adr = adr0 ∧ m1 = m2 ∧ nx = nx0 ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns = ns0) |