Remark WhoCites Definitions DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
How to step from pair to pair exhaustively

Who Cites next nat pair?
next_nat_pairDef  next_nat_pair(xy) == xy/x,y. if y=0 <0,x+1> else <x+1,y-1> fi
Thm*  next_nat_pair  
eq_intDef  i=j == if i=j true ; false fi
Thm*  i,j:. (i=j)  

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

Remark WhoCites Definitions DiscreteMath Sections DiscrMathExt Doc