(10steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
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:

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

About:
listintnatural_numberless_thanapplyfunctionequalmemberimpliesall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(10steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Doc