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

1	next_nat_pair(prev_nat_pair(<y1,y2>)) = <y1,y2>	3 steps
2	next_nat_pair(prev_nat_pair(<y1,y2>)) = <0,0>	9 steps

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