Nuprl - Proof: finite-partition 2 2 1 1

(26steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: finite-partition 2 2 1 1

1. n :

2. 0<n
3. k :

4. c :

n

k
5. p :

k

(

List)
6. sum(||p(j)|| | j < k) = n-1
7.

j:

k, x,y:

||p(j)||. x<y

(p(j))[x]>(p(j))[y]
8.

j:

k, x:

||p(j)||. (p(j))[x]<n-1 & c((p(j))[x]) = j
9. j :

k
10.

x,y:

||p(j)||. x<y

(p(j))[x]>(p(j))[y]
11. c(n-1) = j

x@0,y:

||[(n-1) / (p(j))]||.

x@0<y

[(n-1) / (p(j))][x@0]>[(n-1) / (p(j))][y]

By:	((Reduce 0 THEN Analyze 0) THEN (Analyze 0) THEN (CaseNat 0 `x@0') (THEN ((Reduce 0)) THEN RWW Thm* a:T, as:T List, i:. 0<i i\|\|as\|\| [a / as][i] = as[(i-1)] 0

Generated subgoals:

1 12. x@0 : (||p(j)||+1)
13. y : (||p(j)||+1)
14. x@0 = 0
15. 0<y
n-1>(p(j))[(y-1)]
1 step

2 12. x@0 : (||p(j)||+1)
13. y : (||p(j)||+1)
14. x@0 = 0
15. x@0<y
(p(j))[(x@0-1)]>(p(j))[(y-1)]
1 step

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(26steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Doc