Def f^n == primrec(n;x.x;i,g. f o g)

is mentioned by

Thm* f:(TT), m:(T). Thm* (x:T. m(f(x))m(x) & (m(f(x)) = m(x)  f(x) = x)) Thm*  Thm* (x:T. n:. f(f^n(x)) = f^n(x))	[iteration_terminates]
Thm* f:(TT), n:, x:T. f(f^n-1(x)) = f^n(x)	[fun_exp_add1_sub]
Thm* f:(TT), n:, x:T. f(f^n(x)) = f^n+1(x)	[fun_exp_add1]
Thm* n,m:, f:(TT). f^n+m = f^n o f^m	[fun_exp_add]
Thm* n:, h,f:(TT). f^n o h = primrec(n;h;i,g. f o g)	[fun_exp_compose]

Try larger context: MarkB generic IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html