theorem :: AOFA_I00:63

for A being Euclidean preIfWhileAlgebra
for X being non empty countable set
for b being Element of X
for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)
for x, y, z being Variable of g st ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . z = 3 ) holds
for s being Element of Funcs (X,INT)
for n, m being Element of NAT st n = s . x & m = s . y & n > m holds
(g . (s,(while ((y gt 0),((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))))) . x = n gcd m