Nuprl - Pf phole

PrintForm Definitions finite sets Sections AutomataTheory Doc

1. n: {1+1...}
2. f:((n-1+1)(n-1)). i:(n-1+1), j:i. f(i) = f(j)
3. f: (n+1)n

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

By: Assert (iii:(n+1). (ii:{(iii+1)..(n+1)}, jj:ii. f(ii) = f(jj)) (i:(iii+1), j:i. f(i) = f(j)))

Generated subgoals:

1 iii:(n+1). (ii:{(iii+1)..(n+1)}, jj:ii. f(ii) = f(jj)) (i:(iii+1), j:i. f(i) = f(j))

2 4. iii:(n+1). (ii:{(iii+1)..(n+1)}, jj:ii. f(ii) = f(jj)) (i:(iii+1), j:i. f(i) = f(j))
i:(n+1), j:i. f(i) = f(j)

About:

1	`iii:(n+1). (ii:{(iii+1)..(n+1)}, jj:ii. f(ii) = f(jj)) (i:(iii+1), j:i. f(i) = f(j))`
2	4. `iii:(n+1). (ii:{(iii+1)..(n+1)}, jj:ii. f(ii) = f(jj)) (i:(iii+1), j:i. f(i) = f(j))` `i:(n+1), j:i. f(i) = f(j)`