Nuprl - Proof: compose iter sum 1 1

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

1. A : Type
2. x : A
3. f : A

A
4. i :

i1:

. i1<i

(

j,k:

. k = i1+j

i1}(f{

j}(x)) = f{

k}(x))
6. j :

7. k :

8. k = i+j
9. i = 0

i}(f{

j}(x)) = f{

k}(x)

By:	Rewrite by i = 0 THEN Rewrite by j = k THEN Rewrite by Thm* f:(AA), x:A. f{0}(x) = x

Generated subgoals:

None

About:

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