:: deftheorem Def1 defines ALGO_GCD NTALGO_1:def 1 :
for a, b being Integer
for b₃ being Element of NAT holds
( b₃ = ALGO_GCD (a,b) iff ex A, B being sequence of NAT st
( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & b₃ = A . (min* { i where i is Nat : B . i = 0 } ) ) );