1. b : 
2. b1:. b1<b  (a:. u,v:. GCD(a;b1;ua+vb1))
3. a : 
4. b = 0
5. q : 
6. r : b
7. a = qb+r
8. u : 
9. v : 
10. GCD(b;r;ub+vr)
  u,v:. GCD(a;b;ua+vb)

By:	(InstConcl [v;u-qv]) THEN (HypSubst 7 0) THEN (OnMCls [0;10] ArithSimp)

1

10. GCD(b;r;bu+rv)   GCD(r+bq;b;bu+rv)

2 steps

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