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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

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

Rule argument

Additional information

Used simplifier rules: rangeeq-till-leb5-fwd: m < 5 ⊦ range=(avol1, 0, avol0, 0, 5 + n) → avol1[(* m)] = avol0[m];%⊦ is-encoded-pad(ns0, n, buf) → (is-encoded-pad(ns1, n, buf) ↔ ns0 = ns1); (s)% ⊦ is-encoded(nx, mkbuf(0)) ↔ nx = []; (s)% ⊦ # mkbuf(n) = n; (s)% ⊦ mapped(buf).data = buf; (s)% ⊦ m < # avol → avol[m, aleb][m] = aleb; (s)% ⊦ mapped(buf).mapped?; (s)% ⊦ m < n → (n ≤ m ↔ false); (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%m ≠ n ⊦ avol[(* m), aleb][(* n)] = avol[n]; (s)% ⊦ # avol[n, aleb] = # avol; (s)% ⊦ mapped(buf) = mapped(buf0) ↔ buf = buf0; (s)%m < # avol ⊦ avol[m, aleb][m] = aleb; (s)% ⊦ m < n → n ≠ 0; (s)% ⊦ 0 < m ↔ m ≠ 0; (s)