Proof step 4 from proof range-eq-splice-less (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 5:

  # ar0 < n0 + m1, range=(ar2, n2, splice(ar, n, ar0, n0, m0), n1, m1), n1 ≤ n0, n + m0 ≤ # ar, m1 ≤ m0 ⊦ m1 = 0, range=(ar2, n2, copy(ar, n, resize(ar0, n0 + m1), n0, m1), n1, m1)

• Proof step 41:

  # ar0 < n0 + m1, range=(ar2, n2, copy(ar, n, resize(ar0, n0 + m1), n0, m1), n1, m1), n1 ≤ n0, n + m0 ≤ # ar, m1 ≤ m0 ⊦ m1 = 0, range=(ar2, n2, splice(ar, n, ar0, n0, m0), n1, m1)

Rule argument

Additional information