(10steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
At:
pigeon-hole
1
1
1
1
1.
n:
2.
m:
3.
f:
n
m
4.
Inj(
n;
m; f)
5.
p:
m
(
List)
6.
sum(||p(j)|| | j < m) = n
7.
j:
m, x,y:
||p(j)||. x < y
(p(j))[x] > (p(j))[y]
8.
j:
m, x:
||p(j)||. (p(j))[x] < n & f((p(j))[x]) = j
9.
j:
m
10.
x:
||p(j)||. (p(j))[x] < n & f((p(j))[x]) = j
11.
x,y:
||p(j)||. x < y
(p(j))[x] > (p(j))[y]
12.
||p(j)||
1
||p(j)||
1
By:
InstHyp [0] -3
THEN
InstHyp [1] -4
THEN
InstHyp [0;1] -4
Generated subgoal:
1
13.
(p(j))[0] < n & f((p(j))[0]) = j
14.
(p(j))[1] < n & f((p(j))[1]) = j
15.
(p(j))[0] > (p(j))[1]
||p(j)||
1
5
steps
About:
(10steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc