Nuprl - Proof: gcd exists n 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: gcd exists n 1

1. b :

b1:

. b1<b

(

. GCD(a;b1;y))
3. a :

. GCD(a;b;y)

By:	Decide (b = 0)

Generated subgoals:

1 4. b = 0
y:. GCD(a;b;y)
2 steps

2 4. b = 0
y:. GCD(a;b;y)
6 steps

About:

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

1	4. b = 0 y:. GCD(a;b;y)	2 steps
2	4. b = 0 y:. GCD(a;b;y)	6 steps