Proof step 20 from proof prepost-write-once (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  # apebs1 = # wlar0, # apebs0 = # wlar, q0.head = eq-entry(m4, lref), wlar0[vtblpnum].status = free, LEB_SIZE = (n1 + m0) + m1, vols0[v][m] = unmapped, vtblpnum < # wlar0, m < # vols0[v], bflipset-cons(bflipset, wlar0), bflipset-cons(bflipset, wlar), id(apebs1, apebs0, mapped-pebs(vols0)), is-aligned(m0, EB_PAGE_SIZE), is-aligned(m1, EB_PAGE_SIZE), ubi-io-inv(apebs0), ubi-io-inv(apebs1), unique-sqns(apebs1), unique-sqns(apebs0), valid-ebatbl(apebs1, wlar0, vols0, vtblpnum2), valid-ebatbl(apebs0, wlar, vols0, vtblpnum2), valid-eraseq(apebs1, q1), valid-eraseq(wlar0, q1), valid-eraseq(q1), valid-eraseq(q0), valid-eraseq(wlar, q0), valid-eraseq(apebs0, q0), valid-global-sqn(apebs1, sqnum), valid-global-sqn(apebs0, sqnum), valid-vtbl(apebs1, vols0, wlar0, vtblpnum2), valid-vtbl(apebs0, vols0, wlar, vtblpnum2), valid-wl(apebs1, wlar0), valid-wl(apebs0, wlar), v ∈ vols0, m0 + m1 ≤ LEB_SIZE, m1 + m2 ≤ # buf, m1 ≤ LEB_SIZE, q1.lebrefs ⊆ q0.lebrefs, ¬ vtblpnum2 ∈ q1, ¬ VTBL_VOLID ∈ vols0, ¬ vtblpnum2 ∈ q0, apebs0 = apebs1 ∧ wlar = wlar0 ∧ q0 = q1 ∨ id○(apebs0, apebs1, vtblpnum) ∧ id○(wlar, wlar0, vtblpnum) ∧ q0 = eq-entry(vtblpnum, lref) ' + q1 ⊦ ⟪ubi_next_sqnum#(; sqnum; m3); aubi_io_write_vidhdr#(vtblpnum, avidhdr(v, m, m3, 0, 0); apebs1; err); vols := vols0; if err = ESUCCESS then {if m1 ≠ 0 then aubi_io_write_data#(vtblpnum, m0, m2, m1, buf; apebs1; err); if err = ESUCCESS then {vols[v][m] := ⌜vtblpnum⌝ ; wlar0[vtblpnum] := wl-entry(wlar0[vtblpnum].ec, used)} else ubi_wl_put_peb#(v × m, vtblpnum; wlar0, q1); skip} else ubi_wl_put_peb#(none, vtblpnum; wlar0, q1)⟫ ( # apebs1 = # wlar0 ∧ unique-sqns(apebs1) ∧ valid-global-sqn(apebs1, sqnum) ∧ valid-wl(apebs1, wlar0) ∧ valid-eraseq(q1) ∧ valid-eraseq(wlar0, q1) ∧ valid-eraseq(apebs1, q1) ∧ ¬ VTBL_VOLID ∈ vols ∧ bflipset-cons(bflipset, wlar0) ∧ valid-ebatbl(apebs1, wlar0, vols, vtblpnum2) ∧ valid-vtbl(apebs1, vols, wlar0, vtblpnum2) ∧ ubi-io-inv(apebs1) ∧ id(apebs1, apebs0, mapped-pebs(vols0)) ∧ q1.lebrefs ⊆ q0.lebrefs ++ (v × m) ∧ (m1 = 0 → q1.lebrefs ⊆ q0.lebrefs) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err ≠ ESUCCESS → vols = vols0) ∧ ( err = ESUCCESS → (∃ n. vols = vols0[v, vols0[v][m, ⌜n⌝ ]] ∧ (m1 ≠ 0 → apebs1[n].fill = m0 + m1) ∧ (m1 = 0 → apebs1[n].fill = 0) ∧ apebs1[n].data = mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n1))))

Rule argument

Additional information

Used simplifier rules: lf-vtbl-info: ⊦ valid-vtbl(apebs, vols, wlar, n) ∧ valid-eraseq(wlar, q) → ¬ n ∈ q;% ⊦ m < n → n ≠ 0; (s)%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic