Proof step 4 from proof inv-add-log-leb (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  m5 + # lpt = # avol, avol[m0] = mapped(buf1), avol[m2] = mapped(buf0), avol[0] = mapped(buf), disk-layout(mksb(adr, m, m0, m2, m3, m4, m5), # lpt), ebm-vol-inv(avol), is-encoded(mksb(adr, m, m0, m2, m3, m4, m5), buf), is-encoded(lpt, lebs(avol, m4, lptlebs(# lpt, LEB_SIZE))), is-encoded(log, buf1), is-encoded-pad(orphans, m3, buf0), mapped-full?(avol, m4, lptlebs(# lpt, LEB_SIZE)), logoff ≠ LEB_SIZE → # buf1 = logoff ⊦ ⟪persistence_io_add_log_leb#(m1, mksb(adr, m, m0, m2, m3, m4, m5), EB_PAGE_SIZE, LEB_SIZE; logoff, avol; err)⟫ ( (∃ lpt0, log, orphans. disk-layout(mksb(adr, m, m0, m2, m3, m4, m5), # lpt0) ∧ m5 + # lpt0 = # avol ∧ avol[0].mapped? ∧ is-encoded(mksb(adr, m, m0, m2, m3, m4, m5), avol[0].data) ∧ avol[m2].mapped? ∧ is-encoded-pad(orphans, m3, avol[m2].data) ∧ avol[m0].mapped? ∧ (logoff ≠ LEB_SIZE → # avol[m0].data = logoff) ∧ is-encoded(log, avol[m0].data) ∧ mapped-full?(avol, m4, lptlebs(# lpt0, LEB_SIZE)) ∧ is-encoded(lpt0, lebs(avol, m4, lptlebs(# lpt0, LEB_SIZE)))) ∧ ebm-vol-inv(avol))

Rule argument

Additional information