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

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

By: BackThru Thm* i:, j:{i+1...}, E:({i..j}Prop). E(i) (k:{(i+1)..j}. E(k-1) E(k)) (k:{i..j}. E(k)) THEN All ArithSimp

Generated subgoals:

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

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

About:

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