(26steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
At:
finite-partition
2
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
sum(if c(n-1)=
j
||[(n-1) / (p(j))]|| else ||p(j)|| fi | j < k) = n
By:
Reduce 0
THEN
RWO
Thm*
k:
, f,g:(
k
), p:(
k
). sum(if p(i)
f(i)+g(i) else f(i) fi | i < k) = sum(f(i) | i < k)+sum(if p(i)
g(i) else 0 fi | i < k) 0
THEN
HypSubst' -3 0
Generated subgoal:
1
n-1+sum(if c(n-1)=
j
1 else 0 fi | j < k) = n
5
steps
About:
(26steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc