(5steps total)
PrintForm
Definitions
Lemmas
num
thy
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
coprime
bezout
id0
1
1.
a
:
2.
b
:
3. GCD(
a
;
b
;1)
4.
u
:
5.
v
:
6. GCD(
b
;
a
;
u
b
+
v
a
)
x
,
y
:
. (
a
x
+
b
y
) ~ 1
By:
FwdThru
Thm*
a
,
b
,
y
:
. GCD(
a
;
b
;
y
)
GCD(
b
;
a
;
y
) [3]
Generated subgoal:
1
7. GCD(
b
;
a
;1)
x
,
y
:
. (
a
x
+
b
y
) ~ 1
3
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(5steps total)
PrintForm
Definitions
Lemmas
num
thy
1
Sections
StandardLIB
Doc
b+v
x,y:
a,b,y:
GCD(b;a;y) [3]
