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

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 7:

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

• Proof step 9:

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

Rule argument

Additional information