1. b : 
2. b1:. |b1|<|b|  (a:. GCD(a;b1;gcd(a;b1)))
3. a : 
4. b = 0
5. GCD(b;a-(a  b)b;gcd(b;a rem b))
6. GCD(b;a;gcd(b;a rem b))
  GCD(a;b;gcd(b;a rem b))

By:	BackThru Thm* a,b,y:. GCD(a;b;y)  GCD(b;a;y)

None

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