(7steps 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:
gcd
p
mul
3
1
1.
a
:
2.
b
:
3.
y
:
4.
n
:
5. GCD(
a
;
b
;
y
)
6.
z
:
7.
z
|
n
a
8.
z
|
n
b
9.
u
:
10.
v
:
11. GCD(
a
;
b
;
u
a
+
v
b
)
12.
y
~ (
u
a
+
v
b
)
z
|
n
y
By:
RWH (HypC 12) 0
Generated subgoal:
1
z
|
n
(
u
a
+
v
b
)
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PrintForm
Definitions
Lemmas
num
thy
1
Sections
StandardLIB
Doc
a
z | n
