Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

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

Applied Tactic: UnivCD THENA Auto THEN NSubsetInd 4 THENA Auto'
Generated subgoals:

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

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