Nuprl - Pf min_ar

PrintForm Definitions choice 1 Sections AutomataTheory Doc

1. f:
2. n:
3. i: (n+1)

MinAr(f;i;n) (i+1)

By: NSubsetInd 3 THEN RecCaseSplit `min_ar`

Generated subgoals:

1 3. f(n-0) = f(n)
0 1

2 3. f(n-0) = f(n)
MinAr(f;-1;n) 1

3 3. i:
4. 0 < i
5. i < n+1
6. MinAr(f;i-1;n) (i-1+1)
7. f(n-i) = f(n)
i (i+1)

4 3. i:
4. 0 < i
5. i < n+1
6. MinAr(f;i-1;n) (i-1+1)
7. f(n-i) = f(n)
MinAr(f;i-1;n) (i+1)

About:

1	3. `f(n-0) = f(n)` `0 1`
2	3. `f(n-0) = f(n)` `MinAr(f;-1;n) 1`
3	3. `i:` 4. `0 < i` 5. `i < n+1` 6. `MinAr(f;i-1;n) (i-1+1)` 7. `f(n-i) = f(n)` `i (i+1)`
4	3. `i:` 4. `0 < i` 5. `i < n+1` 6. `MinAr(f;i-1;n) (i-1+1)` 7. `f(n-i) = f(n)` `MinAr(f;i-1;n) (i+1)`