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

By:	SeqOnM [RWN 1 (LemmaC Thm* a:, n:. (a rem n) = a-(a  n)n) 5 ;Using [`k',(a  b)] (FwdThru Thm* a,b,y,k:. GCD(a;b;y)  GCD(a;b+ka;y) [5]) ;ArithSimp 6]

1

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))

1 step

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