Proof step 52 from proof inv-write (previous step)

Heuristic conditional right split applied rule if right

And obtained the following new goals

• Proof step 53:

  avols[v][m2].mapped?, m2 < # avols[v], ebm-cons(avols), is-aligned(n, EB_PAGE_SIZE), is-aligned(m1, EB_PAGE_SIZE), v ∈ avols, n + n2 ≤ # buf, m1 + n ≤ LEB_SIZE, avols[v][m2].mapped? → avols[v][m2].fill ≤ m1, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪choose n1 with n1 < n ∧ is-aligned(n1, EB_PAGE_SIZE) in if n1 ≠ 0 then avols[v][m2] := mapped(subarray(avols[v][m2].data, 0, m1) + subarray(buf, n2, n1) + mkempbuf(LEB_SIZE - m1 - n1), m1 + n1) ifnone skip⟫ ebm-cons(avols), err0 = ESUCCESS

• Proof step 78:

  m2 < # avols[v], ebm-cons(avols), is-aligned(n, EB_PAGE_SIZE), is-aligned(m1, EB_PAGE_SIZE), v ∈ avols, n + n2 ≤ # buf, m1 + n ≤ LEB_SIZE, avols[v][m2].mapped? → avols[v][m2].fill ≤ m1, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪if n ≠ 0 then avols[v][m2] := unmapped⟫ ebm-cons(avols), err0 = ESUCCESS, avols[v][m2].mapped?

• Proof step 81:

  m2 < # avols[v], ebm-cons(avols), is-aligned(n, EB_PAGE_SIZE), is-aligned(m1, EB_PAGE_SIZE), v ∈ avols, n + n2 ≤ # buf, m1 + n ≤ LEB_SIZE, avols[v][m2].mapped? → avols[v][m2].fill ≤ m1, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ err0 = ESUCCESS, m2 < # avols[v] ∧ v ∈ avols

Rule argument

Additional information