Nuprl - Proof: next nat pair vs prev nat pair 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: next nat pair vs prev nat pair 1

1. x :

prev_nat_pair(next_nat_pair(x)) = x

By:	Analyze-1 THEN Compute Coprev_nat_pair(next_nat_pair(<x1,x2>)) Co* Coif x2=0 <0,x1+1> else <x1+1,x2-1> fi/x,y. if x=0 <y-1,0> else <x-1,y+1> fi THEN SplitITE Concl THEN Reduce Concl

Generated subgoals:

1 1. x1 :
2. x2 :
3. x2 = 0
  <x1+1-1,0> = <x1,x2>
1 step

2 1. x1 :
2. x2 :
3. x2  0
  if x1+1=0 <x2-1-1,0> else <x1+1-1,x2-1+1> fi = <x1,x2>
1 step

About:

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

1	1. x1 : 2. x2 : 3. x2 = 0 <x1+1-1,0> = <x1,x2>	1 step
2	1. x1 : 2. x2 : 3. x2 0 if x1+1=0 <x2-1-1,0> else <x1+1-1,x2-1+1> fi = <x1,x2>	1 step