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

At: Ramsey-base-case 1 2
1. L: List
2. n:
3. sum(L[i]-1 | i < ||L||)+1n
4. G: {s:(n List)| ||s|| = 1 & (x,y:||s||. x < y s[x] < s[y]) }||L||
5. c:||L||, f:(L[c]n). increasing(f;L[c]) & (s:L[c]. G([(f(s))]) = c)
c:||L||, f:(L[c]n). increasing(f;L[c]) & (s:L[c] List. ||s|| = 1 (x,y:||s||. x < y s[x] < s[y]) G(map(f;s)) = c)
By: ParallelOp -1
Generated subgoals:

15. c: ||L||
6. f:(L[c]n). increasing(f;L[c]) & (s:L[c]. G([(f(s))]) = c)
f:(L[c]n). increasing(f;L[c]) & (s:L[c] List. ||s|| = 1 (x,y:||s||. x < y s[x] < s[y]) G(map(f;s)) = c)		5 steps
 
25. c: ||L||
6. f:(L[c]n). increasing(f;L[c]) & (s:L[c]. G([(f(s))]) = c)
7. c1: ||L||
8. f: L[c1]n
9. increasing(f;L[c1])
10. s: L[c1] List
11. ||s|| = 1
12. x,y:||s||. x < y s[x] < s[y]
map(f;s) {s:(n List)| ||s|| = 1 & (x,y:||s||. x < y s[x] < s[y]) }		1 step

About:
listconsnilintnatural_numberaddsubtractless_thansetapply
functionequalmemberimpliesandallexists

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