1. 'a : S
2. x : ('a)
3. f : 'a
4. n : 
5. x = <m:. if m<n then f(m) else @x:'a. true fi ,n>
  <m:. if m<n then f(m) else @x:'a. true fi ,n>
  =
  <n@0:. if n@0<||f{n}|| then (f{n})[n@0] else arb('a) fi ,||f{n}||>

By:	Inst Thm* m,n:, f:({m..n}T). n<m  ||f{m..n}|| = n-m   ['a;0;n;f] THEN StrongAuto THEN Try (Complete (Unfold `label` 0)) THEN Last Analyze THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

1	f  n'a	1 step
2	6. ||f{n}|| = n-0     <m:. if m<n then f(m) else @x:'a. true fi ,n>   =   <n@0:. if n@0<||f{n}|| then (f{n})[n@0] else arb('a) fi ,||f{n}||>	7 steps

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