1. a : 
2. b : 
3. y:. GCD(a;b;y) & gcd(a;b) = y
4. y:. GCD(b;a;y) & gcd(b;a) = y
  gcd(a;b) ~ gcd(b;a)

1

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)

2 steps

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