Def  split_factor2(g; x; y)(u)
Def  == if u=x g(x)+g(xy) ; u=y g(y)+g(xy) ; u=xy 0 else g(u) fi

is mentioned by

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

[split_factor2_char]

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html