Nuprl - Proof: compose iter sum

(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

A:Type, x:A, f:(A

A), i,j,k:

. k = i+j

i}(f{

j}(x)) = f{

k}(x)

By:	Guarding (i:. <prop>) Auto THEN CompNatInd Concl

Generated subgoal:

1 1. A : Type
2. x : A
3. f : AA
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)
5 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