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

At: Ramsey-recursion 1
1. r:
2. k:
3. L: List
4. R: List
5. 2k
6. ||R|| = ||L||
7. i:||L||. 0 < L[i] R[i]- > L[i--]^k
8. r- > R^k-1
9. n:
10. r+1n
11. G: {s:(n List)| ||s|| = k & (x,y:||s||. x < y s[x] < s[y]) }||L||
c:||L||, f:(L[c]n). increasing(f;L[c]) & (s:L[c] List. ||s|| = k (x,y:||s||. x < y s[x] < s[y]) G(map(f;s)) = c)
By:
Unfold `arrows` -4
THEN
InstHyp [n-1;s. G(s @ [(n-1)])] -4
THEN
Fold `arrows` -5
Generated subgoals:

112. s: {s:((n-1) List)| ||s|| = k-1 & (x,y:||s||. x < y s[x] < s[y]) }
(s @ [(n-1)]) {s:(n List)| ||s|| = k & (x,y:||s||. x < y s[x] < s[y]) }		6 steps
 
212. c:||R||, f:(R[c](n-1)). increasing(f;R[c]) & (s:R[c] List. ||s|| = k-1 (x,y:||s||. x < y s[x] < s[y]) G(map(f;s) @ [(n-1)]) = c)
c:||L||, f:(L[c]n). increasing(f;L[c]) & (s:L[c] List. ||s|| = k (x,y:||s||. x < y s[x] < s[y]) G(map(f;s)) = c)		91 steps

About:
listconsnilintnatural_numberaddsubtractless_thanset
functionequalmemberimpliesandallexists

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