Proof step 3 from proof inv-map (previous step)

Heuristic nonrec nowhile calls applied rule call right

And obtained the following new goals

• Proof step 4:

  # apebs = # wlar, vols[v][vtblpnum1] = unmapped, vtblpnum0 = EB_PAGE_SIZE, vtblpnum1 < # vols[v], bflipset-cons(bflipset, wlar), ubi-io-inv(apebs), unique-sqns(apebs), valid-ebatbl(apebs, wlar, vols, vtblpnum), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-global-sqn(apebs, sqnum), valid-vtbl(apebs, vols, wlar, vtblpnum), valid-wl(apebs, wlar), v ∈ vols ⊦ ⟪if v ∈ vols ∧ vtblpnum1 < # vols[v] ∧ vols[v][vtblpnum1] = unmapped then let buf = mkbuf(0) in ubi_write#(v, vtblpnum1, 0, 0, 0, buf, vtblpnum0; vols, wlar, q, bflipset, vtblpnum, sqnum, apebs; err) else abort⟫ ( # apebs = # wlar ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, sqnum) ∧ valid-wl(apebs, wlar) ∧ valid-eraseq(q) ∧ valid-eraseq(wlar, q) ∧ valid-eraseq(apebs, q) ∧ ¬ VTBL_VOLID ∈ vols ∧ bflipset-cons(bflipset, wlar) ∧ valid-ebatbl(apebs, wlar, vols, vtblpnum) ∧ valid-vtbl(apebs, vols, wlar, vtblpnum) ∧ ubi-io-inv(apebs)), vtblpnum ∈ q, VTBL_VOLID ∈ vols

Rule argument

Additional information

Used simplifier rules: map: ⊦ ;