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

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

Conclusion:

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

Applied Tactic: Assert (j - 1) + i = (j + i) - 1 THENA Auto' THEN RWH (HypC 10) 8 THENA Auto' THEN Thin 10
Generated subgoals:

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