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

At: Ramsey 1 1 2
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
9. 0 < sum(L[i]-1 | i < ||L||)+1
r:. r- > L^1
By: InstConcl [1]
Generated subgoal:

1 1- > L^11 step

About:
listintnatural_numberaddsubtractless_thanequalimpliesallexists

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