(26steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
At:
finite-partition
2
1
2
1
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
n-1+sum(if c(n-1)=
j
1 else 0 fi | j < k) = n
By:
Assert (sum(if c(n-1)=
j
1 else 0 fi | j < k) = 1)
Generated subgoals:
1
sum(if c(n-1)=
j
1 else 0 fi | j < k) = 1
3
steps
 
2
9.
sum(if c(n-1)=
j
1 else 0 fi | j < k) = 1
n-1+sum(if c(n-1)=
j
1 else 0 fi | j < k) = n
Auto
About:
(26steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc