Nuprl - Proof: bezout ident n sfa 1 1

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

1. b :

. b<b

(

u,v:

. GCD(b;b;u

b+v

b))
3. a :

u,v:

. GCD(a;b;u

a+v

By:	Decide: b = 0

Generated subgoals:

1 4. b = 0
u,v:. GCD(a;b;ua+vb)
2 steps

2 4. b = 0
u,v:. GCD(a;b;ua+vb)
10 steps

About:

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

1	4. b = 0 u,v:. GCD(a;b;ua+vb)	2 steps
2	4. b = 0 u,v:. GCD(a;b;ua+vb)	10 steps