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

At: finite-partition 2 2
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
(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 [(n-1) / (p(j))] 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)
By: Analyze 0
Generated subgoals:

1 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 [(n-1) / (p(j))] else p(j) fi[y]4 steps
 
2 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]) = j9 steps

About:
listconsifthenelseintnatural_numbersubtract
less_thanapplyfunctionequalimpliesandall

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