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

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

f:(

(n+k)

m). Inj(

(n+k);

m; f)

By:	InstConcl [i.if i<n f(i) else g(i-n) fi]

Generated subgoals:

1   (i.if i<n f(i) else g(i-n) fi)  (n+k)m
1 step

2   Inj((n+k); m; i.if i<n f(i) else g(i-n) fi)
3 steps

3 11. f1 : (n+k)m
  Inj((n+k); m; f1)  Prop
Auto

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