(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 1 2 1 1

1. n : 
2. 0<n
3. k : 
4. c : nk
5. p : k( List)
6. sum(||p(j)|| | j < k) = n-1
7. j:kx,y:||p(j)||. x<y  (p(j))[x]>(p(j))[y]
8. j:kx:||p(j)||. (p(j))[x]<n-1 & c((p(j))[x]) = j
  sum(if c(n-1)=j 1 else 0 fi | j < k) = 1


By: Inst
Thm* n:f:(n), m:n.
Thm* (x:nx = m  f(x) = 0)  sum(f(x) | x < n) = f(m)
[k;j. if c(n-1)=j 1 else 0 fi;c(n-1)]


Generated subgoals:

1 9. x : k
10. x = c(n-1)
  if c(n-1)=x 1 else 0 fi = 0

1 step
2 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

1 step

About:
listifthenelseintnatural_numbersubtract
less_thanapplyfunctionequalimpliesall
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