Nuprl - Proof: compose iter inj cycles 1 1 1

(13steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: compose iter inj cycles 1 1 1

1. k :

2. f :

k

k
3. Inj(

k;

k; f)
4. u :

k

i,j:

. i<j & f{

j}(u) = f{

i}(u)

By:	Inst: Thm* m,k:, f:(mk). k<m (x,y:m. x y & f(x) = f(y)) Using:[k+1 \| k \| i.f{i}(u)] ...a THEN Reduce Hyp:-1

Generated subgoal:

1 5. x,y:(k+1). x y & f{x}(u) = f{y}(u)
i,j:. i<j & f{j}(u) = f{i}(u)
5 steps

About:

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

(13steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc