a,b:, f:({a..b}), j:{a..b}.
  0<f(j)  reduce_factorization(f; j)  {a..b}

By:	Def of reduce_factorization(<term>; <term>) THEN Guarding if <bool> <*> else <else> fi Auto

1

1. a :  2. b :  3. f : {a..b} 4. j : {a..b} 5. 0<f(j) 6. i : {a..b}   if i=j f(i)-1 else f(i) fi

2 steps

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