1. a : 
2. b : 
  gcd(a;b) ~ gcd(b;a)

By:	(Inst Thm* a,b:. y:. GCD(a;b;y) & gcd(a;b) = y [a;b]) THEN (Inst Thm* a,b:. y:. GCD(a;b;y) & gcd(a;b) = y [b;a])

1

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)

3 steps

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