| adr0 = adr1, m0 = m1, plog0 = plog1, lpt0 = lpt1, avol0 ⊆ avol1, ns0 = ns1, abs(avol2, bleb0, wbuf, avol0, rofs0), bleb1 = bleb0, adr2 = adr1, m2 = m1, plog2 = plog1, lpt2 = lpt1, ns2 = ns1, rofs1 ↔ rofs0, awbuf-inv(avol2, bleb1), # lpt2 = # avol2, wbuf-cons(bleb0, wbuf, avol0, rofs0), m3 = EB_PAGE_SIZE, ebm-vol-inv(avol0), # lpt1 = # avol0, adr3 = adr4, m4 = m5, ns3 = ns4, log = plog3, lpt3 = lpt4 ⊦ ⟪wbuf_recover#(; adr3, m4, ns3, log, lpt3, wbuf0, m6, adr0, m0, plog0, avol1, lpt0, ns0, bleb2, rofs2; err)⟫ ( ( err = ESUCCESS → (∃ adr, m, plog, avol, lpt, ns, bleb, rofs. (adr = adr2 ∧ m = m2 ∧ plog = plog2 ∧ lpt = lpt2 ∧ avol ↓ avol2 ∧ ns = ns2) ∧ ⟨awbuf_recover#(; adr4, m5, ns4, plog3, lpt4, adr, m, plog, lpt, ns, avol; bleb, rofs, err0)⟩ ( ( abs(avol, bleb2, wbuf0, avol1, rofs2) ∧ bleb = bleb2 ∧ adr = adr0 ∧ m = m0 ∧ plog = plog0 ∧ lpt = lpt0 ∧ ns = ns0 ∧ (rofs ↔ rofs2)) ∧ adr3 = adr4 ∧ m4 = m5 ∧ ns3 = ns4 ∧ log = plog3 ∧ lpt3 = lpt4 ∧ err = err0))) ∧ ( err ≠ ESUCCESS → (∀ adr, m, plog, avol, lpt, ns, bleb, rofs. ⟨awbuf_recover#(; adr4, m5, ns4, plog3, lpt4, adr5, m7, plog4, lpt5, ns5, avol3; bleb3, rofs3, err0)⟩ ( adr = adr5 ∧ m = m7 ∧ plog = plog4 ∧ avol = avol3 ∧ lpt = lpt5 ∧ ns = ns5 ∧ bleb = bleb3 ∧ (rofs ↔ rofs3) ∧ adr3 = adr4 ∧ m4 = m5 ∧ ns3 = ns4 ∧ log = plog3 ∧ lpt3 = lpt4 ∧ err = err0)))) |