1. k : {2...}
2. g : {2..k}
3. x : {2..k}
4. y : {2..k}
5. xy<k
6. x<y
7. x<xy & y<xy
  {2..k}(g) = {2..k}(split_factor2(g; x; y))
  & split_factor2(g; x; y)(xy) = 0
  & (u:{2..k}. xy<u  split_factor2(g; x; y)(u) = g(u))

1	7. x<xy 8. y<xy   {2..k}(g) = {2..k}(split_factor2(g; x; y))	2 steps
2	7. x<xy 8. y<xy   split_factor2(g; x; y)(xy) = 0   & (u:{2..k}. xy<u  split_factor2(g; x; y)(u) = g(u))	1 step

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