1. k : 
2. k1:. k1<k  (x,y:. x+y = k1  (a:. nat_to_nat_pair(a) = <x,y>))
3. x : 
4. x1:. x1<x  (y:. x1+y = k  (a:. nat_to_nat_pair(a) = <x1,y>))
5. y : 
6. x+y = k
7. x = 0
8. n : 
9. nat_to_nat_pair(n) = <x-1,y+1>
  next_nat_pair(<x-1,y+1>) = <x,y>

By:	Compute next_nat_pair(<x-1,y+1>) * if y+1=0 <0,x-1+1> else <x-1+1,y+1-1> fi THEN SplitITE Concl

None

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