1. 'a : S
2. x : 'a
3. f : 'a  'a
4. n : 
5. fun : 'a
6. fun(0) = x
7. m:. m<n+1  fun(m+1) = f(fun(m))
  ncompose(f;n;x) = fun(n)

1

4. fun : 'a 5. fun(0) = x 6. n :  7. 0<n 8. (m:. m<n-1+1  fun(m+1) = f(fun(m)))  ncompose(f;n-1;x) = fun(n-1) 9. m:. m<n+1  fun(m+1) = f(fun(m))   f(ncompose(f;n-1;x)) = fun(n)

7 steps

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