WhoCites Definitions FTA Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Removing one member from a factorization multiset

Who Cites reduce factorization?
reduce_factorizationDef  reduce_factorization(fj)(i) == if i=j f(i)-1 else f(i) fi
Thm*  a,b:f:({a..b}), j:{a..b}.
Thm*  0<f(j reduce_factorization(fj {a..b}
eq_intDef  i=j == if i=j true ; false fi
Thm*  i,j:. (i=j 

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

WhoCites Definitions FTA Sections DiscrMathExt Doc