1. k : {2...}
2. g : {2..k}
3. x : {2..k}
4. xx<k
5. x<xx & x<xx
  {2..k}(g) = {2..k}(split_factor1(g; x))
  & split_factor1(g; x)(xx) = 0
  & (u:{2..k}. xx<u  split_factor1(g; x)(u) = g(u))

1	{2..k}(g) = {2..k}(split_factor1(g; x))	2 steps
2	split_factor1(g; x)(xx) = 0   & (u:{2..k}. xx<u  split_factor1(g; x)(u) = g(u))	1 step

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