Level: Lib Thy Top:
Hypotheses:None
Conclusion:
f:
. n:. i:(n + 1). f (n - MinAr(f;i;n)) = f n
Applied Tactic: UnivCD THENW Auto THEN NSubsetInd 3 THENA Auto' THEN RecCaseSplit `min_ar` THENA Auto' THEN Auto THE
N Assert
n - 0 = n
THENA Auto THEN RWH (HypC 4) 3 THENA Auto' THEN D 3 THEN Auto
Generated subgoals: