Level: Lib Thy Top: 2 1
Hypotheses:

  1. f :

  2. n :

  3. i : (n + 1)

  4. f (n - i) = f n

  5. j :

  6. 0 < j

  7. j < (n - i) + 1

  8. MinAr(f;(j - 1) + i;n) = MinAr(f;j - 1;n - i) + i

  9. f (n - (j + i)) = f n

Conclusion:

j + i = MinAr(f;j;n - i) + i

Applied Tactic: RecCaseSplit `min_ar` THENA Auto'
Generated subgoals:

1. j + i = j + i

2. j + i = MinAr(f;j - 1;n - i) + i