Proof step 271 from proof inv-commit (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 272:

  # 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))

Rule argument

Additional information

Used simplifier rules: id-circle-subarray-concrete-below: n0 < n, n + m + m0 ≤ # avol ⊦ id○(avol, avol0, (* n0)) → subarray(avol, (* n) + m, m0) = subarray(avol0, n + m, m0);%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic% ⊦ mapped(buf).data = buf; (s)% ⊦ mapped(buf).mapped?; (s)%idexcept-size: ⊦ id○(avol, avol0, n) → # avol = # avol0; (forward) from specification array-copy[avolume]%⊦ is-encoded-pad(ns0, n, buf) → (is-encoded-pad(ns1, n, buf) ↔ ns0 = ns1); (s)%mult-c: ⊦ m * n = n * m; from specification nat-mult%mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult% ⊦ m ≤ m; (s)%0 ≠ m ⊦ (* m) * n ≤ m * n0 ↔ n ≤ n0; (s)% ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s)%n ≤ m ⊦ (m - n) + m0 ≤ n0 ↔ m + m0 ≤ n0 + n; (s)% ⊦ m ≤ n → (n < m ↔ false); (s)% ⊦ m ≤ n ↔ ¬ n < m; (ss)% ⊦ mksb(adr, m, m0, m1, m2, m3, m4).maxino = m; (s)% ⊦ mksb(adr, m, m0, m1, m2, m3, m4).indexaddr = adr; (s)%n < m0 ⊦ id○(avol1, avol0, n) → (mapped-full?(avol1, m0, m1) ↔ mapped-full?(avol0, m0, m1)); (s)% ⊦ mksb(adr, m, m0, m1, m2, m3, m4).lpt = m3; (s)% ⊦ LEB_SIZE ≠ 0; (s)% ⊦ mksb(adr, m, m0, m1, m2, m3, m4).log = m0; (s)% ⊦ mksb(adr, m, m0, m1, m2, m3, m4).orphsize = m2; (s)% ⊦ mksb(adr, m, m0, m1, m2, m3, m4).orph = m1; (s)% ⊦ mksb(adr, m, m0, m1, m2, m3, m4).main = m4; (s)%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ m + n = m + n0 ↔ n = n0; (s)% ⊦ SB_LPT = 5; (s)% ⊦ SB_ORPH = 3; (s)%⊦ disk-layout(mksb(adr0, m1, 1, m3, m4, m5, m6), # lpt) ↔ m3 = SB_ORPH ∧ m5 = SB_LPT ∧ m6 = SB_LPT + 2 * lptlebs(# lpt, LEB_SIZE); (s)