Nuprl - Proof: next nat pair wf

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

next_nat_pair

By:	Def THEN Analyze THEN New:[x \| y] Analyze-1 THEN Reduce Concl

Generated subgoal:

1 1. x :
2. y :
if y=0 <0,x+1> else <x+1,y-1> fi
1 step

About:

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