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

At: Ramsey-recursion 1 2 1 1 2 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||
12. c: ||R||
13. f: R[c](n-1)
14. increasing(f;R[c])
15. s:R[c] List. ||s|| = k-1 (x,y:||s||. x < y s[x] < s[y]) G(map(f;s) @ [(n-1)]) = c
16. 0 < L[c]
17. R[c]- > L[c--]^k
18. (s. G(map(f;s))) {s:(R[c] List)| ||s|| = k & (x,y:||s||. x < y s[x] < s[y]) }||L[c--]||
19. c@0:||L[c--]||, f@0:(L[c--][c@0]R[c]). increasing(f@0;L[c--][c@0]) & (s:L[c--][c@0] List. ||s|| = k (x,y:||s||. x < y s[x] < s[y]) G(map(f;map(f@0;s))) = c@0)
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:
Analyze -1
THEN
AssertBY (c@0 ||L||) ((Subst' (||L|| = ||L[c--]||) 0) THEN (RWO Thm* L: List, i:||L||. 0 < L[i] ||L[i--]|| = ||L|| 0))
THEN
InstConcl [c@0]


Generated subgoals:

119. c@0: ||L[c--]||
20. f@0:(L[c--][c@0]R[c]). increasing(f@0;L[c--][c@0]) & (s:L[c--][c@0] List. ||s|| = k (x,y:||s||. x < y s[x] < s[y]) G(map(f;map(f@0;s))) = c@0)
21. c@0 ||L||
f:(L[c@0]n). increasing(f;L[c@0]) & (s:L[c@0] List. ||s|| = k (x,y:||s||. x < y s[x] < s[y]) G(map(f;s)) = c@0)
70 steps
 
219. c@0: ||L[c--]||
20. f@0:(L[c--][c@0]R[c]). increasing(f@0;L[c--][c@0]) & (s:L[c--][c@0] List. ||s|| = k (x,y:||s||. x < y s[x] < s[y]) G(map(f;map(f@0;s))) = c@0)
21. c@0 ||L||
22. c1: ||L||
23. f1: L[c1]n
24. increasing(f1;L[c1])
25. s: L[c1] List
26. ||s|| = k
27. x,y:||s||. x < y s[x] < s[y]
map(f1;s) {s:(n List)| ||s|| = k & (x,y:||s||. x < y s[x] < s[y]) }
1 step

About:
listconsnilintnatural_numberaddsubtractless_thanset
functionequalmemberimpliesandallexists

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