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

(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. 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)

Inj(

m;

(n+k);

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

By:	Unfold `inject` 0 THEN Reduce 0 THEN Analyze 0 THEN Analyze 0

Generated subgoal:

1 10. a1 : m
11. a2 : m
  InjCase(h(a1); p. 1of(p), n+1of(p))
  =
  InjCase(h(a2); p. 1of(p), n+1of(p))
   (n+k)

  a1 = a2
4 steps

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