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

# avol = # avol0, # lpt0 = # lpt, # lebs(avol, 5, lptlebs(# lpt, LEB_SIZE)) = lptsize(# lpt, LEB_SIZE), # avol2 = # avol0, (5 + 2 * lptlebs(# lpt, LEB_SIZE)) + # lpt = # avol0, avol[0] = mapped(buf2), avol[1] = mapped(mkbuf(0)), avol[2] = mapped(buf1), avol[3] = mapped(buf), avol[4] = mapped(buf0), avol0[0] = mapped(buf2), avol0[4] = mapped(buf0), avol0[2] = mapped(buf1), avol2[0] = mapped(buf3), 3 < # avol0, ebm-vol-inv(avol), ebm-vol-inv(avol0[1, mapped(mkbuf(0))]), ebm-vol-inv(avol0), ebm-vol-inv(avol0[1, mapped(mkbuf(0))][3, mapped(buf)]), ebm-vol-inv(avol2), id○(avol2, avol, 0), is-encoded(lpt, lebs(avol, 5, lptlebs(# lpt, LEB_SIZE))), is-encoded(log, buf1), is-encoded(lpt0, lebs(avol0, 5 + lptlebs(# lpt, LEB_SIZE), lptlebs(# lpt, LEB_SIZE))), is-encoded(mksb(adr0, m2, 2, 4, m6, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)), buf2), is-encoded(mksb(adr, m3, 1, 3, # orphans, 5, 5 + 2 * lptlebs(# lpt, LEB_SIZE)), buf3), is-encoded-pad(orphans0, m6, buf0), is-encoded-pad(orphans, # orphans, buf), mapped-full?(avol, 5, lptlebs(# lpt, LEB_SIZE)), mapped-full?(avol0, 5 + lptlebs(# lpt, LEB_SIZE), lptlebs(# lpt, LEB_SIZE)), range=(avol, 5 + lptlebs(# lpt, LEB_SIZE), avol0, 5 + lptlebs(# lpt, LEB_SIZE), lptlebs(# lpt, LEB_SIZE) + # lpt), 5 ≤ # avol0, 5 + lptlebs(# lpt, LEB_SIZE) ≤ # avol0, 5 + 2 * lptlebs(# lpt, LEB_SIZE) ≤ # avol0, logoff ≠ LEB_SIZE → # buf1 = logoff ⊦ (∃ lpt1, log0. 2 * lptlebs(# lpt, LEB_SIZE) = 2 * lptlebs(# lpt1, LEB_SIZE) ∧ (5 + 2 * lptlebs(# lpt, LEB_SIZE)) + # lpt1 = # avol0 ∧ avol2[3].mapped? ∧ avol2[1].mapped? ∧ # avol2[1].data = 0 ∧ is-encoded(log0, avol2[1].data) ∧ mapped-full?(avol, 5, lptlebs(# lpt1, LEB_SIZE)) ∧ is-encoded(lpt1, lebs(avol2, 5, lptlebs(# lpt1, LEB_SIZE)))) ∧ avol2[1].data = mkbuf(0) ∧ is-encoded(lpt, lebs(avol2, 5, lptlebs(# avol0 - 5 + 2 * lptlebs(# lpt, LEB_SIZE), LEB_SIZE))) ∧ is-encoded-pad(orphans, # orphans, avol2[3].data) ∧ subarray(avol, 5 + 2 * lptlebs(# lpt, LEB_SIZE), # avol0 - 5 + 2 * lptlebs(# lpt, LEB_SIZE)) = subarray(avol0, 5 + 2 * lptlebs(# lpt, LEB_SIZE), # avol0 - 5 + 2 * lptlebs(# lpt, LEB_SIZE))

Heuristic elimination applied rule insert elim lemma

And obtained the following new goals

Proof step 273:
# avol2 = # avol0, # lebs(avol, 5, lptlebs(# lpt, LEB_SIZE)) = lptsize(# lpt, LEB_SIZE), # lpt0 = # lpt, # avol = # avol0, # avol0 = n0 + 5 + 2 * lptlebs(# lpt, LEB_SIZE), (5 + 2 * lptlebs(# lpt, LEB_SIZE)) + # lpt = # avol0, avol2[0] = mapped(buf3), avol0[2] = mapped(buf1), avol0[4] = mapped(buf0), avol0[0] = mapped(buf2), avol[4] = mapped(buf0), avol[3] = mapped(buf), avol[2] = mapped(buf1), avol[1] = mapped(mkbuf(0)), avol[0] = mapped(buf2), 3 < # avol0, ebm-vol-inv(avol2), ebm-vol-inv(avol0[1, mapped(mkbuf(0))][3, mapped(buf)]), ebm-vol-inv(avol0), ebm-vol-inv(avol0[1, mapped(mkbuf(0))]), ebm-vol-inv(avol), id○(avol2, avol, 0), is-encoded(mksb(adr, m3, 1, 3, # orphans, 5, 5 + 2 * lptlebs(# lpt, LEB_SIZE)), buf3), is-encoded(mksb(adr0, m2, 2, 4, m6, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)), buf2), is-encoded(lpt0, lebs(avol0, 5 + lptlebs(# lpt, LEB_SIZE), lptlebs(# lpt, LEB_SIZE))), is-encoded(log, buf1), is-encoded(lpt, lebs(avol, 5, lptlebs(# lpt, LEB_SIZE))), is-encoded-pad(orphans, # orphans, buf), is-encoded-pad(orphans0, m6, buf0), mapped-full?(avol0, 5 + lptlebs(# lpt, LEB_SIZE), lptlebs(# lpt, LEB_SIZE)), mapped-full?(avol, 5, lptlebs(# lpt, LEB_SIZE)), range=(avol, 5 + lptlebs(# lpt, LEB_SIZE), avol0, 5 + lptlebs(# lpt, LEB_SIZE), lptlebs(# lpt, LEB_SIZE) + # lpt), 5 + 2 * lptlebs(# lpt, LEB_SIZE) ≤ # avol0, 5 + lptlebs(# lpt, LEB_SIZE) ≤ # avol0, 5 ≤ # avol0, logoff ≠ LEB_SIZE → # buf1 = logoff ⊦ (∃ lpt1, log0. 2 * lptlebs(# lpt, LEB_SIZE) = 2 * lptlebs(# lpt1, LEB_SIZE) ∧ (5 + 2 * lptlebs(# lpt, LEB_SIZE)) + # lpt1 = # avol0 ∧ avol2[3].mapped? ∧ avol2[1].mapped? ∧ # avol2[1].data = 0 ∧ is-encoded(log0, avol2[1].data) ∧ mapped-full?(avol, 5, lptlebs(# lpt1, LEB_SIZE)) ∧ is-encoded(lpt1, lebs(avol2, 5, lptlebs(# lpt1, LEB_SIZE)))) ∧ avol2[1].data = mkbuf(0) ∧ is-encoded(lpt, lebs(avol2, 5, lptlebs(n0, LEB_SIZE))) ∧ is-encoded-pad(orphans, # orphans, avol2[3].data) ∧ subarray(avol, 5 + 2 * lptlebs(# lpt, LEB_SIZE), n0) = subarray(avol0, 5 + 2 * lptlebs(# lpt, LEB_SIZE), n0)

Rule argument

spec: nat name: elim-sub seq: n ≤ m ⊦ n0 = m - n ↔ m = n0 + n subst: [n, m, n0] → [5 + 2 * lptlebs(# lpt, LEB_SIZE), # avol0, n]

Additional information

Used simplifier rules: n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: 5 + 2 * lptlebs(# lpt, LEB_SIZE), # avol0, n