At:
finite-partition
2
1
2
1
1
2
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.
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: