Nuprl - Proof: disjoint increasing onto 1 2 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 2 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.

i:

m. (

j:

n. i = f(j))

(

j:

k. i = g(j))
9.

j1:

n, j2:

k.

f(j1) = g(j2)
10. m

n+k

Inj(

(n+k);

m;

i.if i<

n

f(i) else g(i-n) fi)

By:	AllHyps (i.FwdThru Thm* k,m:, f:(km). increasing(f;k) Inj(k; m; f) [i]) THEN All (Unfold `inject`) THEN Reduce 0 THEN Analyze 0 THEN Analyze 0 THEN Repeat SplitOnConclITE THEN AllHyps (i.FwdThru i [-1] THEN Complete Auto)

Generated subgoals:

1 11. a1,a2:k. g(a1) = g(a2)  a1 = a2
12. a1,a2:n. f(a1) = f(a2)  a1 = a2
13. a1 : (n+k)
14. a2 : (n+k)
15. a1<n
16. na2
17. f(a1) = g(a2-n)
  a1 = a2
1 step

2 11. a1,a2:k. g(a1) = g(a2)  a1 = a2
12. a1,a2:n. f(a1) = f(a2)  a1 = a2
13. a1 : (n+k)
14. a2 : (n+k)
15. na1
16. a2<n
17. g(a1-n) = f(a2)
  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