Nuprl - Pf phole_aux 2 1 1 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. ii:{1..(1+n)}, jj:ii. f(ii) = f(jj)
5. i: n
6. j: i
7. if f(i)=n-1 f(n) else f(i) fi = if f(j)=n-1 f(n) else f(j) fi (-1+n)

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

By: MoveToConcl 7 THEN SplitOnConclITEs

Generated subgoals:

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

2 7. f(i) = n-1
8. f(j) = n-1
f(n) = f(j) (-1+n) (i:1, j:i. f(i) = f(j))

3 7. f(i) = n-1
8. f(j) = n-1
f(i) = f(n) (-1+n) (i:1, j:i. f(i) = f(j))

4 7. f(i) = n-1
8. f(j) = n-1
f(i) = f(j) (-1+n) (i:1, j:i. f(i) = f(j))

About:

1	7. `f(i) = n-1` 8. `f(j) = n-1` `f(n) = f(n) (-1+n) (i:1, j:i. f(i) = f(j))`
2	7. `f(i) = n-1` 8. `f(j) = n-1` `f(n) = f(j) (-1+n) (i:1, j:i. f(i) = f(j))`
3	7. `f(i) = n-1` 8. `f(j) = n-1` `f(i) = f(n) (-1+n) (i:1, j:i. f(i) = f(j))`
4	7. `f(i) = n-1` 8. `f(j) = n-1` `f(i) = f(j) (-1+n) (i:1, j:i. f(i) = f(j))`