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

(22steps 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: disjoint increasing onto 1 1 1 1 2 1 1

1. m :

2. n :

3. k :

4. f :

n

m
5. g :

k

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

m

(j:

n

i = f(j))+(j:

k

i = g(j))
9.

j1:

n, j2:

k.

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

m
11. a2 :

m
12. q1 : (j:

n

a1 = f(j))+(j:

k

a1 = g(j))
13. h(a1) = q1
14. q2 : (j:

n

a2 = f(j))+(j:

k

a2 = g(j))
15. h(a2) = q2

InjCase(q1; p. 1of(p), n+1of(p)) = InjCase(q2; p. 1of(p), n+1of(p))

(n+k)

a1 = a2

By:	Analyze -4 THEN Analyze -4 THEN Analyze -2 THEN Analyze -2 THEN Reduce 0

Generated subgoals:

1 12. j : n
13. x1 : a1 = f(j)
14. h(a1) = inl(<j,x1>)
15. j1 : n
16. x2 : a2 = f(j1)
17. h(a2) = inl(<j1,x2>)
18. j = j1  (n+k)
  a1 = a2
1 step

2 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  (n+k)
  a1 = a2
1 step

About:

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

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