(4steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: next nat pair not zeroes 1 2
1. x : 
2. y : 
3. <0,0> = <x+1,y-1>
  False
By: Analyze-1 THEN OnAllHyps Reduce

Generated subgoals:

None

About:
pairproductnatural_numberaddsubtractequalfalse
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(4steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc