Nuprl - Proof: fun exp compose 2 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fun exp compose 2 1 1 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. T

T
6. f : T

T
7. id : T

T
8. (

x.x) = id

primrec(1+n-1;id;

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

i,g. f o g)

By:	RWO Thm* n,m:, b:T, c:((n+m)TT). Thm* primrec(n+m;b;c) = primrec(n;primrec(m;b;c);i,t. c(i+m,t)) 0 THEN Reduce 0

Generated subgoals:

None

About:

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