Nuprl - Proof: gcd exists

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

a,b:

. GCD(a;b;y)

By:	UnivCD THEN (Decide (0b))

Generated subgoals:

1 1. a :
2. b :
3. 0b
y:. GCD(a;b;y)
1 step

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

About:

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

1	1. a : 2. b : 3. 0b y:. GCD(a;b;y)	1 step
2	1. a : 2. b : 3. 0b y:. GCD(a;b;y)	2 steps