WhoCites Definitions FTA Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites trivial factorization?
trivial_factorizationDef  trivial_factorization(z)(i) == if i=z 1 else 0 fi
Thm*  a,b:z:{a..b}. trivial_factorization(z {a..b}
eq_intDef  i=j == if i=j true ; false fi
Thm*  i,j:. (i=j 

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

WhoCites Definitions FTA Sections DiscrMathExt Doc