Nuprl - Pf min_ar

PrintForm Definitions choice 1 Sections AutomataTheory Doc

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+i-1;n) = MinAr(f;j-1;n-i)+i
9. f(n-(j+i)) = f(n)

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

By: RW (AddrC [3] (RecUnfoldC `min_ar`)) 0 THEN SplitOnConclITE

Generated subgoals:

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

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

About:

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