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

Heuristic elimination applied rule insert elim lemma

And obtained the following new goals

• Proof step 31:

  # apebs = # wlar, # apebs = n0 + vtblpnum, vtblpnum < # wlar, nx < vtblpnum, bflipset-cons(bflipset, subarray(wlar, 0, vtblpnum)), indices-erasing(wlar, nx), ubi-io-inv(apebs), 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)), vtblpnum ≤ # apebs ⊦ ⟪aubi_io_isbad#(vtblpnum, apebs; ; isbad, err); vtblpnum0 := vtblpnum; if err = ESUCCESS then if isbad then wlar[vtblpnum0] := wl-entry(wlar[vtblpnum0].ec, erroneous) else let aehdr = ?, bitflips = ? in {aubi_io_read_echdr#(vtblpnum0, apebs; aehdr; bitflips, err); if err = ESUCCESS then if ¬ aehdr.valid? then {nx := vtblpnum0 ' + nx; wlar[vtblpnum0] := wl-entry(wlar[vtblpnum0].ec, erasing); q := q + eq-entry(vtblpnum0, none) '} else let avhdr = ? in {vtblpnum2 := vtblpnum2 + 1; vtblpnum1 := vtblpnum1 + aehdr.ec; wlar[vtblpnum0].ec := aehdr.ec; aubi_io_read_vidhdr#(vtblpnum0, apebs; avhdr; bitflips, err); if err = ESUCCESS then if avhdr = empty then if bitflips then {wlar[vtblpnum0] := wl-entry(wlar[vtblpnum0].ec, erasing); q := q + eq-entry(vtblpnum0, none) '} else wlar[vtblpnum0] := wl-entry(wlar[vtblpnum0].ec, free) else if avhdr.valid? then let buf = mkbuf(LEB_SIZE) in {if avhdr.size ≠ 0 then let boolvar = ? in {aubi_io_read_data#(vtblpnum0, 0, 0, LEB_SIZE, apebs; buf; boolvar, err); bitflips := bitflips ∨ boolvar}; if err = ESUCCESS then let ladr = avhdr.vol × avhdr.leb, n = 0 in {if ladr ∈ recs then n := recs[ladr].sqn; if avhdr.size ≠ 0 → avhdr.size ≤ datasize(buf) ∧ avhdr.checksum = checksum(buf, avhdr.size) then {sqnum := max(sqnum, avhdr.sqn + 1); if n ≤ avhdr.sqn then {wlar[vtblpnum0] := wl-entry(wlar[vtblpnum0].ec, used); if bitflips then bflipset := bflipset ++ vtblpnum0; if ladr ∈ recs then let vtblpnum = recs[ladr].pnum in {bflipset := bflipset -- vtblpnum; wlar[vtblpnum] := wl-entry(wlar[vtblpnum].ec, erasing); q := q + eq-entry(vtblpnum, avhdr.vol × avhdr.leb) '}; recs[ladr] := recovery-entry(vtblpnum0, avhdr.sqn)} else {wlar[vtblpnum0] := wl-entry(wlar[vtblpnum0].ec, erasing); q := q + eq-entry(vtblpnum0, ladr.vol × ladr.leb) '}} else {wlar[vtblpnum0] := wl-entry(wlar[vtblpnum0].ec, erasing); q := q + eq-entry(vtblpnum0, none) '}}} else {wlar[vtblpnum0] := wl-entry(wlar[vtblpnum0].ec, erasing); q := q + eq-entry(vtblpnum0, none) '}}}; vtblpnum0 := vtblpnum0 + 1⟫ ( vtblpnum0 ≤ # apebs ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err = ESUCCESS → # apebs = # wlar ∧ ¬ dups(nx) ∧ nx < vtblpnum0 ∧ indices-erasing(wlar, nx) ∧ valid-global-sqn(subarray(apebs, 0, vtblpnum0), sqnum) ∧ valid-eraseq(subarray(wlar, 0, vtblpnum0), q) ∧ bflipset-cons(bflipset, subarray(wlar, 0, vtblpnum0)) ∧ valid-eraseq-stronger(subarray(apebs, 0, vtblpnum0), q) ∧ valid-wl(subarray(apebs, 0, vtblpnum0), subarray(wlar, 0, vtblpnum0)) ∧ valid-recs-sqns(apebs, recs) ∧ valid-recs(subarray(apebs, 0, vtblpnum0), subarray(wlar, 0, vtblpnum0), recs)) ∧ # apebs < n0 + vtblpnum0), dups(nx)

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss)%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic%lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic%transitivity: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification oelem[nat-set]% ⊦ m < n → n ≠ 0; (s)% ⊦ m +1 = m + 1; (s)% ⊦ m < n → ¬ n < m; (s)%# apebs = n ⊦ subarray(apebs, 0, n) = apebs; (s)%# wlar = n ⊦ subarray(wlar, 0, n) = wlar; (s)% ⊦ ¬ m + n < m; (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic%n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: # apebs, vtblpnum, n0