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

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

1. y1 :

2. y2 :

<y1,y2> = <0,0>
4. if y2+1=

<0,y1-1+1> else <y1-1+1,y2+1-1> fi = <0,0>
5. y1

<y1,y2> = <0,0>

By:	SplitITE Hyp:-2

Generated subgoal:

1 4. <y1-1+1,y2+1-1> = <0,0>
5. y1  0
6. y2+1  0
  <y1,y2> = <0,0>
1 step

About:

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