Proof step 7 from proof suffix-upper-bound-reduce (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 8:

  ∀ n. n ≤ # ar → sum(ar, n, # ar - n) ≤ i, ∀ n. n ≤ # ar0 → sum(ar0, n, # ar0 - n) ≤ i0 ⊦ ∀ n. (n ≤ # ar → sum(ar, n, # ar - n) ≤ i) → n ≤ # ar0 → sum(ar0, n, # ar0 - n) ≤ i0

• Proof step 12:

  ∀ n. n ≤ # ar → sum(ar, n, # ar - n) ≤ i, ∀ n. (n ≤ # ar → sum(ar, n, # ar - n) ≤ i) → n ≤ # ar0 → sum(ar0, n, # ar0 - n) ≤ i0 ⊦ ∀ n. n ≤ # ar0 → sum(ar0, n, # ar0 - n) ≤ i0

Rule argument

Additional information