| synced(avol), # lpt = # avol, abs(avol, bleb, wbuf, avol0, rofs), bleb0 = bleb, adr = adr0, m = m0, plog = plog0, lpt0 = lpt1, ns = ns0, rofs0 ↔ rofs, awbuf-inv(avol, bleb0), # lpt0 = # avol, wbuf-cons(bleb, wbuf, avol0, rofs), m1 = EB_PAGE_SIZE, ebm-vol-inv(avol0), # lpt1 = # avol0, ns1 = ns2, adr1 = adr2, m2 = m3 ⊦ ⟪wbuf_commit#(lpt, adr1, m2, avol0; ns1, adr0, m0, plog0, lpt1, ns0, rofs; err)⟫ ⟨awbuf_commit#(lpt, adr2, m3, avol, bleb0; ns2, adr, m, plog, lpt0, ns, rofs0; err0)⟩ ( (abs(avol, bleb, wbuf, avol0, rofs) ∧ bleb0 = bleb ∧ adr = adr0 ∧ m = m0 ∧ plog = plog0 ∧ lpt0 = lpt1 ∧ ns = ns0 ∧ (rofs0 ↔ rofs)) ∧ ns1 = ns2 ∧ err = err0) |