At: split factor2 char

  k:{2...}, g:({2..k}), x,y:{2..k}.
  xy<k
  
  x<y
  
  {2..k}(g) = {2..k}(split_factor2(g; x; y))
  & split_factor2(g; x; y)(xy) = 0
  & (u:{2..k}. xy<u  split_factor2(g; x; y)(u) = g(u))

By:	{After letting h = split_factor2(g; x; y)  {2..k} and elaborating the four {cases from its definition, the only work is showing that it factors the same {number as g {} SideProof

1

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..k}(g) = {2..k}(h)

11 steps

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