At:
pigeon-hole
1
1
1
1
1
1
1
1.
n: 
2.
m:
3.
f: n
m
4.
a1,a2:n. f(a1) = f(a2) 
a1 = a2
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
13.
(p(j))[0] < n
14.
f((p(j))[0]) = j
15.
(p(j))[1] < n
16.
f((p(j))[1]) = j
17.
(p(j))[0] > (p(j))[1]
0(p(j))[0]
By:
MoveToConcl -6
THEN
GenConclAtAddr [2;2;2]
THEN
Lemmaize [-1]
Generated subgoals:
None
About:
