InvFuns(;{xy:()| xy = <0,0>   };next_nat_pair;prev_nat_pair)

1	1. x :    prev_nat_pair(next_nat_pair(x)) = x	3 steps
2	1. y : {xy:()| xy = <0,0>   }   next_nat_pair(prev_nat_pair(y)) = y  {xy:()| xy = <0,0>   }	14 steps

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