1. k : {2...}
2. g : {2..k}
3. x : {2..k}
4. xx<k
5. x<xx
6. h : {2..k}
7. h = split_factor1(g; x)
8. h(xx) = 0
9. h(x) = g(x)+g(xx)+g(xx)
10. u:{2..k}. u = x  u = xx  h(u) = g(u)
  xg(x)(xx)g(xx) = x(g(x)+g(xx)+g(xx))(xx)0

By:	{normalize factors into powers of x and x } Rewrite by Thm*  a,b,c:. (ab)c = acbc ...w THEN Repeat Rewrite by Thm*  i:, x,y:. ixiy = i(x+y) ...w

1

xg(x)xg(xx)xg(xx) = xg(x)xg(xx)xg(xx)x0x0

1 step

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