PrintForm Definitions choice 1 Sections AutomataTheory Doc

At: min ar alt


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

By:
UnivCD
THEN
NSubsetInd 4


Generated subgoals:

11. f:
2. n:
3. i: (n+1)
4. f(n-i) = f(n)
MinAr(f;0+i;n) = MinAr(f;0;n-i)+i
21. 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
MinAr(f;j+i;n) = MinAr(f;j;n-i)+i


About:
allfunctionboolnatural_numberadd
subtractimpliesequalapplyint