Nuprl - Proof: bezout ident n sfa 1 1 2 1 1 1 1 1 1 1 1 1

(15steps total) Gloss PrintForm Definitions Lemmas NumThyExamples Sections NuprlLIB Doc

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

1. b :

2.

b:

. b<b

(

u,v:

. GCD(b;b;u

b+v

b))
3. a :

4.

b = 0
5. q :

6. r :

b
7. a = q

b+r
8. x :

9. y :

10. GCD(b;r+q

b;x

b+y

r)

u:

. u+y

q = x

By:	Witness: x-yq

Generated subgoals:

None

About:

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

(15steps total) Gloss PrintForm Definitions Lemmas NumThyExamples Sections NuprlLIB Doc