| m < # avol, avol[m].mapped?, m0 = # avol[m].data, synced(avol), abs(avol, bleb, wbuf, avol0, rofs), bleb0 = bleb, adr = adr0, m1 = m2, plog = plog0, lpt = lpt0, ns = ns0, rofs0 ↔ rofs, awbuf-inv(avol, bleb0), # lpt = # avol, wbuf-cons(bleb, wbuf, avol0, rofs), m3 = EB_PAGE_SIZE, ebm-vol-inv(avol0), # lpt0 = # avol0 ⊦ ⟪wbuf_add_log_leb#(m, m0, rofs, adr0, m2, avol0, lpt0, ns0; bleb, wbuf, plog0; err)⟫ ⟨awbuf_add_log_leb#(m, m0, adr, m1, avol, lpt, ns, rofs0; plog, bleb0; err0)⟩ ( (abs(avol, bleb, wbuf, avol0, rofs) ∧ bleb0 = bleb ∧ adr = adr0 ∧ m1 = m2 ∧ plog = plog0 ∧ lpt = lpt0 ∧ ns = ns0 ∧ (rofs0 ↔ rofs)) ∧ err = err0) |