[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

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

m5 + # lpt = # avol, avol[0] = mapped(buf), avol[m2] = mapped(buf0), avol[m0] = mapped(buf1), subarray(avol0, m5, # lpt) = subarray(avol, m5, # lpt), disk-layout(mksb(adr, m, m0, m2, m3, m4, m5), # lpt), ebm-vol-inv(avol0), 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)), err = ESUCCESS → # avol = # avol0 ∧ avol0[0].mapped? ∧ is-encoded(mksb(adr, m, m0, m2, m3, m4, m5), avol0[0].data) ∧ avol0[m2].mapped? ∧ is-encoded-pad(orphans, m3, avol0[m2].data) ∧ avol0[m0].mapped? ∧ (logoff0 ≠ LEB_SIZE → # avol0[m0].data = logoff0) ∧ is-encoded(log + m1 ', avol0[m0].data) ∧ mapped-full?(avol0, m4, lptlebs(# lpt, LEB_SIZE)) ∧ is-encoded(lpt, lebs(avol0, m4, lptlebs(# lpt, LEB_SIZE))), err ≠ ESUCCESS → # avol = # avol0 ∧ avol0[0].mapped? ∧ is-encoded(mksb(adr, m, m0, m2, m3, m4, m5), avol0[0].data) ∧ avol0[m2].mapped? ∧ is-encoded-pad(orphans, m3, avol0[m2].data) ∧ avol0[m0].mapped? ∧ (logoff0 ≠ LEB_SIZE → # avol0[m0].data = logoff0) ∧ is-encoded(log, avol0[m0].data) ∧ mapped-full?(avol0, m4, lptlebs(# lpt, LEB_SIZE)) ∧ is-encoded(lpt, lebs(avol0, m4, lptlebs(# lpt, LEB_SIZE))), logoff ≠ LEB_SIZE → # buf1 = logoff, err = ESUCCESS ∨ ⌊err⌋ ⊦ ∃ lpt0, log, orphans. disk-layout(mksb(adr, m, m0, m2, m3, m4, m5), # lpt0) ∧ m5 + # lpt0 = # avol0 ∧ avol0[0].mapped? ∧ is-encoded(mksb(adr, m, m0, m2, m3, m4, m5), avol0[0].data) ∧ avol0[m2].mapped? ∧ is-encoded-pad(orphans, m3, avol0[m2].data) ∧ avol0[m0].mapped? ∧ (logoff0 ≠ LEB_SIZE → # avol0[m0].data = logoff0) ∧ is-encoded(log, avol0[m0].data) ∧ mapped-full?(avol0, m4, lptlebs(# lpt0, LEB_SIZE)) ∧ is-encoded(lpt0, lebs(avol0, m4, lptlebs(# lpt0, LEB_SIZE)))

User applied rule case distinction

And obtained the following new goals

Proof step 11:
m5 + # lpt = # avol, avol[m0] = mapped(buf1), avol[m2] = mapped(buf0), avol[0] = mapped(buf), subarray(avol0, m5, # lpt) = subarray(avol, m5, # lpt), disk-layout(mksb(adr, m, m0, m2, m3, m4, m5), # lpt), ebm-vol-inv(avol), ebm-vol-inv(avol0), is-encoded(log, buf1), is-encoded(lpt, lebs(avol, m4, lptlebs(# lpt, LEB_SIZE))), is-encoded(mksb(adr, m, m0, m2, m3, m4, m5), buf), is-encoded-pad(orphans, m3, buf0), mapped-full?(avol, m4, lptlebs(# lpt, LEB_SIZE)), logoff ≠ LEB_SIZE → # buf1 = logoff, err ≠ ESUCCESS → # avol = # avol0 ∧ avol0[0].mapped? ∧ is-encoded(mksb(adr, m, m0, m2, m3, m4, m5), avol0[0].data) ∧ avol0[m2].mapped? ∧ is-encoded-pad(orphans, m3, avol0[m2].data) ∧ avol0[m0].mapped? ∧ (logoff0 ≠ LEB_SIZE → # avol0[m0].data = logoff0) ∧ is-encoded(log, avol0[m0].data) ∧ mapped-full?(avol0, m4, lptlebs(# lpt, LEB_SIZE)) ∧ is-encoded(lpt, lebs(avol0, m4, lptlebs(# lpt, LEB_SIZE))), err = ESUCCESS ∨ ⌊err⌋ ⊦ err = ESUCCESS, ∃ lpt0, log, orphans. disk-layout(mksb(adr, m, m0, m2, m3, m4, m5), # lpt0) ∧ m5 + # lpt0 = # avol0 ∧ avol0[0].mapped? ∧ is-encoded(mksb(adr, m, m0, m2, m3, m4, m5), avol0[0].data) ∧ avol0[m2].mapped? ∧ is-encoded-pad(orphans, m3, avol0[m2].data) ∧ avol0[m0].mapped? ∧ (logoff0 ≠ LEB_SIZE → # avol0[m0].data = logoff0) ∧ is-encoded(log, avol0[m0].data) ∧ mapped-full?(avol0, m4, lptlebs(# lpt0, LEB_SIZE)) ∧ is-encoded(lpt0, lebs(avol0, m4, lptlebs(# lpt0, LEB_SIZE)))
Proof step 13:
# avol = # avol0, m5 + # lpt = # avol, avol[m0] = mapped(buf1), avol[m2] = mapped(buf0), avol[0] = mapped(buf), subarray(avol0, m5, # lpt) = subarray(avol, m5, # lpt), avol0[0].mapped?, avol0[m2].mapped?, avol0[m0].mapped?, disk-layout(mksb(adr, m, m0, m2, m3, m4, m5), # lpt), ebm-vol-inv(avol), ebm-vol-inv(avol0), is-encoded(log, buf1), is-encoded(lpt, lebs(avol, m4, lptlebs(# lpt, LEB_SIZE))), is-encoded(mksb(adr, m, m0, m2, m3, m4, m5), buf), is-encoded(mksb(adr, m, m0, m2, m3, m4, m5), avol0[0].data), is-encoded(log + m1 ', avol0[m0].data), is-encoded(lpt, lebs(avol0, m4, lptlebs(# lpt, LEB_SIZE))), is-encoded-pad(orphans, m3, buf0), is-encoded-pad(orphans, m3, avol0[m2].data), mapped-full?(avol, m4, lptlebs(# lpt, LEB_SIZE)), mapped-full?(avol0, m4, lptlebs(# lpt, LEB_SIZE)), logoff ≠ LEB_SIZE → # buf1 = logoff, err ≠ ESUCCESS → # avol = # avol0 ∧ avol0[0].mapped? ∧ is-encoded(mksb(adr, m, m0, m2, m3, m4, m5), avol0[0].data) ∧ avol0[m2].mapped? ∧ is-encoded-pad(orphans, m3, avol0[m2].data) ∧ avol0[m0].mapped? ∧ (logoff0 ≠ LEB_SIZE → # avol0[m0].data = logoff0) ∧ is-encoded(log, avol0[m0].data) ∧ mapped-full?(avol0, m4, lptlebs(# lpt, LEB_SIZE)) ∧ is-encoded(lpt, lebs(avol0, m4, lptlebs(# lpt, LEB_SIZE))), logoff0 ≠ LEB_SIZE → # avol0[m0].data = logoff0, err = ESUCCESS ∨ ⌊err⌋ ⊦ ∃ lpt0, log, orphans. disk-layout(mksb(adr, m, m0, m2, m3, m4, m5), # lpt0) ∧ m5 + # lpt0 = # avol0 ∧ avol0[0].mapped? ∧ is-encoded(mksb(adr, m, m0, m2, m3, m4, m5), avol0[0].data) ∧ avol0[m2].mapped? ∧ is-encoded-pad(orphans, m3, avol0[m2].data) ∧ avol0[m0].mapped? ∧ (logoff0 ≠ LEB_SIZE → # avol0[m0].data = logoff0) ∧ is-encoded(log, avol0[m0].data) ∧ mapped-full?(avol0, m4, lptlebs(# lpt0, LEB_SIZE)) ∧ is-encoded(lpt0, lebs(avol0, m4, lptlebs(# lpt0, LEB_SIZE)))

Rule argument

pos: left 14

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

User applied rule case distinction

And obtained the following new goals

Rule argument

Additional information