(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. x : 
2. y : 
3. <0,0> = next_nat_pair(<x,y>)
  False
By: Compute-1 next_nat_pair(<x,y>) * if x2=0 <0,x+1> else <x+1,y-1> fi
THEN
SplitITE Hyp:-1

Generated subgoals:

1 3. <0,0> = <0,x+1>  
  False
1 step
2 3. <0,0> = <x+1,y-1>  
  False
1 step

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

(4steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc