Proof step 68 from proof prepost-scan-all (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 69:

  # apebs = n0 + vtblpnum, # wlar = n0 + vtblpnum, apebs[vtblpnum] = mkpeb(aehdr0, avhdr0, buf0, m, false), nx < vtblpnum, bflipset-cons(bflipset, subarray(wlar, 0, vtblpnum)), indices-erasing(wlar, nx), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aehdr0, avhdr0, buf0, m, false)), unique-sqns(apebs), valid-eraseq(subarray(wlar, 0, vtblpnum), q), valid-eraseq-stronger(subarray(apebs, 0, vtblpnum), q), valid-global-sqn(subarray(apebs, 0, vtblpnum), sqnum), valid-recs(subarray(apebs, 0, vtblpnum), subarray(wlar, 0, vtblpnum), recs), valid-recs-sqns(apebs, recs), valid-wl(subarray(apebs, 0, vtblpnum), subarray(wlar, 0, vtblpnum)) ⊦ n0 = 0, aehdr0.valid?, dups(nx), valid-global-sqn(subarray(apebs, 0, vtblpnum + 1), sqnum) ∧ valid-eraseq-stronger(subarray(apebs, 0, vtblpnum + 1), q + eq-entry(vtblpnum, none) ') ∧ valid-wl(subarray(apebs, 0, vtblpnum + 1), subarray(wlar[vtblpnum, wl-entry(wlar[vtblpnum].ec, erasing)], 0, vtblpnum + 1))

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ n < n; (s)% ⊦ m + n < m + n0 ↔ n < n0; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).echdr = aehdr; (s)% ⊦ m < n + 1 ↔ ¬ n < m; (s)%m < # apebs, # wlar = # apebs, stat ≠ used ⊦ valid-recs(subarray(apebs, 0, m), subarray(wlar, 0, m), recs) → valid-recs (subarray(apebs, 0, m + 1), subarray(wlar[m, wl-entry(m0, stat)], 0, m + 1), recs); (ss)% ⊦ used ≠ erasing; (s)% ⊦ m < m + n ↔ n ≠ 0; (s)%n < # wlar ⊦ bflipset-cons(bflipset, subarray(wlar, 0, n)) → bflipset-cons(bflipset, subarray(wlar[n, wle], 0, n + 1)); (ss)%a: ⊦ (q + q0) + q1 = q + q0 + q1; from specification list[erasequeue-base]%m < # wlar ⊦ valid-eraseq(subarray(wlar, 0, m), q) → valid-eraseq (subarray(wlar[m, wl-entry(m0, erasing)], 0, m + 1), q + eq-entry(m, lref) '); (ss)% ⊦ m + m0 ≤ m ↔ m0 = 0; (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)%⊦ indices-erasing(wlar, nx) → indices-erasing(wlar[m, wl-entry(n, erasing)], nx); (ss)% ⊦ wl-entry(m, stat).status = stat; (s)% ⊦ m < # wlar → wlar[m, wle][m] = wle; (s)%⊦ indices-erasing(wlar, n ' + nx) ↔ n < # wlar ∧ wlar[n].status = erasing ∧ indices-erasing(wlar, nx); (s)% ⊦ nx < m → m ' + nx < m + 1; (ss)%a: ⊦ (nx + nx0) + nx1 = nx + nx0 + nx1; from specification list[nat-list-set]% ⊦ nx < m → ¬ m ∈ nx; (s)% ⊦ dups(n ' + nx) ↔ dups(nx) ∨ n ∈ nx; (ws)% ⊦ # wlar[n, wle] = # wlar; (s)%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ m + 1 ≤ n ↔ m < n; (s)% ⊦ ¬ ⌊ESUCCESS⌋ ; (s)