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}

By:	Inst: Thm*  i,j:{2...}. i<ij & j<ij Using:[x | y] ...w

1

6. x<xy & y<xy   split_factor2(g; x; y)  {2..k}

2 steps

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