:: deftheorem Def2 defines ALGO_EXGCD NTALGO_1:def 2 :
for x, y being Element of INT
for b₃ being Element of [:INT,INT,INT:] holds
( b₃ = ALGO_EXGCD (x,y) iff ex g, w, q, t, a, b, v, u being sequence of INT ex istop being Nat st
( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Nat holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) & istop = min* { i where i is Nat : w . i = 0 } & ( 0 <= g . istop implies b₃ = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies b₃ = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) );