(10steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

At: pigeon-hole 1 1 1 1 1
1. n:
2. m:
3. f: nm
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
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
By:
ExRepD
THEN
Unfold `inject` 4
THEN
InstHyp [(p(j))[0];(p(j))[1]] 4
THEN
Try (Complete Auto)
Generated subgoals:

14. 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]
(p(j))[0] n		2 steps
 
24. 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]
(p(j))[1] n		2 steps

About:
listintnatural_numberless_thanapplyfunctionequalmemberimpliesall

(10steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc