Level: Lib Thy Top: 2
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

Conclusion:

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

Applied Tactic: RW (AddrC [2](RecUnfoldC `min_ar`)) 0 THEN SplitOnConclITE THENA Auto'
Generated subgoals:

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

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