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

(18steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc

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

1. y1 :

2. y2 :

<y1,y2> = <0,0>
4. (if y1=

<y2-1,0> else <y1-1,y2+1> fi/x,y.
4. (if y=

<0,x+1> else <x+1,y-1> fi)
4. =
4. <0,0>

<y1,y2> = <0,0>

By:	SplitITE Hyp:-1 THEN Reduce Hyp:-2

Generated subgoals:

1 4. <0,y2-1+1> = <0,0>
5. y1 = 0
  <y1,y2> = <0,0>
2 steps

2 4. if y2+1=0 <0,y1-1+1> else <y1-1+1,y2+1-1> fi = <0,0>
5. y1  0
  <y1,y2> = <0,0>
2 steps

About:

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

(18steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc

1	4. <0,y2-1+1> = <0,0> 5. y1 = 0 <y1,y2> = <0,0>	2 steps
2	4. if y2+1=0 <0,y1-1+1> else <y1-1+1,y2+1-1> fi = <0,0> 5. y1 0 <y1,y2> = <0,0>	2 steps