1. a : 
2. b : 
3. y1 : 
4. GCD(a;b;y1)
5. gcd(a;b) = y1
6. y2 : 
7. GCD(b;a;y2)
8. gcd(b;a) = y2
  gcd(a;b) ~ gcd(b;a)

By:	(FwdThru Thm* a,b,y:. GCD(a;b;y)  GCD(b;a;y) [7]) THEN (FwdThru Thm* a,b,y1,y2:. GCD(a;b;y1)  GCD(a;b;y2)  (y1 ~ y2) [4;-1])

1

9. GCD(a;b;y2) 10. y1 ~ y2   gcd(a;b) ~ gcd(b;a)

1 step

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