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

By:

Let (h = split_factor1(g; x)) ...w THEN ((h(xx) = 0   ((& h(x) = g(x)+g(xx)+g(xx)   ((& (u:{2..k}. u = x    u = xx    h(u) = g(u)  ) ((& By (Rewrite by h = split_factor1(g; x)  {2..k} ...w ((& By (THEN ((& By (Def of split_factor1(g; x) ((& By (THEN ((& By (Reduce Concl ... THEN SplitOnConclITEs ...)) (THEN (Auto)

1

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

PREMISE

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