1. b : 
2. b:. b<b  (u,v:. GCD(b;b;ub+vb))
3. a : 
4. b = 0
  u,v:. GCD(a;b;ua+vb)

By:	Make the goal match the conclusion of Hyp:2, using Thm* a,b,y:. GCD(a;b;y)  GCD(b;a;y) and Thm* a,b:. a+b = b+a

1

u,v:. GCD(b;a;ub+va)

9 steps

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