Nuprl - Proof: Ramsey-recursion 1 2 1 1 2 1 1 1 1 3 2 2 1 2 1 1 2

At: Ramsey-recursion 1 2 1 1 2 1 1 1 1 3 2 2 1 2 1 1 2

1. a:
2. s: a List
3. u: a
4. v: a List
5. (i:||v||. v[i] = a-1) v (a-1) List
6. (i:(||v||+1). [u / v][i] = a-1)

v (a-1) List

By: BackThru -2 THEN ParallelOp -1 THEN ExRepD THEN InstConcl [i+1]

Generated subgoal:

1 6. i: ||v||
7. v[i] = a-1
[u / v][(i+1)] = a-1 1 step

About: