WhoCites Definitions DiscrMathExt Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites split factor1?
split_factor1Def  split_factor1(gx)(u)
Def  == if u=x g(x)+g(xx)+g(xx) ; u=xx 0 else g(u) fi
Thm*  k:{2...}, g:({2..k}), x:{2..k}.
Thm*  xx<k  split_factor1(gx {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 DiscrMathExt Sections NuprlLIB Doc