Nuprl - Proof: injection le 1 1 2

(37steps 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: injection le 1 1 2

1. k :

2. 0<k
3.

m:

. (

f:(

(k-1)

m). Inj(

(k-1);

m; f))

k-1

m
4. m :

5. f :

k

m
6. Inj(

k;

m; f)
7. f(0)

m
8.

g:(

(k-1)

(m-1)).

i:

(k-1). g(i) = if f(i)=

m-1

f(k-1) else f(i) fi

f:(

(k-1)

(m-1)). Inj(

(k-1);

(m-1); f)

By:	ExRepD THEN InstConcl [g]

Generated subgoal:

1 8. g : (k-1)(m-1)
9. i:(k-1). g(i) = if f(i)=m-1 f(k-1) else f(i) fi
Inj((k-1); (m-1); g)
26 steps

About:

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

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