Thm* b:, a:. u,v:. GCD(a;b;ua+vb)

This proof proceeds by induction, and will be seen to rather subtly combine the inductive hypothesis and a couple of lemmas:

b<b  (a:. u,v:. GCD(a;b;ua+vb)) (inductive hyp)
Thm* a,b,y:. GCD(a;b;y)  GCD(b;a;y)
Thm* a,b,y,k:. GCD(a;b;y)  GCD(a;b+ka;y)

Note the complex argument of the last lemma is suggestive of the division theorem

Thm* a:, b:. q:, r:b. a = qb+r

Let's proceed. Use true-for-less induction on b   to show that

a:. u,v:. GCD(a;b;ua+vb)

under the inductive hyp mentioned above for b<b.
It turns out that the inductive hyp will be used with b in place of a, and something else (a remainder) in place of b, so in anticipation we shall immediately simplify our inductive hyp to

b:. b<b  (u,v:. GCD(b;b;ub+vb)).

Recall we are trying to show that

u,v:. GCD(a;b;ua+vb)

If b = 0 then our goal follows from lemma Thm* a:. GCD(a;0;a) by letting u be 1 and v be 0.
So assume for the rest that b = 0.
Let's improve the match between our goal and our simplified inductive hyp. It is enough to show

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

since Thm* a,b,y:. GCD(a;b;y)  GCD(b;a;y) (and Thm* a,b:. a+b = b+a).
Using division, a = qb+r, for some q   and some r   such that r<b, and rewriting all a's in our latest goal with this equality gives us the new goal

u,v:. GCD(b;r+qb;ub+v(r+qb)).

Applying our simplified inductive hyp the the remainder r<b, gives us x,y:. GCD(b;r;xb+yr), and via Thm* a,b,y,k:. GCD(a;b;y)  GCD(a;b+ka;y),

x,y:. GCD(b;r+qb;xb+yr),

which differs from our new goal only in one argument to GCD(<int>;<int>;<int>).
So, it is enough to show

u,v:. ub+v(r+qb) = xb+yr, which would follow from

u:. ub+y(r+qb) = xb+yr, by using y for v, which would follow from

u:. ub+yqb = xb, which is satisfied by x-qy

QED

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