Nuprl - Proof: fun exp compose

(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

T:Type, n:

, h,f:(T

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

i,g. f o g)

By:	RepeatFor 2 (Analyze 0) THEN NatInd -1 THEN Unfold `fun_exp` 0 THEN Reduce 0

Generated subgoals:

1 1. T : Type
h,f:(TT). (x.x) o h = h
1 step

2 1. T : Type
2. n :
3. 0<n
4. h,f:(TT). f^n-1 o h = primrec(n-1;h;i,g. f o g)
h,f:(TT). primrec(n;x.x;i,g. f o g) o h = primrec(n;h;i,g. f o g)
9 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	1. T : Type h,f:(TT). (x.x) o h = h	1 step
2	1. T : Type 2. n : 3. 0<n 4. h,f:(TT). f^n-1 o h = primrec(n-1;h;i,g. f o g) h,f:(TT). primrec(n;x.x;i,g. f o g) o h = primrec(n;h;i,g. f o g)	9 steps