(4steps total)
PrintForm
Definitions
Lemmas
num
thy
1
Sections
StandardLIB
Search
Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
gcd
exists
a
,
b
:
.
y
:
. GCD(
a
;
b
;
y
)
By:
UnivCD THEN (Decide (0
b
))
Generated subgoals:
1
1.
a
:
2.
b
:
3. 0
b
y
:
. GCD(
a
;
b
;
y
)
1
step
2
1.
a
:
2.
b
:
3.
0
b
y
:
. GCD(
a
;
b
;
y
)
2
steps
About:
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
(4steps total)
PrintForm
Definitions
Lemmas
num
thy
1
Sections
StandardLIB
Search
Doc
a,b:
. 
y:. GCD(a;b;y) a,b:. y:. GCD(a;b;y)
b))
b
y:. GCD(a;b;y)
0b
y:. GCD(a;b;y)
