Nuprl - Proof: compose iter sum 1

(6steps 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 sum 1

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

A
4. i :

5.

i1:

. i1<i

(

j,k:

. k = i1+j

f{

i1}(f{

j}(x)) = f{

k}(x))
6. j :

7. k :

8. k = i+j

f{

i}(f{

j}(x)) = f{

k}(x)

By:	Decide: i = 0

Generated subgoals:

1 9. i = 0
  f{i}(f{j}(x)) = f{k}(x)
1 step

2 9. i = 0
  f{i}(f{j}(x)) = f{k}(x)
3 steps

About:

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

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