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

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

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. i :

InjCase(h(i); p. 1of(p), n+1of(p))

(n+k)

By:	GenConcl (h(i) = q) THEN Analyze -2 THEN Analyze -2 THEN Reduce 0

Generated subgoals:

None

About:

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