Nuprl - Proof: inj imp le 1 1 2 1

(7steps total) PfGloss PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: inj imp le 1 1 2 1

1. m :

2. 0<m
3.

k':

. (

f':(

(m-1)

k'). Inj(

(m-1);

k'; f'))

m-1

k'
4. k :

5. f :

m

k
6. Inj(

m;

k; f)
7. k-1

f':(

(m-1)

(k-1)). Inj(

(m-1);

(k-1); f')

By:	Witness: Replace value k-1 by f(m-1) in f

Generated subgoal:

1 Inj((m-1); (k-1); Replace value k-1 by f(m-1) in f)
1 step

About:

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

(7steps total) PfGloss PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc