(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 1
1. x : 
2. 
3. <0,0> = <0,x+1>
  False
By: Analyze-1 THEN OnAllHyps Reduce

Generated subgoals:

None

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

(4steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc