Nuprl - Proof: Ramsey-base-case 1 2 1 1 1

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

At: Ramsey-base-case 1 2 1 1 1

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||
6. f: L[c]n
7. increasing(f;L[c])
8. s:L[c]. G([(f(s))]) = c
9. 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: UnivCD THEN RepeatFor 2 ((Analyze -3) THEN (All Reduce) THEN (Try (Complete Auto)))

Generated subgoal:

1 10. u: L[c]
11. 1 = 1
12. x,y:1. x < y [u][x] < [u][y]
G([(f(u))]) = c 1 step

About:

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