Nuprl - Proof: fun exp compose 2 1 1

(11steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fun exp compose 2 1 1

1. T : Type
2. n :

3. 0<n
4.

h,f:(T

T). f^n-1 o h = primrec(n-1;h;

i,g. f o g)
5. h : T

T
6. f : T

primrec(1+n-1;

x.x;

i,g. f o g) o h = f o primrec(n-1;h;

i,g. f o g)

By:	Subst (primrec(1+n-1;x.x;i,g. f o g) = f o primrec(n-1;x.x;i,g. f o g)) 0

Generated subgoals:

1 primrec(1+n-1;x.x;i,g. f o g) = f o primrec(n-1;x.x;i,g. f o g) TT
2 steps

2 f o primrec(n-1;x.x;i,g. f o g) o h = f o primrec(n-1;h;i,g. f o g)
4 steps

About:

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

(11steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Doc

1	primrec(1+n-1;x.x;i,g. f o g) = f o primrec(n-1;x.x;i,g. f o g) TT	2 steps
2	f o primrec(n-1;x.x;i,g. f o g) o h = f o primrec(n-1;h;i,g. f o g)	4 steps