WhoCites Definitions FTA Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(eliminating the power of a composite of two number by adding it to the power of its two factors)

Who Cites split factor2?
split_factor2Def  split_factor2(gxy)(u)
Def  == if u=x g(x)+g(xy) ; u=y g(y)+g(xy) ; u=xy 0 else g(u) fi
Thm*  k:{2...}, g:({2..k}), x,y:{2..k}.
Thm*  xy<k  split_factor2(gxy {2..k}
eq_intDef  i=j == if i=j true ; false fi
Thm*  i,j:. (i=j 

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

WhoCites Definitions FTA Sections DiscrMathExt Doc