[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 113 from proof inv-format (previous step)

# lebs(avol0, 5, lptlebs(# lpt, LEB_SIZE)) = lptsize(# lpt, LEB_SIZE), # avol = # avol0, # avol0 = # lpt + 5 + 2 * lptlebs(# lpt, LEB_SIZE), avol0[0] = fill(mkavolume(# avol0), unmapped)[0], avol0[1] = mapped(mkbuf(0)), avol0[2] = fill(mkavolume(# avol0), unmapped)[2], avol0[3] = mapped(mkbuf(0)), avol0[4] = fill(mkavolume(# avol0), unmapped)[4], avol[0] = mapped(buf), ebm-vol-inv(avol), ebm-vol-inv(avol0), ebm-vol-inv(fill(mkavolume(# avol0), unmapped)[1, mapped(mkbuf(0))]), ebm-vol-inv(fill(mkavolume(# avol0), unmapped)), ebm-vol-inv(fill(mkavolume(# avol0), unmapped)[1, mapped(mkbuf(0))][3, mapped(mkbuf(0))]), id○(avol, avol0, 0), is-encoded(lpt, lebs(avol0, 5, lptlebs(# lpt, LEB_SIZE))), is-encoded(mksb(adr, m1, 1, 3, 0, 5, 5 + 2 * lptlebs(# lpt, LEB_SIZE)), buf), mapped-full?(avol0, 5, lptlebs(# lpt, LEB_SIZE)), range= (avol0, 5 + lptlebs(# lpt, LEB_SIZE), fill(mkavolume(# avol0), unmapped), 5 + lptlebs(# lpt, LEB_SIZE), lptlebs(# lpt, LEB_SIZE) + # lpt), 5 + lptlebs(# lpt, LEB_SIZE) ≤ # avol0, 5 ≤ # avol0, 5 + 2 * lptlebs(# lpt, LEB_SIZE) ≤ # avol0 ⊦ (∃ lpt0, log, orphans. 2 * lptlebs(# lpt, LEB_SIZE) = 2 * lptlebs(# lpt0, LEB_SIZE) ∧ (5 + 2 * lptlebs(# lpt, LEB_SIZE)) + # lpt0 = # avol0 ∧ avol[3].mapped? ∧ is-encoded-pad(orphans, 0, avol[3].data) ∧ avol[1].mapped? ∧ is-encoded(log, avol[1].data) ∧ mapped-full?(avol0, 5, lptlebs(# lpt0, LEB_SIZE)) ∧ is-encoded(lpt0, lebs(avol, 5, lptlebs(# lpt0, LEB_SIZE)))) ∧ subarray(fill(mkavolume(# avol0), unmapped), 5 + 2 * lptlebs(# lpt, LEB_SIZE), # lpt) = fill(mkavolume(# lpt), unmapped) ∧ avol[1].data = mkbuf(0) ∧ avol[3].data = mkbuf(0)

User applied rule cut formula

And obtained the following new goals

Proof step 114:
# avol0 = # lpt + 5 + 2 * lptlebs(# lpt, LEB_SIZE), # avol = # avol0, # lebs(avol0, 5, lptlebs(# lpt, LEB_SIZE)) = lptsize(# lpt, LEB_SIZE), avol[0] = mapped(buf), avol0[4] = fill(mkavolume(# avol0), unmapped)[4], avol0[3] = mapped(mkbuf(0)), avol0[2] = fill(mkavolume(# avol0), unmapped)[2], avol0[1] = mapped(mkbuf(0)), avol0[0] = fill(mkavolume(# avol0), unmapped)[0], avol[1] = mapped(mkbuf(0)), avol[3] = mapped(mkbuf(0)), ebm-vol-inv(fill(mkavolume(# avol0), unmapped)[1, mapped(mkbuf(0))][3, mapped(mkbuf(0))]), ebm-vol-inv(fill(mkavolume(# avol0), unmapped)), ebm-vol-inv(fill(mkavolume(# avol0), unmapped)[1, mapped(mkbuf(0))]), ebm-vol-inv(avol0), ebm-vol-inv(avol), id○(avol, avol0, 0), is-encoded(mksb(adr, m1, 1, 3, 0, 5, 5 + 2 * lptlebs(# lpt, LEB_SIZE)), buf), is-encoded(lpt, lebs(avol0, 5, lptlebs(# lpt, LEB_SIZE))), mapped-full?(avol0, 5, lptlebs(# lpt, LEB_SIZE)), range= (avol0, 5 + lptlebs(# lpt, LEB_SIZE), fill(mkavolume(# avol0), unmapped), 5 + lptlebs(# lpt, LEB_SIZE), lptlebs(# lpt, LEB_SIZE) + # lpt), 5 + 2 * lptlebs(# lpt, LEB_SIZE) ≤ # avol0, 5 ≤ # avol0, 5 + lptlebs(# lpt, LEB_SIZE) ≤ # avol0 ⊦ (∃ lpt0, log, orphans. 2 * lptlebs(# lpt, LEB_SIZE) = 2 * lptlebs(# lpt0, LEB_SIZE) ∧ (5 + 2 * lptlebs(# lpt, LEB_SIZE)) + # lpt0 = # avol0 ∧ avol[3].mapped? ∧ is-encoded-pad(orphans, 0, avol[3].data) ∧ avol[1].mapped? ∧ is-encoded(log, avol[1].data) ∧ mapped-full?(avol0, 5, lptlebs(# lpt0, LEB_SIZE)) ∧ is-encoded(lpt0, lebs(avol, 5, lptlebs(# lpt0, LEB_SIZE)))) ∧ subarray(fill(mkavolume(# avol0), unmapped), 5 + 2 * lptlebs(# lpt, LEB_SIZE), # lpt) = fill(mkavolume(# lpt), unmapped) ∧ avol[1].data = mkbuf(0) ∧ avol[3].data = mkbuf(0)
Proof step 123:
# avol0 = # lpt + 5 + 2 * lptlebs(# lpt, LEB_SIZE), # avol = # avol0, # lebs(avol0, 5, lptlebs(# lpt, LEB_SIZE)) = lptsize(# lpt, LEB_SIZE), avol[0] = mapped(buf), avol0[4] = fill(mkavolume(# avol0), unmapped)[4], avol0[3] = mapped(mkbuf(0)), avol0[2] = fill(mkavolume(# avol0), unmapped)[2], avol0[1] = mapped(mkbuf(0)), avol0[0] = fill(mkavolume(# avol0), unmapped)[0], ebm-vol-inv(fill(mkavolume(# avol0), unmapped)[1, mapped(mkbuf(0))][3, mapped(mkbuf(0))]), ebm-vol-inv(fill(mkavolume(# avol0), unmapped)), ebm-vol-inv(fill(mkavolume(# avol0), unmapped)[1, mapped(mkbuf(0))]), ebm-vol-inv(avol0), ebm-vol-inv(avol), id○(avol, avol0, 0), is-encoded(mksb(adr, m1, 1, 3, 0, 5, 5 + 2 * lptlebs(# lpt, LEB_SIZE)), buf), is-encoded(lpt, lebs(avol0, 5, lptlebs(# lpt, LEB_SIZE))), mapped-full?(avol0, 5, lptlebs(# lpt, LEB_SIZE)), range= (avol0, 5 + lptlebs(# lpt, LEB_SIZE), fill(mkavolume(# avol0), unmapped), 5 + lptlebs(# lpt, LEB_SIZE), lptlebs(# lpt, LEB_SIZE) + # lpt), 5 + 2 * lptlebs(# lpt, LEB_SIZE) ≤ # avol0, 5 ≤ # avol0, 5 + lptlebs(# lpt, LEB_SIZE) ≤ # avol0 ⊦ (∃ lpt0, log, orphans. 2 * lptlebs(# lpt, LEB_SIZE) = 2 * lptlebs(# lpt0, LEB_SIZE) ∧ (5 + 2 * lptlebs(# lpt, LEB_SIZE)) + # lpt0 = # avol0 ∧ avol[3].mapped? ∧ is-encoded-pad(orphans, 0, avol[3].data) ∧ avol[1].mapped? ∧ is-encoded(log, avol[1].data) ∧ mapped-full?(avol0, 5, lptlebs(# lpt0, LEB_SIZE)) ∧ is-encoded(lpt0, lebs(avol, 5, lptlebs(# lpt0, LEB_SIZE)))) ∧ subarray(fill(mkavolume(# avol0), unmapped), 5 + 2 * lptlebs(# lpt, LEB_SIZE), # lpt) = fill(mkavolume(# lpt), unmapped) ∧ avol[1].data = mkbuf(0) ∧ avol[3].data = mkbuf(0), avol[1] = mapped(mkbuf(0)) ∧ avol[3] = mapped(mkbuf(0))

Rule argument

fma: avol[1] = mapped(mkbuf(0)) ∧ avol[3] = mapped(mkbuf(0))

Additional information

Used formulas: avol[1] = mapped(mkbuf(0)) ∧ avol[3] = mapped(mkbuf(0))