Nuprl - Proof: disjoint increasing onto 1 1 1 1 2 1 1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: disjoint increasing onto 1 1 1 1 2 1 1 2

1. m :

2. n :

3. k :

4. f :

m
5. g :

m
6. increasing(f;n)
7. increasing(g;k)
8. h : i:

(j:

i = f(j))+(j:

i = g(j))
9.

j1:

n, j2:

f(j1) = g(j2)
10. a1 :

m
11. a2 :

m
12. j :

k
13. y1 : a1 = g(j)
14. h(a1) = inr(<j,y1>)
15. j1 :

k
16. y2 : a2 = g(j1)
17. h(a2) = inr(<j1,y2>)
18. n+j = n+j1

a1 = a2

By:	HypSubstSq -3 0 THEN HypSubstSq -6 0 THEN Analyze

Generated subgoals:

None

About:

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