Nuprl - Proof: Ramsey 1 1

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

At: Ramsey 1 1

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

r:. r- > L^1

By: Decide (0 < sum(L[i]-1 | i < ||L||)+1)

Generated subgoals:

1 9. 0 < sum(L[i]-1 | i < ||L||)+1
r:. r- > L^1 1 step

2 9. 0 < sum(L[i]-1 | i < ||L||)+1
r:. r- > L^1 2 steps

About:

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

1	9. `0 < sum(L[i]-1 \| i < \|\|L\|\|)+1` `r:. r- > L^1`	1 step

2	9. `0 < sum(L[i]-1 \| i < \|\|L\|\|)+1` `r:. r- > L^1`	2 steps