Proof step 12 from proof crash-neutral-write (previous step)

Heuristic conditional right split applied rule if right

And obtained the following new goals

• Proof step 13:

  avols[v][m2].mapped?, m2 < # avols[v], ebm-cons(avols0), 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 ⊆ avols0, avols[v][m2].mapped? → avols[v][m2].fill ≤ m1 ⊦ ⟨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⟩ (avols ⊆ avols0)

• Proof step 23:

  m2 < # avols[v], ebm-cons(avols0), 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 ⊆ avols0, avols[v][m2].mapped? → avols[v][m2].fill ≤ m1 ⊦ ⟨if n ≠ 0 then avols[v][m2] := unmapped⟩ (avols ⊆ avols0), avols[v][m2].mapped?

• Proof step 41:

  m2 < # avols[v], ebm-cons(avols0), 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 ⊆ avols0, avols[v][m2].mapped? → avols[v][m2].fill ≤ m1 ⊦ m2 < # avols[v] ∧ v ∈ avols

Rule argument

Additional information