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

At: Ramsey-base-case 1 1 1 1 1 1 2
1. L: List
2. n:
3. G: {s:(n List)| ||s|| = 1 & (x,y:||s||. x < y s[x] < s[y]) }||L||
4. c: ||L||
5. A: List
6. m:
7. m||A||
8. x: ||A||
9. A[x] < n
[A[x]] {s:(n List)| ||s|| = 1 & (x,y:||s||. x < y s[x] < s[y]) }
By:
Analyze
THEN
Reduce 0
THEN
Try (Complete Auto)
Generated subgoal:

1 [A[x]] n List1 step

About:
listconsnilintnatural_numberless_thanset
functionequalmemberimpliesandall

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