Nuprl - Proof: Ramsey 2 1

(41steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

At: Ramsey 2 1

1. k:
2. 0 < k
3. 0 < k-1 (L: List. 0 < ||L|| (r:. r- > L^k-1))
4. k = 1
5. 0 < k
6. d:
7. d1:. d1 < d (L: List. sum(L[i] | i < ||L||) = d1 0 < ||L|| (r:. r- > L^k))
8. L: List
9. sum(L[i] | i < ||L||) = d
10. 0 < ||L||

r:. r- > L^k

By: Decide (i:||L||. L[i] < k)

Generated subgoals:

1 11. i:||L||. L[i] < k
r:. r- > L^k 1 step

2 11. (i:||L||. L[i] < k)
r:. r- > L^k 32 steps

About:

(41steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

1	11. `i:\|\|L\|\|. L[i] < k` `r:. r- > L^k`	1 step

2	11. `(i:\|\|L\|\|. L[i] < k)` `r:. r- > L^k`	32 steps