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

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

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. p: ||L||( List)
6. sum(||p(j)|| | j < ||L||) = n
7. j:||L||, x,y:||p(j)||. x < y (p(j))[x] > (p(j))[y]
8. j:||L||, x:||p(j)||. (p(j))[x] < n & (x.G([x]))((p(j))[x]) = j
9. c: ||L||
10. L[c]||p(c)||

f:(L[c]n). increasing(f;L[c]) & (s:L[c]. G([(f(s))]) = c)

By: AllHyps (InstHyp [c]) THEN RepeatFor 3 (MoveToConcl -1) THEN GenConcl (p(c) = A) THEN GenConcl (L[c] = m) THEN AllHyps Thin THEN Reduce 0

Generated subgoal:

1 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:
m||A|| (x:||A||. A[x] < n & G([A[x]]) = c) (x,y:||A||. x < y A[x] > A[y]) (f:(mn). increasing(f;m) & (s:m. G([(f(s))]) = c)) 10 steps

About:

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