1. y1 : 
2. y2 : 
3. <y1,y2> = <0,0>
  next_nat_pair(prev_nat_pair(<y1,y2>)) = <y1,y2>

By:	Compute Conext_nat_pair(prev_nat_pair(<y1,y2>)) Co* Coif y1=0 <y2-1,0> else <y1-1,y2+1> fi/x,y. if y=0 <0,x+1> else <x+1,y-1> fi THEN SplitITE Concl THEN Reduce Concl

1	4. y1 = 0   <0,y2-1+1> = <y1,y2>	1 step
2	4. y1  0   if y2+1=0 <0,y1-1+1> else <y1-1+1,y2+1-1> fi = <y1,y2>	1 step

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