Nuprl - Pf phole_aux 2 1 2 1 2 1

PrintForm Definitions finite sets Sections AutomataTheory Doc

1. n: {2...}
2. f:(n(-1+n)). i:n, j:i. f(i) = f(j)
3. f: (1+n)n
4. iii: {1..(1+n)}
5. (ii:{iii..(1+n)}, jj:ii. f(ii) = f(jj)) (i:iii, j:i. f(i) = f(j))
6. ii:{(1+iii)..(1+n)}, jj:ii. f(ii) = f(jj)
7. fi: n
8. fi = f(iii)
9. x:iii. fi = f(x)

i:(1+iii), j:i. f(i) = f(j)

By: Analyze 5 THEN Analyze -1 THEN Analyze -1

Generated subgoals:

1 5. ii:{(1+iii)..(1+n)}, jj:ii. f(ii) = f(jj)
6. fi: n
7. fi = f(iii)
8. x:iii. fi = f(x)
ii:{iii..(1+n)}, jj:ii. f(ii) = f(jj)

2 5. ii:{(1+iii)..(1+n)}, jj:ii. f(ii) = f(jj)
6. fi: n
7. fi = f(iii)
8. x:iii. fi = f(x)
9. i: iii
10. j: i
11. f(i) = f(j)
i:(1+iii), j:i. f(i) = f(j)

About:

1	5. `ii:{(1+iii)..(1+n)}, jj:ii. f(ii) = f(jj)` 6. `fi:` `n` 7. `fi = f(iii)` 8. `x:iii. fi = f(x)` `ii:{iii..(1+n)}, jj:ii. f(ii) = f(jj)`
2	5. `ii:{(1+iii)..(1+n)}, jj:ii. f(ii) = f(jj)` 6. `fi:` `n` 7. `fi = f(iii)` 8. `x:iii. fi = f(x)` 9. `i:` `iii` 10. `j:` `i` 11. `f(i) = f(j)` `i:(1+iii), j:i. f(i) = f(j)`