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

By:	Compute-1 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

1

4. (if y1=0 <y2-1,0> else <y1-1,y2+1> fi/x,y. 4. (if y=0 <0,x+1> else <x+1,y-1> fi) 4. = 4. <0,0> 4.     <y1,y2> = <0,0>

5 steps

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