Nuprl - Pf phole_aux 2 1 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. ii:{1..(1+n)}, jj:ii. f(ii) = f(jj)

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

By: Inst [x.if f(x)=n-1 f(n) else f(x) fi] 2

Generated subgoals:

1 (x.if f(x)=n-1 f(n) else f(x) fi) n(-1+n)

2 5. i:n, j:i. (x.if f(x)=n-1 f(n) else f(x) fi)(i) = (x.if f(x)=n-1 f(n) else f(x) fi)(j) (-1+n)
i:1, j:i. f(i) = f(j)

About:

1	`(x.if f(x)=n-1 f(n) else f(x) fi) n(-1+n)`
2	5. `i:n, j:i. (x.if f(x)=n-1 f(n) else f(x) fi)(i) = (x.if f(x)=n-1 f(n) else f(x) fi)(j) (-1+n)` `i:1, j:i. f(i) = f(j)`