k:{2...}, g:({2..k}), x,y:{2..k}.
  xy<k  split_factor2(g; x; y)  {2..k}

By:

Auto

1

1. k : {2...} 2. g : {2..k} 3. x : {2..k} 4. y : {2..k} 5. xy<k   split_factor2(g; x; y)  {2..k}

3 steps

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