Proof step 8 from proof at-fill-h (previous step)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 9:

  m < # ar, n < # ar, m0 ≤ n, ∀ n, ar, a, m0. n < # ar → fill(ar, a, m0, m)[n] = (m0 ≤ n ∧ n < m0 + m ⊃ a;ar[n]) ⊦ fill(ar, a, m0, m)[n] = a, n = m0 + m, m0 + m < n

• Proof step 11:

  m < # ar, n < # ar, ∀ n, ar, a, m0. n < # ar → fill(ar, a, m0, m)[n] = (m0 ≤ n ∧ n < m0 + m ⊃ a;ar[n]), ¬ m0 ≤ n ∨ m0 + m < n ⊦ fill(ar, a, m0, m)[n] = ar[n], n = m0 + m

Rule argument

Additional information