k:{2...}, g:({2..k}), x:{2..k}.
  xx<k  split_factor1(g; x)  {2..k}

By:

Auto

1

1. k : {2...} 2. g : {2..k} 3. x : {2..k} 4. xx<k   split_factor1(g; x)  {2..k}

3 steps

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