Def  split_factor1(g; x)(u)
Def  == if u=x g(x)+g(xx)+g(xx) ; u=xx 0 else g(u) fi

is mentioned by

Thm*  k:{2...}, g:({2..k}), x:{2..k}. Thm*  xx<k Thm*   Thm*  {2..k}(g) = {2..k}(split_factor1(g; x)) Thm*  & split_factor1(g; x)(xx) = 0 Thm*  & (u:{2..k}. xx<u  split_factor1(g; x)(u) = g(u))

[split_factor1_char]

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html