Nuprl - Proof: gcd sat pred 1 2

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

1. b :

b1:

. |b1|<|b|

(

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

b = 0

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

By:	InstHyp [a rem b;b] 2

Generated subgoals:

1 |a rem b|<|b|
1 step

2 5. GCD(b;a rem b;gcd(b;a rem b))
GCD(a;b;gcd(b;a rem b))
2 steps

About:

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

1	\|a rem b\|<\|b\|	1 step
2	5. GCD(b;a rem b;gcd(b;a rem b)) GCD(a;b;gcd(b;a rem b))	2 steps