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

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

At: Ramsey 2 1 2 2 2 1 2 3 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 < 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||
11. (i:||L||. L[i] < k)
12. i:||L||. 2L[i]
13. L: List. sum(L[i] | i < ||L||) = d-1 0 < ||L|| (r:. r- > L^k)
14. i: ||L||
15. d:. sum(L[x]-L[i--][x] | x < ||L||) = d sum(L[x] | x < ||L||) = sum(L[i--][x] | x < ||L||)+d

sum(L[x]-L[i--][x] | x < ||L||) = 1

By: Inst Thm* n:, f:(n), m:n. (x:n. x = m f(x) = 0) sum(f(x) | x < n) = f(m) [||L||;x. L[x]-L[i--][x];i] THEN AutoInst [i] THEN Try ((RWO Thm* L: List, i:||L||. 0 < L[i] ||L[i--]|| = ||L|| 0) THEN (AutoInst [i]))

Generated subgoals:

1 16. x: ||L||
17. x = i
L[x]-L[i--][x] = 0 1 step

2 16. sum(L[x]-L[i--][x] | x < ||L||) = L[i]-L[i--][i]
sum(L[x]-L[i--][x] | x < ||L||) = 1 2 steps

About:

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

1	16. `x:` `\|\|L\|\|` 17. `x = i` `L[x]-L[i--][x] = 0`	1 step

2	16. `sum(L[x]-L[i--][x] \| x < \|\|L\|\|) = L[i]-L[i--][i]` `sum(L[x]-L[i--][x] \| x < \|\|L\|\|) = 1`	2 steps