Proof step 19 from proof inv-remap (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  m5 + # lpt = # avol, avol[m1] = mapped(buf1), avol[m2] = mapped(buf0), avol[0] = mapped(buf), m6 < # lpt, disk-layout(mksb(adr, m0, m1, m2, m3, m4, m5), # lpt), ebm-vol-inv(avol[m5 + m6, mapped(mkbuf(0))]), ebm-vol-inv(avol), is-encoded(mksb(adr, m0, m1, 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 ⊦ ∃ lpt0, log0. m5 + # lpt0 = # avol ∧ avol[m5 + m6, mapped(mkbuf(0))][0].mapped? ∧ is-encoded(mksb(adr, m0, m1, m2, m3, m4, m5), avol[m5 + m6, mapped(mkbuf(0))][0].data) ∧ avol[m5 + m6, mapped(mkbuf(0))][m1].mapped? ∧ (logoff ≠ LEB_SIZE → # avol[m5 + m6, mapped(mkbuf(0))][m1].data = logoff) ∧ is-encoded(log0, avol[m5 + m6, mapped(mkbuf(0))][m1].data) ∧ mapped-full?(avol[m5 + m6, mapped(mkbuf(0))], m4, lptlebs(# lpt0, LEB_SIZE)) ∧ is-encoded(lpt0, lebs(avol[m5 + m6, mapped(mkbuf(0))], m4, lptlebs(# lpt0, LEB_SIZE)))

Rule argument

Additional information

Used simplifier rules: ⊦ is-encoded-pad(ns0, n, buf) → (is-encoded-pad(ns1, n, buf) ↔ ns0 = ns1); (s)% ⊦ mapped(buf).data = buf; (s)% ⊦ mapped(buf).mapped?; (s)%m ≠ n ⊦ avol[m, aleb][n] = avol[n]; (s)%⊦ disk-layout(mksb(adr, m0, m1, m2, m, m3, m4), mainareasize) → m4 + n ≠ m2; (s)%m = n ⊦ disk-layout(sb, m) → disk-layout(sb, n); (s)%eqs: ⊦ m = n + n0 ∧ m = n + n1 → n0 = n1; (forward) from specification nat-basic% ⊦ aleb.mapped? ↔ (∃ buf. aleb = mapped(buf)); (as)% ⊦ # avol[n, aleb] = # avol; (s)% ⊦ ¬ ⌊ESUCCESS⌋ ; (s)% ⊦ m = m0 + n0 ∧ n < n0 → m0 + n < m; (s)%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic