Nuprl - Pf phole_aux 2 1 2 1 2 1 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:{(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)

By: Analyze 0 THEN Decide (iii = ii)

Generated subgoals:

1 9. ii: {iii..(1+n)}
10. iii = ii {1..(1+n)}
jj:ii. f(ii) = f(jj)

2 9. ii: {iii..(1+n)}
10. iii = ii {1..(1+n)}
jj:ii. f(ii) = f(jj)

About:

1	9. `ii:` `{iii..(1+n)}` 10. `iii = ii {1..(1+n)}` `jj:ii. f(ii) = f(jj)`
2	9. `ii:` `{iii..(1+n)}` 10. `iii = ii {1..(1+n)}` `jj:ii. f(ii) = f(jj)`