Nuprl - Proof: gcd sat gcd p 1

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

1. b :

b1:

. |b1|<|b|

(

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

GCD(a;b;gcd(a;b))

By:	RecCaseSplit `gcd`

Generated subgoals:

1 4. b = 0
GCD(a;b;a)
1 step

2 4. b = 0
GCD(a;b;gcd(b;a rem b))
4 steps

About:

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

1	4. b = 0 GCD(a;b;a)	1 step
2	4. b = 0 GCD(a;b;gcd(b;a rem b))	4 steps