1. n : 
2. 0<n
3. f:((n-1)), m:(n-1).
3. sum(f(x) | x < n-1) = f(m)+sum(if x=m 0 else f(x) fi | x < n-1)
4. f : n
5. m:(n-1). sum(f(x) | x < n-1) = f(m)+sum(if x=m 0 else f(x) fi | x < n-1)
6. m : n
7. m = n-1
8. sum(f(x) | x < n-1) = f(m)+sum(if x=m 0 else f(x) fi | x < n-1)
  sum(f(x) | x < n) = f(m)+sum(if x=m 0 else f(x) fi | x < n)

1

if n=0 0 else (x,n. n+f(x))(n-1,sum(f(x) | x < n-1)) fi   =   f(m)+if n=0 0   f(m)+else (x,n. n+if x=m 0 else f(x) fi)   f(m)+else (n-1   f(m)+else ,sum(if x=m 0 else f(x) fi | x < n-1)) fi

1 step

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