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

At: Ramsey 2 1 2 2 2 2 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 < 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. f: i:||L||r:r- > L[i--]^k
||mklist(||L||;i.1of(f(i)))|| = ||L|| & (i:||L||. 0 < L[i] mklist(||L||;i.1of(f(i)))[i]- > L[i--]^k)
By:
RWO Thm* n:, f:(nT). ||mklist(n;f)|| = n 0
THEN
RWO Thm* n:, f:(nT), i:n. mklist(n;f)[i] = f(i) 0
THEN
AutoInst [i1]
Generated subgoals:

115. i: ||L||
16. r:
0 < L[i]		1 step
 
2 ||L|| = ||L|| & (i:||L||. 0 < L[i] (i.1of(f(i)))(i)- > L[i--]^k)2 steps

About:
productlistintnatural_numbersubtractless_thanlambdaapply
functionuniverseequalimpliesallexists

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