1. y : {xy:()| xy = <0,0> }
  next_nat_pair(prev_nat_pair(y)) = y  {xy:()| xy = <0,0>   }

1

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

13 steps

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