Nuprl - Proof: compose iter inj cycles 1 1 2 1

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

1. k :

2. f :

k
3. Inj(

k; f)
4. u :

k
5. i :

6. j :

7. i<j
8. f{

j}(u) = f{

i}(u)

. f{

i}(u) = u

By:	Rewrite-1 by Thm* x:A, f:(AA), k:, i:{0...k}. f{k}(x) = f{i}(f{k-i}(x)) Using:[A:= k \| k:= j \| i:= i \| x:= u] ...

Generated subgoal:

1 9. f{i}(f{j-i}(u)) = f{i}(u)
i:. f{i}(u) = u
2 steps

About:

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