IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
finite-partition212112 1. n : 2. 0<n 3. k : 4. c : nk 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. sum(if c(n-1)=x 1 else 0 fi | x < k) = if c(n-1)=c(n-1) 1 else 0 fi
sum(if c(n-1)=j 1 else 0 fi | j < k) = 1
By:
MoveToConcl -1 THEN SplitOnConclITE
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html