1. x1 : 
2. y1 : 
3. x2 : 
4. y2 : 
5. next_nat_pair(<x1,y1>) = next_nat_pair(<x2,y2>)
  <x1,y1> = <x2,y2>

By:	Compute-1 Co(next_nat_pair(<x1,y1>) * if y1=0 <0,x1+1> else <x1+1,y1-1> fi) Co= Co(next_nat_pair(<x2,y2>) * if y2=0 <0,x2+1> else <x2+1,y2-1> fi) Co  THEN 2 Times (SplitITE Hyp:5) THEN Analyze5 THEN OnAllHyps Reduce THEN RemoveImpossibleCasesBy Auto

1	5. 0 = 0   6. x1+1 = x2+1   7. y1 = 0 8. y2 = 0   <x1,y1> = <x2,y2>	1 step
2	5. x1+1 = x2+1   6. y1-1 = y2-1   7. y1  0 8. y2  0   <x1,y1> = <x2,y2>	1 step

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