1. k : {2...}
2. g : {2..k}
3. x : {2..k}
4. y : {2..k}
5. xy<k
6. x<y
7. x<xy
8. y<xy
9. h : {2..k}
10. h = split_factor2(g; x; y)
11. h(xy) = 0
12. h(x) = g(x)+g(xy)
13. h(y) = g(y)+g(xy)
14. u:{2..k}. u = x  u = y  u = xy  h(u) = g(u)
  {2..x}(g)xg(x){x+1..y}(g)yg(y){y+1..xy}(g)
  {2..x}(g)xg(x){x+1..y}(g)yg(y)(xy)g(xy){xy+1..k}(g)
  =
  {2..x}(h)xh(x){x+1..y}(h)yh(y){y+1..xy}(h)
  {2..x}(h)xh(x){x+1..y}(h)yh(y)(xy)h(xy){xy+1..k}(h)

By:	MulFactorOut [{2..x}(g),{2..x}(h) ;{x+1..y}(g),{x+1..y}(h) ;{y+1..xy}(g),{y+1..xy}(h) ;{xy+1..k}(g),{xy+1..k}(h)] Concl ...a

1	{2..x}(g) = {2..x}(h)	1 step
2	{x+1..y}(g) = {x+1..y}(h)	1 step
3	{y+1..xy}(g) = {y+1..xy}(h)	1 step
4	{xy+1..k}(g) = {xy+1..k}(h)	1 step
5	xg(x)yg(y)(xy)g(xy) = xh(x)yh(y)(xy)h(xy)	PREMISE

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