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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 185:

  # apebs = n1 + vtblpnum1, # wlar0 = n1 + vtblpnum1, apebs[m4].vidhdr.sqn = valid-sqns(v, m1, apebs, vtblpnum1).max, recs[v × m1] = recovery-entry(m4, valid-sqns(v, m1, apebs, vtblpnum1).max), apebs[vtblpnum1] = mkpeb(aechdr(m), avidhdr(v, m1, m2, m3, checksum(buf1, m3)), buf1, m0, false), nx < vtblpnum1, m4 < vtblpnum1, m4 < n1 + vtblpnum1, bflipset-cons(bflipset, subarray(wlar0, 0, vtblpnum1)), indices-erasing(wlar0, nx), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aechdr(m), avidhdr(v, m1, m2, m3, checksum(buf1, m3)), buf1, m0, false)), unique-sqns(apebs), valid-eraseq(subarray(wlar0, 0, vtblpnum1), q), valid-eraseq-stronger(subarray(apebs, 0, vtblpnum1), q), valid-global-sqn(subarray(apebs, 0, vtblpnum1), sqnum), valid-peb(v, m1, apebs[m4]), valid-recs(subarray(apebs, 0, vtblpnum1), subarray(wlar0, 0, vtblpnum1), recs), valid-recs-sqns(apebs, recs), valid-wl(subarray(apebs, 0, vtblpnum1), subarray(wlar0, 0, vtblpnum1)), v × m1 ∈ recs, m3 ≤ datasize(buf1), valid-sqns(v, m1, apebs, vtblpnum1).max ≤ m2, m3 ≤ LEB_SIZE ⊦ m3 = 0, n1 = 0, dups(nx), m4 ∈ q, indices-erasing(wlar0[vtblpnum1, wl-entry(m, used)][m4, wl-entry(wlar0[m4].ec, erasing)], nx) ∧ valid-global-sqn(subarray(apebs, 0, vtblpnum1 + 1), max(sqnum, m2 + 1)) ∧ valid-eraseq-stronger(subarray(apebs, 0, vtblpnum1 + 1), q + eq-entry(m4, v × m1) ') ∧ valid-wl(subarray(apebs, 0, vtblpnum1 + 1), subarray(wlar0[vtblpnum1, wl-entry(m, used)][m4, wl-entry(wlar0[m4].ec, erasing)], 0, vtblpnum1 + 1)) ∧ valid-recs-sqns(apebs, recs[v × m1, recovery-entry(vtblpnum1, m2)])

Rule argument

Additional information

Used simplifier rules: lf-valid-recs-notin-eraseq: ⊦ v × m ∈ recs ∧ recs[v × m] = recovery-entry(n0, n1) ∧ valid-recs(apebs, wlar, recs) ∧ valid-eraseq(wlar, q) → ¬ n0 ∈ q;%lf-valid-recs-sqns-vidhdr: ⊦ v × m ∈ recs ∧ recs[v × m] = recovery-entry(n0, n1) ∧ valid-recs-sqns(apebs, recs) → apebs[n0].vidhdr.sqn = n1;%lf-valid-recs-in-apebs: m0 ≤ # apebs ⊦ v × m ∈ recs ∧ recs[v × m] = recovery-entry(n0, n1) ∧ valid-recs(subarray(apebs, 0, m0), subarray(wlar, 0, m0), recs) → n0 < m0;%lf-valid-recs-valid-peb: m0 ≤ # apebs, # apebs = # wlar ⊦ v × m ∈ recs ∧ recs[v × m] = recovery-entry(n0, n1) ∧ valid-recs(subarray(apebs, 0, m0), subarray(wlar, 0, m0), recs) ∧ valid-wl(subarray(apebs, 0, m0), subarray(wlar, 0, m0)) → valid-peb(v, m, apebs[n0]);%lf-valid-recs-max: m ≤ # apebs, # apebs = # wlar ⊦ valid-recs(subarray(apebs, 0, m), subarray(wlar, 0, m), recs) ∧ valid-recs-sqns(apebs, recs) ∧ valid-wl(subarray(apebs, 0, m), subarray(wlar, 0, m)) ∧ v × n ∈ recs ∧ recs[v × n] = recovery-entry(m0, m1) → m1 = valid-sqns(v, n, apebs, m).max;% ⊦ m < n → n ≠ 0; (s)%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%n < # wlar ⊦ bflipset-cons(bflipset, subarray(wlar, 0, n)) ∧ n0 < n → bflipset-cons (bflipset -- n0, subarray (wlar[n, wl-entry(m0, used)][n0, wl-entry(m1, erasing)], 0, n + 1)); (ss)%a: ⊦ (q + q0) + q1 = q + q0 + q1; from specification list[erasequeue-base]%m < # wlar ⊦ m1 < m ∧ valid-eraseq(subarray(wlar, 0, m), q) → valid-eraseq (subarray (wlar[m, wl-entry(m0, used)][m1, wl-entry(m2, erasing)], 0, m + 1), q + eq-entry(m1, lref) '); (ss)% ⊦ m + m0 ≤ m ↔ m0 = 0; (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic%m < # apebs, # wlar = # apebs ⊦ valid-recs(subarray(apebs, 0, m), subarray(wlar, 0, m), recs) ∧ apebs[m] = mkpeb(aehdr, avidhdr(v, n, m0, m1, m5), buf, m2, boolvar) ∧ v × n ∈ recs ∧ recs[v × n] = recovery-entry(m3, m4) → valid-recs (subarray(apebs, 0, m + 1), subarray (wlar[m, wl-entry(n0, used)][m3, wl-entry(n1, erasing)], 0, m + 1), recs[v × n, recovery-entry(m, m0)]); (ss)%m ≠ n ⊦ wlar[m, wle][n] = wlar[n]; (s)% ⊦ ¬ n < n; (s)% ⊦ m ≤ m + n; (s)% ⊦ ¬ m + n < m; (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 < m + n ↔ n ≠ 0; (s)