Proof step 64 from proof inv-recover (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 65:

  # wlar1 = # wlar, # apebs0 = # wlar, apebs0[vtblpnum1] = mkpeb(aehdr, avhdr, buf1, m0, false), recs0[VTBL_VOLID × VTBL_LNUM] = recovery-entry(vtblpnum1, avhdr.sqn), vtblpnum1 < # wlar, nx < # wlar, bflipset-cons(bflipset, wlar), bflipset-cons(bflipset1, wlar1), bflipset-cons(bflipset0, wlar), indices-erasing(wlar, nx), ubi-io-inv(apebs0), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf1, m0, false)), unique-sqns(apebs0), valid-ebatbl(apebs0, wlar1, vols1, vtblpnum1), valid-eraseq(wlar, q), valid-eraseq(apebs0, q1), valid-eraseq(wlar1, q1), valid-eraseq(q1), valid-eraseq-stronger(apebs0, q), valid-global-sqn(apebs0, sqnum), valid-global-sqn(apebs0, vtblpnum5), valid-recs(apebs0, wlar, recs0), valid-recs-sqns(apebs0, recs0), valid-vtbl(apebs0, vols1, wlar1, vtblpnum1), valid-wl(apebs0, wlar), valid-wl(apebs0, wlar1), VTBL_VOLID × VTBL_LNUM ∈ recs0, ¬ dups(nx), ¬ vtblpnum1 ∈ q1, ¬ VTBL_VOLID ∈ vols1, ¬ vtblpnum1 ∈ q, err = ESUCCESS → vtbl = to-vtbl(vols1), err = ESUCCESS ∨ ⌊err⌋ ⊦ ⟪vols := ∅; if err = ESUCCESS then {ubi_init_vols_sizes#(recs0, wlar, apebs0; vtbl, vols); ubi_init_vols_mappings#(vtblpnum1, apebs0; recs0, vols, wlar, q, bflipset0); let n = 0 in ubi_fix_ecs#(n; nx, wlar)}⟫ ( ( err = ESUCCESS → # wlar1 = # wlar ∧ valid-wl(apebs0, wlar) ∧ valid-eraseq(q) ∧ valid-eraseq(wlar, q) ∧ valid-eraseq(apebs0, q) ∧ ¬ VTBL_VOLID ∈ vols ∧ bflipset-cons(bflipset0, wlar) ∧ valid-ebatbl(apebs0, wlar, vols, vtblpnum1) ∧ valid-vtbl(apebs0, vols, wlar, vtblpnum1)) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → is-max(apebs0, vols, wlar, q, bflipset0, vtblpnum1, sqnum) ∧ q.lebrefs ⊆ q1.lebrefs ∧ vols1 ⊆ vols ∧ vols⌈vols1, q1⌉))

Rule argument

Additional information