Nuprl - Proof: compose iter prod 1 2 2 1 1

(14steps 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 prod 1 2 2 1 1

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

A
4. i :

5. j :

6.

j1:

. j1<j

(

k:

. k = i

j1

f{

i}{

j1}(x) = f{

k}(x))
7. k :

8. k = i

j
9.

j = 0
10.

i = 0
11. i

1

i

j

f{

i}(f{

i}{

j-1}(x)) = f{

k}(x)

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

Generated subgoal:

1 f{i}(f{i}{j-1}(x)) = (f{i} o f{k-i})(x)
3 steps

About:

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

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