num thy 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
2Thm* a,b:. GCD(a;b;gcd(a;b))[gcd_sat_pred]
cites the following:
1Thm* a:. GCD(a;0;a)[gcd_p_zero]
0Thm* a:b:. |a rem b|<|b|[rem_bounds_z]
1Thm* a,b,y,k:. GCD(a;b;y GCD(a;b+ka;y)[gcd_p_shift]
1Thm* a:n:. (a rem n) = a-(a  n)n[rem_to_div]
0Thm* a,b,y:. GCD(a;b;y GCD(b;a;y)[gcd_p_sym]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
num thy 1 Sections StandardLIB Doc