| # avol0 = # avol2, # lpt1 = # avol2, # buf = EB_PAGE_SIZE, err = err1, abs(avol2, bleb0, mkwbuf(buf, m2, m3), avol0, rofs0), awbuf-inv(avol2, bleb0), ebm-vol-inv(avol0), avol0 ⊆ avol1, ⌊err1⌋ , bleb0 ≠ nobuffer → bleb0.leb < # avol2 ∧ wbuf-cons(mkwbuf(buf, m2, m3), avol0[bleb0.leb], rofs0) ⊦ ⟨avol := ?, bleb := ?, rofs := ?, adr := ?, m := ?, plog := ?, lpt := ?, adr0 := ?, m0 := ?, log := ?, lpt0 := ?, ns0 := ?, ns := ?⟩ ( adr1 = adr ∧ m1 = m ∧ plog0 = plog ∧ avol4 = avol ∧ lpt2 = lpt ∧ ns1 = ns ∧ bleb1 = bleb ∧ (rofs1 ↔ rofs) ∧ adr2 = adr0 ∧ m4 = m0 ∧ ns2 = ns0 ∧ log0 = log ∧ lpt3 = lpt0 ∧ err1 = err) |