(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. n : 
2. 0<n
3. k:, c:((n-1)k).
3. p:(k( List)). 
3. sum(||p(j)|| | j < k) = n-1
3. & (j:k, x,y:||p(j)||. x<y  (p(j))[x]>(p(j))[y])
3. & (j:k, x:||p(j)||. (p(j))[x]<n-1 & c((p(j))[x]) = j)
  k:, c:(nk).
  p:(k( List)). 
  sum(||p(j)|| | j < k) = n
  & (j:k, x,y:||p(j)||. x<y  (p(j))[x]>(p(j))[y])
  & (j:k, x:||p(j)||. (p(j))[x]<n & c((p(j))[x]) = j)
By: ((RepeatFor 2 (ParallelOp -1 THEN Thin -3) THEN ExRepD
((THEN
((InstConcl [j.if c(n-1)=j [(n-1) / (p(j))] else p(j) fi])
(THEN
((Reduce 0)
(THEN
((Analyze 0))
THENA
(RepeatFor 5 (Analyze THEN Try (Complete Auto)) THEN GenConcl ((p1(j))[x] = a)
(THEN
(Try (Complete Auto)
(THEN
(Analyze)

Generated subgoals:

1 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
  sum(||if c(n-1)=j [(n-1) / (p(j))] else p(j) fi|| | j < k) = n
8 steps
2 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
  (j:k, x,y:||if c(n-1)=j [(n-1) / (p(j))] else p(j) fi||.
  (x<y
  (
  (if c(n-1)=j [(n-1) / (p(j))] else p(j) fi[x]>if c(n-1)=j
  (if c(n-1)=j [(n-1) / (p(j))] else p(j) fi[x]>if [(n-1) / (p(j))]
  (if c(n-1)=j [(n-1) / (p(j))] else p(j) fi[x]>else p(j) fi[y])
  & (j:k, x:||if c(n-1)=j [(n-1) / (p(j))] else p(j) fi||.
  & (if c(n-1)=j [(n-1) / (p(j))] else p(j) fi[x]<n
  & (& c(if c(n-1)=j [(n-1) / (p(j))] else p(j) fi[x]) = j)
14 steps

About:
listconsifthenelseintnatural_numbersubtractless_than
lambdaapplyfunctionequalimpliesandall
exists
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